Axioms to maintain constant sections of memory

[l-kent]

Our current approach to modelling initialised memory is inadequate, and this causes issues for some tests (specifically some of the gcc_pic tests). Currently, we add the initial values for the .data, .rodata and .got sections of the binary (because those have proven relevant so far) to the precondition of the main procedure, which allows pointers stored in the global offset table to be loaded, for instance. This approach works for accesses within main, but these preconditions are not added to other procedures (so obviously do not work for those procedures), and calls to rely() mean that these parts of memory are havoced away if there are rely conditions specified, as we do not adequately preserve all of memory. The issue with rely calls is something the memory region analysis (#63) should help with, by splitting the memory into discrete regions, but may not entirely solve.

We likely want to perform some analysis to detect initialised memory locations that are read but not written to, and add Boogie axioms so that these memory accesses are constant across all procedures. We could just assume for the time being that the global offset table pointers detailed in the '.rela,dyn' section section are going to be constant (as these are the most important constants in the initialised memory), without actually checking, but a more sophisticated approach could be helpful more broadly in the future.

[l-kent]

Out of the sections we use, only .rodata is guaranteed to be read-only, but we still want some way to determine if any parts of the others are constant in practice.