Make (frama-c-wp.Wp.LogicAssigns.Make)

Parameters

module M : Sigs.Model

module L : Sigs.LogicSemantics with module M = M

module M = M

module L = L

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.