What is the memory model used by Frama-C?
There is not a single memory model. Each plug-in is free to define the hypotheses it needs. The annotation language, ACSL, is as memory-model-agnostic as we were able to make it. Basically, there is one untyped byte array for each “base address”, base addresses being among other things string literals and variables. A weakest precondition plug-in such as Jessie may have a more abstract view of memory, in order to obtain separation hypotheses between pointers of different types for free (at the cost of not handling some kinds of pointer casts). More precisely, the “default” memory model in Jessie is typed, which allows to assume separation properties which are handy in general, but does not allow pointer casts. When pointer casts occurs, it tries to switch to a more complicated memory model. More details can be found in http://www.lri.fr/~marche/moy09phd.pdf.
