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 | *) |
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
It 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