module type LogicAssigns =sig
..end
module M:Wp.Sigs.Model
module L:Wp.Sigs.LogicSemantics
with module M = M
val domain : M.loc Wp.Sigs.region -> M.Heap.set
val apply_assigns : M.sigma Wp.Sigs.sequence -> M.loc Wp.Sigs.region -> Wp.Lang.F.pred list