Frama-C:
Plug-ins:
Libraries:

Frama-C API - A

module M = M
module L = L
val domain : M.loc region -> Sigma.Heap.set

Memory footprint of a region.

val apply_assigns : Sigma.sigma sequence -> M.loc region -> Lang.F.pred list

Relates two memory states corresponding to an assigns clause with the specified set of locations.