@@ -13,6 +13,14 @@ class Node extends TNode {
13
13
* Gets the underlying `Expr` or `VarDef` node, if this is an `AstNodeNode`.
14
14
*/
15
15
AstNode asAstNode ( ) { astNode ( result ) = this }
16
+
17
+ /**
18
+ * Gets the predicate containing this data-flow node.
19
+ *
20
+ * All data-flow nodes belong in exactly one predicate.
21
+ * TODO: select clauses
22
+ */
23
+ Predicate getEnclosingPredicate ( ) { none ( ) } // overridden in subclasses
16
24
}
17
25
18
26
/**
@@ -35,6 +43,10 @@ class AstNodeNode extends Node, MkAstNodeNode {
35
43
AstNode getAstNode ( ) {
36
44
result = ast
37
45
}
46
+
47
+ override Predicate getEnclosingPredicate ( ) {
48
+ result = ast .getEnclosingPredicate ( )
49
+ }
38
50
}
39
51
40
52
/**
@@ -71,6 +83,10 @@ class ScopedVariableNode extends Node, MkScopedVariable {
71
83
AstNode getScope ( ) {
72
84
result = scope
73
85
}
86
+
87
+ override Predicate getEnclosingPredicate ( ) {
88
+ result = var .getEnclosingPredicate ( )
89
+ }
74
90
}
75
91
76
92
/**
@@ -101,6 +117,10 @@ class ThisNode extends Node, MkThisNode {
101
117
Predicate getPredicate ( ) {
102
118
result = pred
103
119
}
120
+
121
+ override Predicate getEnclosingPredicate ( ) {
122
+ result = pred
123
+ }
104
124
}
105
125
106
126
/**
@@ -131,6 +151,10 @@ class ResultNode extends Node, MkResultNode {
131
151
Predicate getPredicate ( ) {
132
152
result = pred
133
153
}
154
+
155
+ override Predicate getEnclosingPredicate ( ) {
156
+ result = pred
157
+ }
134
158
}
135
159
136
160
/**
@@ -171,6 +195,10 @@ class FieldNode extends Node, MkFieldNode {
171
195
override Location getLocation ( ) {
172
196
result = pred .getLocation ( )
173
197
}
198
+
199
+ override Predicate getEnclosingPredicate ( ) {
200
+ result = pred
201
+ }
174
202
}
175
203
176
204
/**
0 commit comments