File tree Expand file tree Collapse file tree 1 file changed +11
-13
lines changed
Expand file tree Collapse file tree 1 file changed +11
-13
lines changed Original file line number Diff line number Diff line change @@ -32,20 +32,18 @@ private string getEofValue() {
3232 * Holds if the value of `call` has been checked to not equal `EOF`.
3333 */
3434private predicate checkedForEof ( ScanfFunctionCall call ) {
35- exists ( IRGuardCondition gc |
36- exists ( CallInstruction i | i .getUnconvertedResultExpression ( ) = call |
37- exists ( int val | gc .comparesEq ( valueNumber ( i ) .getAUse ( ) , val , _, _) |
38- // call == EOF
39- val = getEofValue ( ) .toInt ( )
40- or
41- // call == [any positive number]
42- val > 0
43- )
35+ exists ( IRGuardCondition gc , CallInstruction i | i .getUnconvertedResultExpression ( ) = call |
36+ exists ( int val | gc .comparesEq ( valueNumber ( i ) .getAUse ( ) , val , _, _) |
37+ // call == EOF
38+ val = getEofValue ( ) .toInt ( )
4439 or
45- exists ( int val | gc .comparesLt ( valueNumber ( i ) .getAUse ( ) , val , true , _) |
46- // call < [any non-negative number] (EOF is guaranteed to be negative)
47- val >= 0
48- )
40+ // call == [any positive number]
41+ val > 0
42+ )
43+ or
44+ exists ( int val | gc .comparesLt ( valueNumber ( i ) .getAUse ( ) , val , true , _) |
45+ // call < [any non-negative number] (EOF is guaranteed to be negative)
46+ val >= 0
4947 )
5048 )
5149}
You can’t perform that action at this time.
0 commit comments