Expand description
Transformation which injects well-formed assumptions at top-level entry points of verified functions. These assumptions are both about parameters and any memory referred to by the code. For ghost memory, the transformation also assumes initial values if provided.
This needs to be run after function specifications and global invariants have been injected because only then we know all accessed memory.
This phase need to be run before data invariant instrumentation, because the latter relies on the well-formed assumptions, augmenting them with the data invariant. Because data invariants cannot refer to global memory, they are not relevant for memory usage, and their injection therefore can happen after this phase.