@@ -660,10 +660,9 @@ predicate storeStep(Node node1, ContentSet c, Node node2) {
660660 node1 .asStmt ( ) = var .getAssignStmt ( ) .getRightHandSide ( ) and
661661 e = var .getIndex ( )
662662 |
663- exists ( int index , Content:: KnownElementContent ec |
663+ exists ( Content:: KnownElementContent ec |
664664 c .isKnownOrUnknownElement ( ec ) and
665- index = ec .getIndex ( ) .asInt ( ) and
666- index = e .getValue ( ) .asInt ( )
665+ e .getValue ( ) = ec .getIndex ( )
667666 )
668667 or
669668 not exists ( e .getValue ( ) .asInt ( ) ) and
@@ -676,6 +675,18 @@ predicate storeStep(Node node1, ContentSet c, Node node2) {
676675 index = ec .getIndex ( ) .asInt ( )
677676 )
678677 or
678+ exists ( CfgNodes:: ExprCfgNode key |
679+ node2 .asExpr ( ) .( CfgNodes:: ExprNodes:: HashTableCfgNode ) .getElement ( key ) = node1 .asStmt ( )
680+ |
681+ exists ( Content:: KnownElementContent ec |
682+ c .isKnownOrUnknownElement ( ec ) and
683+ ec .getIndex ( ) = key .getValue ( )
684+ )
685+ or
686+ not exists ( key .getValue ( ) ) and
687+ c .isAnyElement ( )
688+ )
689+ or
679690 exists (
680691 CfgNodes:: ExprNodes:: ArrayExprCfgNode arrayExpr , EscapeContainer:: EscapeContainer container
681692 |
@@ -714,13 +725,12 @@ predicate readStep(Node node1, ContentSet c, Node node2) {
714725 node1 .asExpr ( ) = var .getBase ( ) and
715726 e = var .getIndex ( )
716727 |
717- exists ( int index , Content:: KnownElementContent ec |
728+ exists ( Content:: KnownElementContent ec |
718729 c .isKnownOrUnknownElement ( ec ) and
719- index = ec .getIndex ( ) .asInt ( ) and
720- index = e .getValue ( ) .asInt ( )
730+ e .getValue ( ) = ec .getIndex ( )
721731 )
722732 or
723- not exists ( e .getValue ( ) . asInt ( ) ) and
733+ not exists ( e .getValue ( ) ) and
724734 c .isAnyElement ( )
725735 )
726736 or
0 commit comments