Module Wp.Sigs

module Sigs: sig .. end


Common Types and Signatures

General Definitions


type 'a sequence = {
   pre : 'a;
   post : 'a;
}
type 'a binder = {
   bind : 'b 'c. 'a -> ('b -> 'c) -> 'b -> 'c;
}
type equation = 
| Set of Wp.Lang.F.term * Wp.Lang.F.term (*
Set(a,b) is a := b.
*)
| Assert of Wp.Lang.F.pred
Oriented equality or arbitrary relation
type acs = 
| RW (*
Read-Write Access
*)
| RD (*
Read-Only Access
*)
Access conditions
type 'a value = 
| Val of Wp.Lang.F.term
| Loc of 'a
Abstract location or concrete value
type 'a rloc = 
| Rloc of Wp.Ctypes.c_object * 'a
| Rrange of 'a * Wp.Ctypes.c_object * Wp.Lang.F.term option * Wp.Lang.F.term option
Contiguous set of locations
type 'a sloc = 
| Sloc of 'a
| Sarray of 'a * Wp.Ctypes.c_object * int (*
full sized range (optimized assigns)
*)
| Srange of 'a * Wp.Ctypes.c_object * Wp.Lang.F.term option * Wp.Lang.F.term option
| Sdescr of Wp.Lang.F.var list * 'a * Wp.Lang.F.pred
Structured set of locations
type 'a region = (Wp.Ctypes.c_object * 'a sloc) list 
Typed set of locations
type 'a logic = 
| Vexp of Wp.Lang.F.term
| Vloc of 'a
| Vset of Wp.Vset.set
| Lset of 'a sloc list
Logical values, locations, or sets of
type scope = 
| Enter
| Leave
Scope management for locals and formals
type 'a result = 
| R_loc of 'a
| R_var of Wp.Lang.F.var
Container for the returned value of a function
type polarity = [ `Negative | `NoPolarity | `Positive ] 
Polarity of predicate compilation
type frame = string * Wp.Definitions.trigger list * Wp.Lang.F.pred list * Wp.Lang.F.term *
Wp.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).

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 = 
| Mvar of Cil_types.varinfo (*
Variable
*)
| Mmem of Wp.Lang.F.term (*
Pointed value
*)
| Mval of s_lval (*
Pointed value of another abstract left-value
*)
type s_offset = 
| Mfield of Cil_types.fieldinfo
| Mindex of Wp.Lang.F.term
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 (*
The value is the value of an l-value in current memory
*)
| Mchunk of string (*
The value is an abstract memory chunk (description)
*)
Reversed abstract value
type update = 
| Mstore of s_lval * Wp.Lang.F.term (*
An update of the ACSL left-value with the given value
*)
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