Module Wp.Sigs.Compiler.A

module A: Wp.Sigs.LogicAssigns  with module M = M and module L = L

module M: Wp.Sigs.Model 
module L: Wp.Sigs.LogicSemantics  with module M = M
val domain : M.loc Wp.Sigs.region -> M.Heap.set

Memory footprint of a region.

val apply_assigns : M.sigma Wp.Sigs.sequence -> M.loc Wp.Sigs.region -> Wp.Lang.F.pred list

Relates two memory states corresponding to an assigns clause with the specified set of locations.