@@ -667,19 +667,19 @@ predicate storeStep(Node node1, ContentSet c, Node node2) {
667667 c .isSingleton ( fc )
668668 )
669669 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 |
674671 node2 .( PostUpdateNode ) .getPreUpdateNode ( ) .asExpr ( ) = var .getBase ( ) and
675672 node1 .asStmt ( ) = var .getAssignStmt ( ) .getRightHandSide ( ) and
676- c .isKnownOrUnknownElement ( ec ) and
677- index = ec .getIndex ( ) .asInt ( ) and
678673 e = var .getIndex ( )
679674 |
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+ )
681680 or
682- not exists ( e .getValue ( ) .asInt ( ) )
681+ not exists ( e .getValue ( ) .asInt ( ) ) and
682+ c .isAnyElement ( )
683683 )
684684 or
685685 exists ( Content:: KnownElementContent ec , int index |
@@ -712,19 +712,19 @@ predicate readStep(Node node1, ContentSet c, Node node2) {
712712 c .isSingleton ( fc )
713713 )
714714 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 |
719716 node2 .asExpr ( ) = var and
720717 node1 .asExpr ( ) = var .getBase ( ) and
721- c .isKnownOrUnknownElement ( ec ) and
722- index = ec .getIndex ( ) .asInt ( ) and
723718 e = var .getIndex ( )
724719 |
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+ )
726725 or
727- not exists ( e .getValue ( ) .asInt ( ) )
726+ not exists ( e .getValue ( ) .asInt ( ) ) and
727+ c .isAnyElement ( )
728728 )
729729 or
730730 exists ( CfgNode cfgNode |
0 commit comments