@@ -660,10 +660,9 @@ predicate storeStep(Node node1, ContentSet c, Node node2) {
660
660
node1 .asStmt ( ) = var .getAssignStmt ( ) .getRightHandSide ( ) and
661
661
e = var .getIndex ( )
662
662
|
663
- exists ( int index , Content:: KnownElementContent ec |
663
+ exists ( Content:: KnownElementContent ec |
664
664
c .isKnownOrUnknownElement ( ec ) and
665
- index = ec .getIndex ( ) .asInt ( ) and
666
- index = e .getValue ( ) .asInt ( )
665
+ e .getValue ( ) = ec .getIndex ( )
667
666
)
668
667
or
669
668
not exists ( e .getValue ( ) .asInt ( ) ) and
@@ -676,6 +675,18 @@ predicate storeStep(Node node1, ContentSet c, Node node2) {
676
675
index = ec .getIndex ( ) .asInt ( )
677
676
)
678
677
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
679
690
exists (
680
691
CfgNodes:: ExprNodes:: ArrayExprCfgNode arrayExpr , EscapeContainer:: EscapeContainer container
681
692
|
@@ -714,13 +725,12 @@ predicate readStep(Node node1, ContentSet c, Node node2) {
714
725
node1 .asExpr ( ) = var .getBase ( ) and
715
726
e = var .getIndex ( )
716
727
|
717
- exists ( int index , Content:: KnownElementContent ec |
728
+ exists ( Content:: KnownElementContent ec |
718
729
c .isKnownOrUnknownElement ( ec ) and
719
- index = ec .getIndex ( ) .asInt ( ) and
720
- index = e .getValue ( ) .asInt ( )
730
+ e .getValue ( ) = ec .getIndex ( )
721
731
)
722
732
or
723
- not exists ( e .getValue ( ) . asInt ( ) ) and
733
+ not exists ( e .getValue ( ) ) and
724
734
c .isAnyElement ( )
725
735
)
726
736
or
0 commit comments