@@ -133,6 +133,18 @@ module ProductFlow {
133
133
this .isAdditionalFlowStep2 ( node1 , node2 )
134
134
}
135
135
136
+ /**
137
+ * Holds if data flow into `node` is prohibited in the first projection of the product
138
+ * dataflow graph.
139
+ */
140
+ predicate isBarrierIn1 ( DataFlow:: Node node ) { none ( ) }
141
+
142
+ /**
143
+ * Holds if data flow into `node` is prohibited in the second projection of the product
144
+ * dataflow graph.
145
+ */
146
+ predicate isBarrierIn2 ( DataFlow:: Node node ) { none ( ) }
147
+
136
148
predicate hasFlowPath (
137
149
DataFlow:: PathNode source1 , DataFlow2:: PathNode source2 , DataFlow:: PathNode sink1 ,
138
150
DataFlow2:: PathNode sink2
@@ -169,6 +181,10 @@ module ProductFlow {
169
181
) {
170
182
exists ( Configuration conf | conf .isAdditionalFlowStep1 ( node1 , state1 , node2 , state2 ) )
171
183
}
184
+
185
+ override predicate isBarrierIn ( DataFlow:: Node node ) {
186
+ exists ( Configuration conf | conf .isBarrierIn1 ( node ) )
187
+ }
172
188
}
173
189
174
190
class Conf2 extends DataFlow2:: Configuration {
@@ -202,9 +218,14 @@ module ProductFlow {
202
218
) {
203
219
exists ( Configuration conf | conf .isAdditionalFlowStep2 ( node1 , state1 , node2 , state2 ) )
204
220
}
221
+
222
+ override predicate isBarrierIn ( DataFlow:: Node node ) {
223
+ exists ( Configuration conf | conf .isBarrierIn2 ( node ) )
224
+ }
205
225
}
206
226
}
207
227
228
+ pragma [ nomagic]
208
229
private predicate reachableInterprocEntry (
209
230
Configuration conf , DataFlow:: PathNode source1 , DataFlow2:: PathNode source2 ,
210
231
DataFlow:: PathNode node1 , DataFlow2:: PathNode node2
0 commit comments