package frama-c

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

Theory

val t_addr : Lang.F.tau
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 a_null : Lang.F.term

Null address. Same as a_addr 0 0

val a_global : Lang.F.term -> Lang.F.term

Zero-offset base. Same as a_addr base 0

Constructor for { base ; offset }

val a_shift : Lang.F.term -> Lang.F.term -> Lang.F.term

Shift: a_shift a k adds k to a.offset

val a_base : Lang.F.term -> Lang.F.term

Returns the base

val a_offset : Lang.F.term -> Lang.F.term

Returns the offset

val a_base_offset : Lang.F.term -> Lang.F.term -> Lang.F.term

Returns the offset in bytes from the logic offset (which is a memory cell index, actually)

val f_null : Lang.lfun
val f_base : Lang.lfun
val f_global : Lang.lfun
val f_shift : Lang.lfun
val f_offset : Lang.lfun
val f_havoc : Lang.lfun
val f_set_init : Lang.lfun
val f_region : Lang.lfun
val f_addr_of_int : Lang.lfun

Physical address

val f_int_of_addr : Lang.lfun

Physical address

val p_addr_lt : Lang.lfun
val p_addr_le : Lang.lfun
val p_linked : Lang.lfun
val p_framed : Lang.lfun
val p_sconst : Lang.lfun
val p_cinits : Lang.lfun
val p_is_init_r : Lang.lfun
val p_separated : Lang.lfun
val p_included : Lang.lfun
val p_valid_rd : Lang.lfun
val p_valid_rw : Lang.lfun
val p_valid_obj : Lang.lfun
val p_invalid : Lang.lfun
val p_eqmem : Lang.lfun
val p_monotonic : Lang.lfun

Addr Producer Registration

Register simplifiers for functions producing addr terms:

  • ~base es is the simplifier for (f es).base
  • ~offset es is the simplifier for (f es).offset
  • ~linear:true register simplifier f(f(p,i),k)=f(p,i+j) on f
  • ~equal a b is the set_eq_builtin for f

The equality builtin is wrapped inside a default builtin that compares f es by computing base and offset.

val register : ?base:(Lang.F.term list -> Lang.F.term) -> ?offset:(Lang.F.term list -> Lang.F.term) -> ?equal:(Lang.F.term -> Lang.F.term -> Lang.F.pred) -> ?linear:bool -> Lang.lfun -> unit

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

Range of Address

val separated : shift:('a -> Ctypes.c_object -> Lang.F.term -> 'a) -> addrof:('a -> Lang.F.term) -> sizeof:(Ctypes.c_object -> Lang.F.term) -> 'a Sigs.rloc -> 'a Sigs.rloc -> Lang.F.pred
val included : shift:('a -> Ctypes.c_object -> Lang.F.term -> 'a) -> addrof:('a -> Lang.F.term) -> sizeof:(Ctypes.c_object -> Lang.F.term) -> 'a Sigs.rloc -> 'a Sigs.rloc -> Lang.F.pred
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