@@ -27,7 +27,7 @@ class VariableEffectOrAccess extends Expr {
27
27
pragma [ noinline]
28
28
predicate partOfFullExpr ( VariableEffectOrAccess e , FullExpr fe ) {
29
29
(
30
- e . ( VariableEffect ) .getAnAccess ( ) = fe .getAChild + ( )
30
+ exists ( VariableEffect ve | e = ve and ve .getAnAccess ( ) = fe .getAChild + ( ) and not ve . isPartial ( ) )
31
31
or
32
32
e .( VariableAccess ) = fe .getAChild + ( )
33
33
)
@@ -154,6 +154,24 @@ int getOperandIndex(LeftRightOperation binop, Expr operand) {
154
154
)
155
155
}
156
156
157
+ predicate inConditionalThen ( ConditionalExpr ce , Expr e ) {
158
+ e = ce .getThen ( )
159
+ or
160
+ exists ( Expr parent |
161
+ inConditionalThen ( ce , parent ) and
162
+ parent .getAChild ( ) = e
163
+ )
164
+ }
165
+
166
+ predicate inConditionalElse ( ConditionalExpr ce , Expr e ) {
167
+ e = ce .getElse ( )
168
+ or
169
+ exists ( Expr parent |
170
+ inConditionalElse ( ce , parent ) and
171
+ parent .getAChild ( ) = e
172
+ )
173
+ }
174
+
157
175
from
158
176
ConstituentExprOrdering orderingConfig , FullExpr fullExpr , VariableEffect variableEffect1 ,
159
177
VariableAccess va1 , VariableAccess va2 , Locatable placeHolder , string label
@@ -219,8 +237,6 @@ where
219
237
not variableEffect1 .getAChild + ( ) = va2
220
238
) and
221
239
// Both are evaluated
222
- not exists ( ConditionalExpr ce |
223
- ce .getThen ( ) .getAChild * ( ) = va1 and ce .getElse ( ) .getAChild * ( ) = va2
224
- )
240
+ not exists ( ConditionalExpr ce | inConditionalThen ( ce , va1 ) and inConditionalElse ( ce , va2 ) )
225
241
select fullExpr , "The expression contains unsequenced $@ to $@ and $@ to $@." , variableEffect1 ,
226
242
"side effect" , va1 , va1 .getTarget ( ) .getName ( ) , placeHolder , label , va2 , va2 .getTarget ( ) .getName ( )
0 commit comments