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