@@ -822,19 +822,23 @@ predicate jumpStep(Node n1, Node n2) {
822
822
* store step can be used to clear a field (see `clearsContent`).
823
823
*/
824
824
predicate storeStepImpl ( Node node1 , Content c , Node node2 , boolean certain ) {
825
- exists ( int indirectionIndex1 , int numberOfLoads , StoreInstruction store |
825
+ exists (
826
+ PostFieldUpdateNode postFieldUpdate , int indirectionIndex1 , int numberOfLoads ,
827
+ StoreInstruction store
828
+ |
829
+ postFieldUpdate = node2 and
826
830
nodeHasInstruction ( node1 , store , pragma [ only_bind_into ] ( indirectionIndex1 ) ) and
827
- node2 . ( PostFieldUpdateNode ) .getIndirectionIndex ( ) = 1 and
828
- numberOfLoadsFromOperand ( node2 . ( PostFieldUpdateNode ) .getFieldAddress ( ) ,
831
+ postFieldUpdate .getIndirectionIndex ( ) = 1 and
832
+ numberOfLoadsFromOperand ( postFieldUpdate .getFieldAddress ( ) ,
829
833
store .getDestinationAddressOperand ( ) , numberOfLoads , certain )
830
834
|
831
835
exists ( FieldContent fc | fc = c |
832
- fc .getField ( ) = node2 . ( PostFieldUpdateNode ) .getUpdatedField ( ) and
836
+ fc .getField ( ) = postFieldUpdate .getUpdatedField ( ) and
833
837
fc .getIndirectionIndex ( ) = 1 + indirectionIndex1 + numberOfLoads
834
838
)
835
839
or
836
840
exists ( UnionContent uc | uc = c |
837
- uc .getAField ( ) = node2 . ( PostFieldUpdateNode ) .getUpdatedField ( ) and
841
+ uc .getAField ( ) = postFieldUpdate .getUpdatedField ( ) and
838
842
uc .getIndirectionIndex ( ) = 1 + indirectionIndex1 + numberOfLoads
839
843
)
840
844
)
0 commit comments