@@ -134,31 +134,42 @@ module ControlFlow {
134134
135135 /**
136136 * Holds if this node sets the value of field `f` on `base` (or its implicit dereference) to
137- * `rhs`.
137+ * `rhs`, where `base` represents the post-update value .
138138 *
139139 * For example, for the assignment `x.width = newWidth`, `base` is the post-update node of
140140 * either the data-flow node corresponding to `x` or (if `x` is a pointer) the data-flow node
141141 * corresponding to the implicit dereference `*x`, `f` is the field referenced by `width`, and
142142 * `rhs` is the data-flow node corresponding to `newWidth`. If this `WriteNode` is a struct
143- * initialization then there is no need for a post-update node and `base` is the struct literal
144- * being initialized.
143+ * initialization then there is no post-update node and `base` is the struct literal being
144+ * initialized.
145145 */
146146 predicate writesField ( DataFlow:: Node base , Field f , DataFlow:: Node rhs ) {
147- exists ( DataFlow:: Node b | this .writesFieldInsn ( b . asInstruction ( ) , f , rhs . asInstruction ( ) ) |
147+ exists ( DataFlow:: Node b | this .writesFieldPreUpdate ( b , f , rhs ) |
148148 this .isInitialization ( ) and base = b
149149 or
150150 not this .isInitialization ( ) and
151151 b = base .( DataFlow:: PostUpdateNode ) .getPreUpdateNode ( )
152152 )
153153 }
154154
155+ /**
156+ * Holds if this node sets the value of field `f` on `base` (or its implicit dereference) to
157+ * `rhs`, where `base` represents the pre-update value.
158+ *
159+ * For example, for the assignment `x.width = newWidth`, `base` is either the data-flow node
160+ * corresponding to `x` or (if `x` is a pointer) the data-flow node corresponding to the
161+ * implicit dereference `*x`, `f` is the field referenced by `width`, and `rhs` is the
162+ * data-flow node corresponding to `newWidth`.
163+ */
164+ predicate writesFieldPreUpdate ( DataFlow:: Node base , Field f , DataFlow:: Node rhs ) {
165+ this .writesFieldInsn ( base .asInstruction ( ) , f , rhs .asInstruction ( ) )
166+ }
167+
155168 /**
156169 * Holds if this node sets the value of field `f` on `v` to `rhs`.
157170 */
158171 predicate writesFieldOnSsaWithFields ( SsaWithFields v , Field f , DataFlow:: Node rhs ) {
159- exists ( IR:: Instruction insn | this .writesFieldInsn ( insn , f , rhs .asInstruction ( ) ) |
160- v .getAUse ( ) .asInstruction ( ) = insn
161- )
172+ this .writesFieldPreUpdate ( v .getAUse ( ) , f , rhs )
162173 }
163174
164175 private predicate writesFieldInsn ( IR:: Instruction base , Field f , IR:: Instruction rhs ) {
0 commit comments