Frama-C:
Plug-ins:
Libraries:

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.

Create a mixed Hoare Memory Model from VarUsage instance.