Frama-C API - Sigs
Common Types and Signatures
General Definitions
Oriented equality or arbitrary relation
Access conditions
Abstract location or concrete value
type 'a rloc =
| Rloc of Ctypes.c_object * 'a
| Rrange of 'a * Ctypes.c_object * Lang.F.term option * Lang.F.term option
Contiguous set of locations
type 'a sloc =
| Sloc of 'a
| Sarray of 'a * Ctypes.c_object * int
(*full sized range (optimized assigns)
*)| Srange of 'a * Ctypes.c_object * Lang.F.term option * Lang.F.term option
| Sdescr of Lang.F.var list * 'a * Lang.F.pred
Structured set of locations
type 'a region = (Ctypes.c_object * 'a sloc) list
Typed set of locations
Logical values, locations, or sets of
Container for the returned value of a function
type frame = string * Definitions.trigger list * Lang.F.pred list * Lang.F.term * Lang.F.term
Frame Conditions. Consider a function phi(m)
over memory m
, we want memories m1,m2
and condition p
such that p(m1,m2) -> phi(m1) = phi(m2)
.
name
used for generating lemmatriggers
for the lemmaconditions
for the frame lemma to holdmem1,mem2
to two memories for which the lemma holds
Reversing Models
It is sometimes possible to reverse memory models abstractions into ACSL left-values via the definitions below.
and s_host =
| Mvar of Frama_c_kernel.Cil_types.varinfo
(*Variable
*)| Mmem of Lang.F.term
(*Pointed value
*)| Mval of s_lval
(*Pointed value of another abstract left-value
*)
type mval =
| Mterm
(*Not a state-related value
*)| Maddr of s_lval
(*The value is the address of an l-value in current memory
*)| Mlval of s_lval * Lang.datakind
(*The value is the value of an l-value in current memory
*)| Mchunk of string * Lang.datakind
(*The value is an abstract memory chunk (description)
*)
Reversed abstract value
type update =
| Mstore of s_lval * Lang.F.term
(*An update of the ACSL left-value with the given value
*)
Reversed update
Memory Models
module type Type = sig ... end
module type Chunk = sig ... end
Memory Chunks.
module type Sigma = sig ... end
Memory Environments.
module type Model = sig ... end
Memory Models.
C and ACSL Compilers
module type CodeSemantics = sig ... end
Compiler for C expressions
module type LogicSemantics = sig ... end
Compiler for ACSL expressions
module type LogicAssigns = sig ... end
Compiler for Performing Assigns
module type Compiler = sig ... end
All Compilers Together