Module Wp.MemVar

module type VarUsage = sig ... end
module Raw : VarUsage

VarUsage naive instance. It reports a by-value access for all variables.

module Static : VarUsage

VarUsage that uses only Cil-Static infos.

Create a mixed Hoare Memory Model from VarUsage instance.