@@ -192,13 +192,13 @@ module ProductFlow {
192192 * Holds if data flow through `node` is prohibited through the first projection of the product
193193 * dataflow graph when the flow state is `state`.
194194 */
195- predicate isBarrier1 ( DataFlow:: Node node , FlowState1 state ) ;
195+ default predicate isBarrier1 ( DataFlow:: Node node , FlowState1 state ) { none ( ) }
196196
197197 /**
198198 * Holds if data flow through `node` is prohibited through the second projection of the product
199199 * dataflow graph when the flow state is `state`.
200200 */
201- predicate isBarrier2 ( DataFlow:: Node node , FlowState2 state ) ;
201+ default predicate isBarrier2 ( DataFlow:: Node node , FlowState2 state ) { none ( ) }
202202
203203 /**
204204 * Holds if data flow through `node` is prohibited through the first projection of the product
@@ -237,9 +237,11 @@ module ProductFlow {
237237 *
238238 * This step is only applicable in `state1` and updates the flow state to `state2`.
239239 */
240- predicate isAdditionalFlowStep1 (
240+ default predicate isAdditionalFlowStep1 (
241241 DataFlow:: Node node1 , FlowState1 state1 , DataFlow:: Node node2 , FlowState1 state2
242- ) ;
242+ ) {
243+ none ( )
244+ }
243245
244246 /**
245247 * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
@@ -253,9 +255,11 @@ module ProductFlow {
253255 *
254256 * This step is only applicable in `state1` and updates the flow state to `state2`.
255257 */
256- predicate isAdditionalFlowStep2 (
258+ default predicate isAdditionalFlowStep2 (
257259 DataFlow:: Node node1 , FlowState2 state1 , DataFlow:: Node node2 , FlowState2 state2
258- ) ;
260+ ) {
261+ none ( )
262+ }
259263
260264 /**
261265 * Holds if data flow into `node` is prohibited in the first projection of the product
0 commit comments