module Sigs: sig
.. end
Common Types and Signatures
General Definitions
type 'a
sequence = {
}
type 'a
binder = {
|
bind : 'b 'c. 'a -> ('b -> 'c) -> 'b -> 'c ; |
}
type
equation =
Oriented equality or arbitrary relation
type
acs =
Access conditions
type 'a
value =
Abstract location or concrete value
type 'a
rloc =
Contiguous set of locations
type 'a
sloc =
Structured set of locations
type 'a
region = (Ctypes.c_object * 'a sloc) list
Typed set of locations
type 'a
logic =
Logical values, locations, or sets of
type
scope =
Scope management for locals and formals
type 'a
result =
Container for the returned value of a function
type
polarity = [ `Negative | `NoPolarity | `Positive ]
Polarity of predicate compilation
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 lemma
triggers
for the lemma
conditions
for the frame lemma to hold
mem1,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.
type
s_lval = s_host * s_offset list
Reversed ACSL left-value
type
s_host =
type
s_offset =
type
mval =
| |
Mterm |
| |
Maddr of s_lval |
| |
Mlval of s_lval |
| |
Mchunk of string |
Reversed abstract value
type
update =
Reversed update
Memory Models
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