module Sigs:sig
..end
Common Types and Signatures
type 'a
sequence = {
|
pre : |
|
post : |
type 'a
binder = {
|
bind : |
type
equation =
| |
Set of |
(* |
| *) |
| |
Assert of |
Oriented equality or arbitrary relation
type
acs =
| |
RW |
(* | Read-Write Access | *) |
| |
RD |
(* | Read-Only Access | *) |
| |
OBJ |
(* | Valid Object Pointer | *) |
Access conditions
type 'a
value =
| |
Val of |
| |
Loc of |
Abstract location or concrete value
type 'a
rloc =
| |
Rloc of |
| |
Rrange of |
Contiguous set of locations
type 'a
sloc =
| |
Sloc of |
|||
| |
Sarray of |
(* | full sized range (optimized assigns) | *) |
| |
Srange of |
|||
| |
Sdescr of |
Structured set of locations
type'a
region =(Ctypes.c_object * 'a sloc) list
Typed set of locations
type 'a
logic =
| |
Vexp of |
| |
Vloc of |
| |
Vset of |
| |
Lset of |
Logical values, locations, or sets of
type
scope =
| |
Enter |
| |
Leave |
Scope management for locals and formals
type 'a
result =
| |
R_loc of |
| |
R_var of |
Container for the returned value of a function
typepolarity =
[ `Negative | `NoPolarity | `Positive ]
Polarity of predicate compilation
typeframe =
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.
types_lval =
s_host * s_offset list
Reversed ACSL left-value
type
s_host =
| |
Mvar of |
(* | Variable | *) |
| |
Mmem of |
(* | Pointed value | *) |
| |
Mval of |
(* | Pointed value of another abstract left-value | *) |
type
s_offset =
| |
Mfield of |
| |
Mindex of |
type
mval =
| |
Mterm |
(* | Not a state-related value | *) |
| |
Maddr of |
(* | The value is the address of an l-value in current memory | *) |
| |
Mlval of |
(* | The value is the value of an l-value in current memory | *) |
| |
Mchunk of |
(* | The value is an abstract memory chunk (description) | *) |
Reversed abstract value
type
update =
| |
Mstore of |
(* | 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