@@ -55,32 +55,30 @@ predicate resultIsChecked(SSLGetPeerCertificateCall getCertCall, ControlFlowNode
55
55
predicate certIsZero (
56
56
SSLGetPeerCertificateCall getCertCall , ControlFlowNode node1 , ControlFlowNode node2
57
57
) {
58
- exists ( GuardCondition guard , Expr cert |
59
- cert = globalValueNumber ( getCertCall ) .getAnExpr ( ) and
60
- (
61
- exists ( Expr zero |
62
- zero .getValue ( ) .toInt ( ) = 0 and
63
- node1 = guard and
64
- (
65
- // if (cert == zero) {
66
- guard .comparesEq ( cert , zero , 0 , true , true ) and
67
- node2 = guard .getATrueSuccessor ( )
68
- or
69
- // if (cert != zero) { }
70
- guard .comparesEq ( cert , zero , 0 , false , true ) and
71
- node2 = guard .getAFalseSuccessor ( )
72
- )
58
+ exists ( Expr cert | cert = globalValueNumber ( getCertCall ) .getAnExpr ( ) |
59
+ exists ( GuardCondition guard , Expr zero |
60
+ zero .getValue ( ) .toInt ( ) = 0 and
61
+ node1 = guard and
62
+ (
63
+ // if (cert == zero) {
64
+ guard .comparesEq ( cert , zero , 0 , true , true ) and
65
+ node2 = guard .getATrueSuccessor ( )
66
+ or
67
+ // if (cert != zero) { }
68
+ guard .comparesEq ( cert , zero , 0 , false , true ) and
69
+ node2 = guard .getAFalseSuccessor ( )
73
70
)
74
- or
71
+ )
72
+ or
73
+ (
75
74
// if (cert) { }
76
- guard = cert and
77
- node1 = guard and
78
- node2 = guard .getAFalseSuccessor ( )
75
+ node1 = cert
79
76
or
80
77
// if (!cert) {
81
- node1 = guard .getParent ( ) and
82
- node2 = guard .getParent ( ) .( NotExpr ) .getATrueSuccessor ( )
83
- )
78
+ node1 .( NotExpr ) .getAChild ( ) = cert
79
+ ) and
80
+ node2 = node1 .getASuccessor ( ) and
81
+ not cert .( GuardCondition ) .controls ( node2 , true ) // cert may be false
84
82
)
85
83
}
86
84
0 commit comments