@@ -82,36 +82,20 @@ module ValidState {
82
82
* library will perform, and visit all the places where the size argument is modified.
83
83
* 2. Once that dataflow traversal is done, we accumulate the offsets added at each places
84
84
* where the offset is modified (see `validStateImpl`).
85
- *
86
- * Because we want to guarantee that each place where we modify the offset has a `PathNode`
87
- * we "flip" a boolean flow state in each `isAdditionalFlowStep`. This ensures that the node
88
- * has a corresponding `PathNode`.
89
85
*/
90
- private module ValidStateConfig implements DataFlow:: StateConfigSig {
91
- class FlowState = boolean ;
92
-
93
- predicate isSource ( DataFlow:: Node source , FlowState state ) {
94
- hasSize ( _, source , _) and
95
- state = false
96
- }
86
+ private module ValidStateConfig implements DataFlow:: ConfigSig {
87
+ predicate isSource ( DataFlow:: Node source ) { hasSize ( _, source , _) }
97
88
98
- predicate isSink ( DataFlow:: Node sink , FlowState state ) {
99
- isSinkPairImpl ( _, _, sink , _, _) and
100
- state = [ false , true ]
101
- }
89
+ predicate isSink ( DataFlow:: Node sink ) { isSinkPairImpl ( _, _, sink , _, _) }
102
90
103
- predicate isAdditionalFlowStep (
104
- DataFlow:: Node node1 , FlowState state1 , DataFlow:: Node node2 , FlowState state2
105
- ) {
106
- isAdditionalFlowStep2 ( node1 , node2 , _) and
107
- state1 = [ false , true ] and
108
- state2 = state1 .booleanNot ( )
91
+ predicate isAdditionalFlowStep ( DataFlow:: Node node1 , DataFlow:: Node node2 ) {
92
+ isAdditionalFlowStep2 ( node1 , node2 , _)
109
93
}
110
94
111
95
predicate includeHiddenNodes ( ) { any ( ) }
112
96
}
113
97
114
- private import DataFlow:: GlobalWithState < ValidStateConfig >
98
+ private import DataFlow:: Global < ValidStateConfig >
115
99
116
100
private predicate inLoop ( PathNode n ) { n .getASuccessor + ( ) = n }
117
101
0 commit comments