Breaking change: Disallow reading from uninitialized arrays

[bart....@cs.kuleuven.be]

Dear all,

I just pushed the first of a series of breaking changes to VeriFast with the goal of making VeriFast sound with respect to the fact that C is not just syntactic sugar for assembly language: C compilers perform optimizations justified by a view of C as a high-level (i.e. Java-like as opposed to assembly-like) programming language. The main aspects of this are:

- It is not sound to treat uninitialized memory as if it was regular memory with some unspecified but valid and stable value. See e.g. https://www.ralfj.de/blog/2019/07/14/uninit.html and https://godbolt.org/z/dYq1Gc9G4 .

- Pointers are not just addresses: compilers are allowed to assume that pointers derived from distinct allocations are distinct, even if they happen to point to the same address in memory. This is known as pointer provenance.

- It might not be sound to assume that struct padding bytes preserve their value or otherwise behave like regular bytes.

- In the absence of the -fno-strict-aliasing flag, compilers are allowed to assume that pointers of different types do not alias. This is known as effective types.

These changes will unfortunately make VeriFast a bit harder to use and harder to teach. If you are impacted by this, do reach out so that we can see how we can make this as painless as possible. We can for example investigate providing options (similar to -disable_overflow_check) that trade off soundness for verification convenience. At first glance, for the current change this does not seem to be necessary but let me know if you do feel a need for this.

Best,

Bart