@@ -45,12 +45,7 @@ predicate isRealRange(Expr exp) {
45
45
lowerBound ( exp ) != - 8388608 and
46
46
lowerBound ( exp ) != - 65536 and
47
47
lowerBound ( exp ) != - 32768 and
48
- lowerBound ( exp ) != - 128 and
49
- lowerBound ( exp ) != 0 and
50
- lowerBound ( exp ) != upperBound ( exp )
51
- or
52
- lowerBound ( exp ) = 0 and
53
- upperBound ( exp ) = 1
48
+ lowerBound ( exp ) != - 128
54
49
}
55
50
56
51
/** Holds if the range of values for the condition is less than the choices. */
@@ -115,6 +110,10 @@ predicate isWrongLableName(SwitchStmt swtmp) {
115
110
predicate isCodeBeforeCase ( SwitchStmt swtmp ) {
116
111
exists ( Expr exp |
117
112
exp .getEnclosingStmt ( ) .getParentStmt * ( ) = swtmp .getStmt ( ) and
113
+ not exists ( Loop lp |
114
+ exp .getEnclosingStmt ( ) .getParentStmt * ( ) = lp and
115
+ lp .getEnclosingStmt ( ) .getParentStmt * ( ) = swtmp .getStmt ( )
116
+ ) and
118
117
not exists ( Stmt sttmp , SwitchCase sctmp |
119
118
sttmp = swtmp .getASwitchCase ( ) .getAStmt ( ) and
120
119
sctmp = swtmp .getASwitchCase ( ) and
@@ -129,6 +128,13 @@ predicate isCodeBeforeCase(SwitchStmt swtmp) {
129
128
from SwitchStmt sw , string msg
130
129
where
131
130
isRealRange ( sw .getExpr ( ) ) and
131
+ lowerBound ( sw .getExpr ( ) ) != upperBound ( sw .getExpr ( ) ) and
132
+ lowerBound ( sw .getExpr ( ) ) != 0 and
133
+ not exists ( Expr cexp |
134
+ cexp = sw .getASwitchCase ( ) .getExpr ( ) and not isRealRange ( cexp )
135
+ or
136
+ cexp = sw .getASwitchCase ( ) .getEndExpr ( ) and not isRealRange ( cexp )
137
+ ) and
132
138
not exists ( Expr exptmp |
133
139
exptmp = sw .getExpr ( ) .getAChild * ( ) and
134
140
not exptmp .isConstant ( ) and
0 commit comments