Number and repetition of properties

[rod-chapman]

This example:

https://github.com/rod-chapman/cbmc-examples/tree/main/arrays

doing “make TARGET=assign_st1”

generates 303 properties for just 8 lines of code!

There seems to a lot of repetition on those
  Checking that pointers are not NULL over and over again
  Checking that dst[0] is valid
  and so on...

While most of these properties are trivial in isolation, I am concerned that the sheer number of them is leading to explosion on the SAT engine inside Z3.  Reducing the repetion might have a big impact on overall performance.

1. Why does this repetition exist in the first place? Is it really necessary?
2. Can some/all of the repetition be removed?

[remi-delmas-3000]

Hi, contract instrumentation, dynamic frames in particular, adds ghost code that allocates ghost storage, takes snapshots of memory locations, computes if memory accesses performed by the program are in range of the assigns clause targets, all of that ghost code uses pointer arithmetic, bit vector arithmetic, and essentially has C semantics (see cprover_contracts.c library for details), the instrumentation only produces sound results if it is itself proved to be free of pointer and arithmetic errors. Given the limits of CBMC’s memory model in terms of max number of objects, maximum offsets, etc. we cannot prove the support library is UB-free once and for all, these POs have to be discharged per use.

[rod-chapman]

So.. in the simple example I cited above, the single line of code

dst[0] = src[0];

generates 31 properties. What "instrumentation" is even required here? (I can see 6 things that need to verified, not 31...). The next line of code:

dst[1] = src[1];

generates another 31 properties, and so on...