@@ -55,32 +55,30 @@ predicate resultIsChecked(SSLGetPeerCertificateCall getCertCall, ControlFlowNode
5555predicate certIsZero (
5656 SSLGetPeerCertificateCall getCertCall , ControlFlowNode node1 , ControlFlowNode node2
5757) {
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 ( )
7370 )
74- or
71+ )
72+ or
73+ (
7574 // if (cert) { }
76- guard = cert and
77- node1 = guard and
78- node2 = guard .getAFalseSuccessor ( )
75+ node1 = cert
7976 or
8077 // 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
8482 )
8583}
8684
0 commit comments