Module Wp.Sigs

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
| 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 = [
| `Positive
| `Negative
| `NoPolarity
]

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

and s_host =
| Mvar of Frama_c_kernel.Cil_types.varinfo(*

Variable

*)
| Mmem of Lang.F.term(*

Pointed value

*)
| Mval of s_lval(*

Pointed value of another abstract left-value

*)
and s_offset =
| Mfield of Frama_c_kernel.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