@@ -128,14 +128,6 @@ private predicate adjacentDefRead(
128
128
v = def .getSourceVariable ( )
129
129
}
130
130
131
- pragma [ noinline]
132
- private predicate adjacentDefReadExt (
133
- DefinitionExt def , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 , SsaInput:: SourceVariable v
134
- ) {
135
- Impl:: adjacentDefReadExt ( def , _, bb1 , i1 , bb2 , i2 ) and
136
- v = def .getSourceVariable ( )
137
- }
138
-
139
131
/** Holds if `v` is read at index `i` in basic block `bb`. */
140
132
private predicate variableReadActual ( BasicBlock bb , int i , Variable v ) {
141
133
exists ( VariableAccess read |
@@ -191,22 +183,6 @@ private predicate adjacentDefReachesRead(
191
183
)
192
184
}
193
185
194
- private predicate adjacentDefReachesReadExt (
195
- DefinitionExt def , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2
196
- ) {
197
- exists ( SsaInput:: SourceVariable v | adjacentDefReadExt ( def , bb1 , i1 , bb2 , i2 , v ) |
198
- def .definesAt ( v , bb1 , i1 , _)
199
- or
200
- SsaInput:: variableRead ( bb1 , i1 , v , true )
201
- )
202
- or
203
- exists ( BasicBlock bb3 , int i3 |
204
- adjacentDefReachesReadExt ( def , bb1 , i1 , bb3 , i3 ) and
205
- SsaInput:: variableRead ( bb3 , i3 , _, false ) and
206
- Impl:: adjacentDefReadExt ( def , _, bb3 , i3 , bb2 , i2 )
207
- )
208
- }
209
-
210
186
/** Same as `adjacentDefRead`, but skips uncertain reads. */
211
187
pragma [ nomagic]
212
188
private predicate adjacentDefSkipUncertainReads (
0 commit comments