package frama-c

  1. Overview
  2. Docs

doc/frama-c-wp.core/Wp/MemVar/index.html

Module Wp.MemVarSource

Sourcemodule type VarUsage = sig ... end

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

VarUsage that uses only Cil-Static infos.

Create a mixed Hoare Memory Model from VarUsage instance.

OCaml

Innovation. Community. Security.