LogicAssigns.Make
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.