@@ -873,23 +873,16 @@ predicate jumpStep(Node n1, Node n2) {
873873predicate storeStepImpl ( Node node1 , Content c , Node node2 , boolean certain ) {
874874 exists (
875875 PostFieldUpdateNode postFieldUpdate , int indirectionIndex1 , int numberOfLoads ,
876- StoreInstruction store
876+ StoreInstruction store , FieldContent fc
877877 |
878878 postFieldUpdate = node2 and
879+ fc = c and
879880 nodeHasInstruction ( node1 , store , pragma [ only_bind_into ] ( indirectionIndex1 ) ) and
880881 postFieldUpdate .getIndirectionIndex ( ) = 1 and
881882 numberOfLoadsFromOperand ( postFieldUpdate .getFieldAddress ( ) ,
882- store .getDestinationAddressOperand ( ) , numberOfLoads , certain )
883- |
884- exists ( FieldContent fc | fc = c |
885- fc .getField ( ) = postFieldUpdate .getUpdatedField ( ) and
886- fc .getIndirectionIndex ( ) = 1 + indirectionIndex1 + numberOfLoads
887- )
888- or
889- exists ( UnionContent uc | uc = c |
890- uc .getAField ( ) = postFieldUpdate .getUpdatedField ( ) and
891- uc .getIndirectionIndex ( ) = 1 + indirectionIndex1 + numberOfLoads
892- )
883+ store .getDestinationAddressOperand ( ) , numberOfLoads , certain ) and
884+ fc .getAField ( ) = postFieldUpdate .getUpdatedField ( ) and
885+ fc .getIndirectionIndex ( ) = 1 + indirectionIndex1 + numberOfLoads
893886 )
894887 or
895888 // models-as-data summarized flow
@@ -965,22 +958,17 @@ predicate nodeHasInstruction(Node node, Instruction instr, int indirectionIndex)
965958 * `node2`.
966959 */
967960predicate readStep ( Node node1 , ContentSet c , Node node2 ) {
968- exists ( FieldAddress fa1 , Operand operand , int numberOfLoads , int indirectionIndex2 |
961+ exists (
962+ FieldAddress fa1 , Operand operand , int numberOfLoads , int indirectionIndex2 , FieldContent fc
963+ |
964+ fc = c and
969965 nodeHasOperand ( node2 , operand , indirectionIndex2 ) and
970966 // The `1` here matches the `node2.getIndirectionIndex() = 1` conjunct
971967 // in `storeStep`.
972968 nodeHasOperand ( node1 , fa1 .getObjectAddressOperand ( ) , 1 ) and
973- numberOfLoadsFromOperand ( fa1 , operand , numberOfLoads , _)
974- |
975- exists ( FieldContent fc | fc = c |
976- fc .getField ( ) = fa1 .getField ( ) and
977- fc .getIndirectionIndex ( ) = indirectionIndex2 + numberOfLoads
978- )
979- or
980- exists ( UnionContent uc | uc = c |
981- uc .getAField ( ) = fa1 .getField ( ) and
982- uc .getIndirectionIndex ( ) = indirectionIndex2 + numberOfLoads
983- )
969+ numberOfLoadsFromOperand ( fa1 , operand , numberOfLoads , _) and
970+ fc .getAField ( ) = fa1 .getField ( ) and
971+ fc .getIndirectionIndex ( ) = indirectionIndex2 + numberOfLoads
984972 )
985973 or
986974 // models-as-data summarized flow
0 commit comments