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.
module Make (_ : VarUsage) (_ : Sigs.Model) : Sigs.Model
Create a mixed Hoare Memory Model from VarUsage instance.