@@ -325,6 +325,19 @@ private predicate fieldReadStep(Node node1, FieldContent f, Node node2) {
325325 )
326326}
327327
328+ /**
329+ * When a store step happens in a function that looks like an array write such as:
330+ * ```cpp
331+ * void f(int* pa) {
332+ * pa = source();
333+ * }
334+ * ```
335+ * it can be a write to an array, but it can also happen that `f` is called as `f(&a.x)`. If that is
336+ * the case, the `ArrayContent` that was written by the call to `f` should be popped off the access
337+ * path, and a `FieldContent` containing `x` should be pushed instead.
338+ * So this case pops `ArrayContent` off the access path, and the `fieldStoreStepAfterArraySuppression`
339+ * predicate in `storeStep` ensures that we push the right `FieldContent` onto the access path.
340+ */
328341predicate suppressArrayRead ( Node node1 , ArrayContent a , Node node2 ) {
329342 a = TArrayContent ( ) and
330343 exists ( BufferMayWriteSideEffectInstruction write , ChiInstruction chi |
@@ -383,17 +396,6 @@ private predicate arrayReadStep(Node node1, ArrayContent a, Node node2) {
383396predicate readStep ( Node node1 , Content f , Node node2 ) {
384397 fieldReadStep ( node1 , f , node2 ) or
385398 arrayReadStep ( node1 , f , node2 ) or
386- // When a store step happens in a function that looks like an array write such as:
387- // ```cpp
388- // void f(int* pa) {
389- // *pa = source();
390- // }
391- // ```
392- // it can be a write to an array, but it can also happen that `f` is called as `f(&a.x)`. If that is
393- // the case, the `ArrayContent` that was written by the call to `f` should be popped off the access
394- // path, and a `FieldContent` containing `x` should be pushed instead.
395- // So this case pops `ArrayContent` off the access path, and the `fieldStoreStepAfterArraySuppression`
396- // predicate in `storeStep` ensures that we push the right `FieldContent` onto the access path.
397399 suppressArrayRead ( node1 , f , node2 )
398400}
399401
0 commit comments