package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Theory

val t_malloc : Lang.F.tau

allocation tables

val t_init : Lang.F.tau

initialization tables

val t_mem : Lang.F.tau -> Lang.F.tau

t_addr indexed array

val f_havoc : Lang.lfun
val f_set_init : Lang.lfun
val p_is_init_r : Lang.lfun
val p_eqmem : Lang.lfun
val p_monotonic : Lang.lfun
val cinits : Lang.F.term -> Lang.F.pred
val sconst : Lang.F.term -> Lang.F.pred
val framed : Lang.F.term -> Lang.F.pred

Frame Conditions

frames ~addr are frame conditions for reading a value at address addr from a chunk of memory. The value read at addr have length offset, while individual element in memory chunk have type tau and offset length sizeof.

Memory variables use ~basename or "mem" by default.

val frames : addr:Lang.F.term -> offset:Lang.F.term -> sizeof:Lang.F.term -> ?basename:string -> Lang.F.tau -> Sigs.frame list

Unsupported Union Fields

val unsupported_union : Frama_c_kernel.Cil_types.fieldinfo -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct