Frama-C API - `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) (_ : Memory.Model) : Memory.Model

Create a mixed Hoare Memory Model from VarUsage instance.

Frama-C API - MemVar