@@ -128,14 +128,6 @@ private predicate adjacentDefRead(
128128 v = def .getSourceVariable ( )
129129}
130130
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-
139131/** Holds if `v` is read at index `i` in basic block `bb`. */
140132private predicate variableReadActual ( BasicBlock bb , int i , Variable v ) {
141133 exists ( VariableAccess read |
@@ -191,22 +183,6 @@ private predicate adjacentDefReachesRead(
191183 )
192184}
193185
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-
210186/** Same as `adjacentDefRead`, but skips uncertain reads. */
211187pragma [ nomagic]
212188private predicate adjacentDefSkipUncertainReads (
0 commit comments