@@ -667,19 +667,19 @@ predicate storeStep(Node node1, ContentSet c, Node node2) {
667
667
c .isSingleton ( fc )
668
668
)
669
669
or
670
- exists (
671
- CfgNodes:: ExprNodes:: IndexCfgWriteNode var , Content:: KnownElementContent ec , int index ,
672
- CfgNodes:: ExprCfgNode e
673
- |
670
+ exists ( CfgNodes:: ExprNodes:: IndexCfgWriteNode var , CfgNodes:: ExprCfgNode e |
674
671
node2 .( PostUpdateNode ) .getPreUpdateNode ( ) .asExpr ( ) = var .getBase ( ) and
675
672
node1 .asStmt ( ) = var .getAssignStmt ( ) .getRightHandSide ( ) and
676
- c .isKnownOrUnknownElement ( ec ) and
677
- index = ec .getIndex ( ) .asInt ( ) and
678
673
e = var .getIndex ( )
679
674
|
680
- index = e .getValue ( ) .asInt ( )
675
+ exists ( int index , Content:: KnownElementContent ec |
676
+ c .isKnownOrUnknownElement ( ec ) and
677
+ index = ec .getIndex ( ) .asInt ( ) and
678
+ index = e .getValue ( ) .asInt ( )
679
+ )
681
680
or
682
- not exists ( e .getValue ( ) .asInt ( ) )
681
+ not exists ( e .getValue ( ) .asInt ( ) ) and
682
+ c .isAnyElement ( )
683
683
)
684
684
or
685
685
exists ( Content:: KnownElementContent ec , int index |
@@ -712,19 +712,19 @@ predicate readStep(Node node1, ContentSet c, Node node2) {
712
712
c .isSingleton ( fc )
713
713
)
714
714
or
715
- exists (
716
- CfgNodes:: ExprNodes:: IndexCfgReadNode var , Content:: KnownElementContent ec , int index ,
717
- CfgNodes:: ExprCfgNode e
718
- |
715
+ exists ( CfgNodes:: ExprNodes:: IndexCfgReadNode var , CfgNodes:: ExprCfgNode e |
719
716
node2 .asExpr ( ) = var and
720
717
node1 .asExpr ( ) = var .getBase ( ) and
721
- c .isKnownOrUnknownElement ( ec ) and
722
- index = ec .getIndex ( ) .asInt ( ) and
723
718
e = var .getIndex ( )
724
719
|
725
- index = e .getValue ( ) .asInt ( )
720
+ exists ( int index , Content:: KnownElementContent ec |
721
+ c .isKnownOrUnknownElement ( ec ) and
722
+ index = ec .getIndex ( ) .asInt ( ) and
723
+ index = e .getValue ( ) .asInt ( )
724
+ )
726
725
or
727
- not exists ( e .getValue ( ) .asInt ( ) )
726
+ not exists ( e .getValue ( ) .asInt ( ) ) and
727
+ c .isAnyElement ( )
728
728
)
729
729
or
730
730
exists ( CfgNode cfgNode |
0 commit comments