@@ -31,57 +31,39 @@ predicate isGuarded(SubExpr sub, Expr left, Expr right) {
31
31
}
32
32
33
33
/**
34
- * Holds if `e ` is known or suspected to be less than or equal to
34
+ * Holds if `n ` is known or suspected to be less than or equal to
35
35
* `sub.getLeftOperand()`.
36
36
*/
37
- predicate exprIsSubLeftOrLess ( SubExpr sub , Element e ) {
38
- e = sub .getLeftOperand ( )
37
+ predicate exprIsSubLeftOrLess ( SubExpr sub , DataFlow :: Node n ) {
38
+ n = DataFlow :: exprNode ( sub .getLeftOperand ( ) )
39
39
or
40
- exists ( Expr other |
40
+ exists ( DataFlow :: Node other |
41
41
// dataflow
42
42
exprIsSubLeftOrLess ( sub , other ) and
43
43
(
44
- DataFlow:: localFlowStep ( DataFlow :: exprNode ( e ) , DataFlow :: exprNode ( other ) ) or
45
- DataFlow:: localFlowStep ( DataFlow :: exprNode ( other ) , DataFlow :: exprNode ( e ) )
44
+ DataFlow:: localFlowStep ( n , other ) or
45
+ DataFlow:: localFlowStep ( other , n )
46
46
)
47
47
)
48
48
or
49
- exists ( Element other |
50
- // dataflow (via parameter)
51
- exprIsSubLeftOrLess ( sub , other ) and
52
- (
53
- DataFlow:: localFlowStep ( DataFlow:: parameterNode ( e ) , DataFlow:: exprNode ( other ) ) or
54
- DataFlow:: localFlowStep ( DataFlow:: parameterNode ( other ) , DataFlow:: exprNode ( e ) )
55
- )
56
- )
57
- or
58
- exists ( Element other |
59
- // dataflow (via uninitialized)
60
- exprIsSubLeftOrLess ( sub , other ) and
61
- (
62
- DataFlow:: localFlowStep ( DataFlow:: uninitializedNode ( e ) , DataFlow:: exprNode ( other ) ) or
63
- DataFlow:: localFlowStep ( DataFlow:: uninitializedNode ( other ) , DataFlow:: exprNode ( e ) )
64
- )
65
- )
66
- or
67
- exists ( Expr other |
49
+ exists ( DataFlow:: Node other |
68
50
// guard constraining `sub`
69
51
exprIsSubLeftOrLess ( sub , other ) and
70
- isGuarded ( sub , other , e ) // other >= e
52
+ isGuarded ( sub , other . asExpr ( ) , n . asExpr ( ) ) // other >= e
71
53
)
72
54
or
73
- exists ( Expr other , float p , float q |
55
+ exists ( DataFlow :: Node other , float p , float q |
74
56
// linear access of `other`
75
57
exprIsSubLeftOrLess ( sub , other ) and
76
- linearAccess ( e , other , p , q ) and // e = p * other + q
58
+ linearAccess ( n . asExpr ( ) , other . asExpr ( ) , p , q ) and // e = p * other + q
77
59
p <= 1 and
78
60
q <= 0
79
61
)
80
62
or
81
- exists ( Expr other , float p , float q |
63
+ exists ( DataFlow :: Node other , float p , float q |
82
64
// linear access of `e`
83
65
exprIsSubLeftOrLess ( sub , other ) and
84
- linearAccess ( other , e , p , q ) and // other = p * e + q
66
+ linearAccess ( other . asExpr ( ) , n . asExpr ( ) , p , q ) and // other = p * e + q
85
67
p >= 1 and
86
68
q >= 0
87
69
)
95
77
ro .getGreaterOperand ( ) = sub and
96
78
sub .getFullyConverted ( ) .getUnspecifiedType ( ) .( IntegralType ) .isUnsigned ( ) and
97
79
exprMightOverflowNegatively ( sub .getFullyConverted ( ) ) and // generally catches false positives involving constants
98
- not exprIsSubLeftOrLess ( sub , sub .getRightOperand ( ) ) // generally catches false positives where there's a relation between the left and right operands
80
+ not exprIsSubLeftOrLess ( sub , DataFlow :: exprNode ( sub .getRightOperand ( ) ) ) // generally catches false positives where there's a relation between the left and right operands
99
81
select ro , "Unsigned subtraction can never be negative."
0 commit comments