Module Wp.Sigs

module Sigs: sig .. end

Common Types and Signatures

General Definitions

type 'a sequence = {
   pre : 'a;
   post : 'a;
}
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

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