@@ -18,7 +18,7 @@ import semmle.code.cpp.commons.Scanf
18
18
import semmle.code.cpp.controlflow.Guards
19
19
import semmle.code.cpp.dataflow.new.DataFlow:: DataFlow
20
20
import semmle.code.cpp.ir.IR
21
- import semmle.code.cpp.ir.ValueNumbering
21
+ import semmle.code.cpp.valuenumbering.GlobalValueNumbering
22
22
import ScanfChecks
23
23
import ScanfToUseFlow:: PathGraph
24
24
@@ -155,31 +155,20 @@ predicate hasNonGuardedAccess(
155
155
flowPath ( source , call , index , sink , e ) and
156
156
minGuard = getMinimumGuardConstant ( call , index )
157
157
|
158
- not exists ( int value |
159
- e .getBasicBlock ( ) = blockGuardedBy ( value , "==" , call ) and minGuard <= value
158
+ not exists ( GuardCondition guard |
159
+ // call == k and k >= minGuard so call >= minGuard
160
+ guard
161
+ .ensuresEq ( globalValueNumber ( call ) .getAnExpr ( ) , any ( int k | minGuard <= k ) ,
162
+ e .getBasicBlock ( ) , true )
160
163
or
161
- e .getBasicBlock ( ) = blockGuardedBy ( value , "<" , call ) and minGuard - 1 <= value
162
- or
163
- e .getBasicBlock ( ) = blockGuardedBy ( value , "<=" , call ) and minGuard <= value
164
+ // call >= k and k >= minGuard so call >= minGuard
165
+ guard
166
+ .ensuresLt ( globalValueNumber ( call ) .getAnExpr ( ) , any ( int k | minGuard <= k ) ,
167
+ e .getBasicBlock ( ) , false )
164
168
)
165
169
)
166
170
}
167
171
168
- /** Returns a block guarded by the assertion of `value op call` */
169
- BasicBlock blockGuardedBy ( int value , string op , ScanfFunctionCall call ) {
170
- exists ( GuardCondition g , Expr left , Expr right |
171
- right = g .getAChild ( ) and
172
- value = left .getValue ( ) .toInt ( ) and
173
- localExprFlow ( call , right )
174
- |
175
- g .ensuresEq ( left , right , 0 , result , true ) and op = "=="
176
- or
177
- g .ensuresLt ( left , right , 0 , result , true ) and op = "<"
178
- or
179
- g .ensuresLt ( left , right , 1 , result , true ) and op = "<="
180
- )
181
- }
182
-
183
172
from
184
173
ScanfToUseFlow:: PathNode source , ScanfToUseFlow:: PathNode sink , ScanfFunctionCall call , Expr e ,
185
174
int minGuard
0 commit comments