@@ -19,23 +19,50 @@ predicate oppositeOperators(string op1, string op2) {
19
19
/* this match is very syntactic: we simply check that op1 is defined as
20
20
!op2(_, _) */
21
21
predicate 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 |
23
23
b = op1 .getBlock ( ) and
24
24
b .getNumStmt ( ) = 1 and
25
25
r = b .getStmt ( 0 ) and
26
26
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 ( ) ) ) )
29
51
}
30
52
31
53
from Class c , string op , string opp , Operator rator
32
54
where c .fromSource ( ) and
33
55
oppositeOperators ( op , opp ) and
56
+ classIsCheckableFor ( c , op ) and
57
+ classIsCheckableFor ( c , opp ) and
34
58
rator = c .getAMember ( ) and
35
59
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 ) ) ) )
40
67
select c , "When two operators are opposites, both should be defined and one should be defined in terms of the other. Operator " + op +
41
68
" is declared on line " + rator .getLocation ( ) .getStartLine ( ) .toString ( ) + ", but it is not defined in terms of its opposite operator " + opp + "."
0 commit comments