Frama-C API - Make
Parameters
module M : Sigs.Model
module L : Sigs.LogicSemantics with module M = M
Signature
module M = M
module L = L
val domain : M.loc Sigs.region -> M.Heap.set
Memory footprint of a region.
val apply_assigns : M.sigma Sigs.sequence -> M.loc Sigs.region -> Lang.F.pred list
Relates two memory states corresponding to an assigns clause with the specified set of locations.