Frama-C API - `Make`

Parameters

module M : Memory.Model

module L : Memory.LogicSemantics with module M = M

module M = M

module L = L

val domain : M.loc Memory.region -> Sigma.Heap.set

Memory footprint of a region.

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

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