Wp.Sigs
Common Types and Signatures
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 holdsIt 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
module type Chunk = sig ... end
Memory Chunks.
module type Sigma = sig ... end
Memory Environments.
module type Model = sig ... end
Memory Models.
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