Functor LogicAssigns.Make

module Make: 
functor (M : Memory.Model) -> 
functor (C : Code  with type loc = M.loc) -> 
functor (L : Logic  with type loc = M.loc) -> sig .. end

module Hmap: M.Heap.Map

module Dom: M.Heap.Set

type region = (Ctypes.c_object * M.loc Memory.sloc list) list 

val vars : region -> Lang.F.Vars.t

val dsloc : Ctypes.c_object -> M.loc Memory.sloc -> M.Heap.set

val domain : region -> Dom.t

val assigned_seq : Lang.F.pred Bag.t ->
       M.sigma Memory.sequence ->
       (Ctypes.c_object * M.loc Memory.sloc) list -> Lang.F.pred Bag.t

val assigned : M.sigma Memory.sequence -> region -> Lang.F.pred list