@@ -188,16 +188,29 @@ module ControlFlow {
188188 * initialized.
189189 */
190190 predicate writesElement ( DataFlow:: Node base , DataFlow:: Node index , DataFlow:: Node rhs ) {
191- exists ( DataFlow:: Node b |
192- this .writesElementInsn ( b .asInstruction ( ) , index .asInstruction ( ) , rhs .asInstruction ( ) )
193- |
191+ exists ( DataFlow:: Node b | this .writesElementPreUpdate ( b , index , rhs ) |
194192 this .isInitialization ( ) and base = b
195193 or
196194 not this .isInitialization ( ) and
197195 b = base .( DataFlow:: PostUpdateNode ) .getPreUpdateNode ( )
198196 )
199197 }
200198
199+ /**
200+ * Holds if this node sets the value of element `index` on `base` (or its implicit dereference)
201+ * to `rhs`.
202+ *
203+ * For example, for the assignment `xs[i] = v`, `base` is the post-update node of the data-flow
204+ * node corresponding to `xs` or (if `xs` is a pointer) the implicit dereference `*xs`, `index`
205+ * is the data-flow node corresponding to `i`, and `rhs` is the data-flow node corresponding to
206+ * `base`. If this `WriteNode` corresponds to the initialization of an array/slice/map then
207+ * there is no need for a post-update node and `base` is the array/slice/map literal being
208+ * initialized.
209+ */
210+ predicate writesElementPreUpdate ( DataFlow:: Node base , DataFlow:: Node index , DataFlow:: Node rhs ) {
211+ this .writesElementInsn ( base .asInstruction ( ) , index .asInstruction ( ) , rhs .asInstruction ( ) )
212+ }
213+
201214 private predicate writesElementInsn (
202215 IR:: Instruction base , IR:: Instruction index , IR:: Instruction rhs
203216 ) {
0 commit comments