Module 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 Lang.F.term * Lang.F.term (*

Set(a,b) is a := b.

*)
| Assert of Lang.F.pred

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 Lang.F.term
| Loc of 'a

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

type 'a logic = 
| Vexp of Lang.F.term
| Vloc of 'a
| Vset of 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 Lang.F.var

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).

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

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