Functor LogicAssigns.Make

module Make: 
functor (M : Sigs.Model-> 
functor (L : Sigs.LogicSemantics with module M = M-> Sigs.LogicAssigns with module M = M and module L = L
Parameters:
M : Sigs.Model
L : Sigs.LogicSemantics with module M = M

module M: Sigs.Model 
module L: Sigs.LogicSemantics  with module M = M
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.