@@ -19,23 +19,50 @@ predicate oppositeOperators(string op1, string op2) {
1919/* this match is very syntactic: we simply check that op1 is defined as
2020 !op2(_, _) */
2121predicate implementedAsNegationOf ( Operator op1 , Operator op2 ) {
22- exists ( Block b , ReturnStmt r , NotExpr n , FunctionCall c |
22+ exists ( Block b , ReturnStmt r , NotExpr n , Expr o |
2323 b = op1 .getBlock ( ) and
2424 b .getNumStmt ( ) = 1 and
2525 r = b .getStmt ( 0 ) and
2626 n = r .getExpr ( ) and
27- c = n .getOperand ( ) and
28- c .getTarget ( ) = op2 )
27+ o = n .getOperand ( ) and
28+ (
29+ o instanceof LTExpr and op2 .hasName ( "operator<" ) or
30+ o instanceof LEExpr and op2 .hasName ( "operator<=" ) or
31+ o instanceof GTExpr and op2 .hasName ( "operator>" ) or
32+ o instanceof GEExpr and op2 .hasName ( "operator>=" ) or
33+ o instanceof EQExpr and op2 .hasName ( "operator==" ) or
34+ o instanceof NEExpr and op2 .hasName ( "operator!=" ) or
35+ o .( FunctionCall ) .getTarget ( ) = op2
36+ )
37+ )
38+ }
39+
40+ predicate classIsCheckableFor ( Class c , string op ) {
41+ oppositeOperators ( op , _) and
42+ // We check the template, not its instantiations
43+ not c instanceof ClassTemplateInstantiation and
44+ // Member functions of templates are not necessarily instantiated, so
45+ // if the function we want to check exists, then make sure that its
46+ // body also exists
47+ ( ( c instanceof TemplateClass )
48+ implies
49+ forall ( Function f | f = c .getAMember ( ) and f .hasName ( op )
50+ | exists ( f .getEntryPoint ( ) ) ) )
2951}
3052
3153from Class c , string op , string opp , Operator rator
3254where c .fromSource ( ) and
3355 oppositeOperators ( op , opp ) and
56+ classIsCheckableFor ( c , op ) and
57+ classIsCheckableFor ( c , opp ) and
3458 rator = c .getAMember ( ) and
3559 rator .hasName ( op ) and
36- not exists ( Operator oprator | oprator = c .getAMember ( ) and
37- oprator .hasName ( opp ) and
38- ( implementedAsNegationOf ( rator , oprator )
39- or implementedAsNegationOf ( oprator , rator ) ) )
60+ forex ( Operator aRator |
61+ aRator = c .getAMember ( ) and aRator .hasName ( op ) |
62+ not exists ( Operator oprator |
63+ oprator = c .getAMember ( ) and
64+ oprator .hasName ( opp ) and
65+ ( implementedAsNegationOf ( aRator , oprator )
66+ or implementedAsNegationOf ( oprator , aRator ) ) ) )
4067select c , "When two operators are opposites, both should be defined and one should be defined in terms of the other. Operator " + op +
4168 " is declared on line " + rator .getLocation ( ) .getStartLine ( ) .toString ( ) + ", but it is not defined in terms of its opposite operator " + opp + "."
0 commit comments