@@ -500,19 +500,22 @@ predicate jumpStep(Node pred, Node succ) {
500
500
}
501
501
502
502
predicate storeStep ( Node node1 , ContentSet c , Node node2 ) {
503
+ // assignment to a member variable `obj.member = value`
503
504
exists ( MemberRefExpr ref , AssignExpr assign |
504
505
ref = assign .getDest ( ) and
505
506
node1 .asExpr ( ) = assign .getSource ( ) and
506
507
node2 .( PostUpdateNode ) .getPreUpdateNode ( ) .asExpr ( ) = ref .getBase ( ) and
507
508
c .isSingleton ( any ( Content:: FieldContent ct | ct .getField ( ) = ref .getMember ( ) ) )
508
509
)
509
510
or
511
+ // creation of a tuple `(v1, v2)`
510
512
exists ( TupleExpr tuple , int pos |
511
513
node1 .asExpr ( ) = tuple .getElement ( pos ) and
512
514
node2 .asExpr ( ) = tuple and
513
515
c .isSingleton ( any ( Content:: TupleContent ct | ct .getIndex ( ) = pos ) )
514
516
)
515
517
or
518
+ // assignment to a tuple member `tuple.index = value`
516
519
exists ( TupleElementExpr tuple , AssignExpr assign |
517
520
tuple = assign .getDest ( ) and
518
521
node1 .asExpr ( ) = assign .getSource ( ) and
@@ -526,13 +529,15 @@ predicate storeStep(Node node1, ContentSet c, Node node2) {
526
529
predicate isLValue ( Expr e ) { any ( AssignExpr assign ) .getDest ( ) = e }
527
530
528
531
predicate readStep ( Node node1 , ContentSet c , Node node2 ) {
532
+ // read of a member variable `obj.member`
529
533
exists ( MemberRefExpr ref |
530
534
not isLValue ( ref ) and
531
535
node1 .asExpr ( ) = ref .getBase ( ) and
532
536
node2 .asExpr ( ) = ref and
533
537
c .isSingleton ( any ( Content:: FieldContent ct | ct .getField ( ) = ref .getMember ( ) ) )
534
538
)
535
539
or
540
+ // read of a tuple member `tuple.index`
536
541
exists ( TupleElementExpr tuple |
537
542
node1 .asExpr ( ) = tuple .getSubExpr ( ) and
538
543
node2 .asExpr ( ) = tuple and
0 commit comments