package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-wp.core/Wp/Sigs/index.html

Module `Wp.Sigs`Source

Common Types and Signatures

General Definitions

Sourcetype 'a sequence = {

pre : 'a;
post : 'a;

}

Sourcetype 'a binder = {

bind : 'b 'c. 'a -> ('b -> 'c) -> 'b -> 'c;

}

Sourcetype 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

Sourcetype acs =

| RW
(*
Read-Write Access
*)
| RD
(*
Read-Only Access
*)
| OBJ
(*
Valid Object Pointer
*)

Access conditions

Sourcetype 'a value =

| Val of Lang.F.term
| Loc of 'a

Abstract location or concrete value

Sourcetype '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

Sourcetype '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

Sourcetype 'a region = (Ctypes.c_object * 'a sloc) list

Typed set of locations

Sourcetype 'a logic =

| Vexp of Lang.F.term
| Vloc of 'a
| Vset of Wp__.Vset.vset list
| Lset of 'a sloc list

Logical values, locations, or sets of

Sourcetype scope =

| Enter
| Leave

Scope management for locals and formals

Sourcetype 'a result =

| R_loc of 'a
| R_var of Lang.F.var

Container for the returned value of a function

Sourcetype polarity = [

| `Positive
| `Negative
| `NoPolarity

]

Polarity of predicate compilation

Source

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.

Sourcetype s_lval = s_host * s_offset list

Reversed ACSL left-value

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

Sourceand s_offset =

| Mfield of Frama_c_kernel.Cil_types.fieldinfo
| Mindex of Lang.F.term

Sourcetype 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

Sourcetype update =

| Mstore of s_lval * Lang.F.term
(*
An update of the ACSL left-value with the given value
*)

Reversed update

Memory Models

Sourcemodule type Chunk = sig ... end

Memory Chunks.

Sourcemodule type Sigma = sig ... end

Memory Environments.

Sourcemodule type Model = sig ... end

Memory Models.

C and ACSL Compilers

Sourcemodule type CodeSemantics = sig ... end

Compiler for C expressions

Sourcemodule type LogicSemantics = sig ... end

Compiler for ACSL expressions

Sourcemodule type LogicAssigns = sig ... end

Compiler for Performing Assigns

Sourcemodule type Compiler = sig ... end

All Compilers Together

On This Page

General Definitions
Reversing Models
Memory Models
C and ACSL Compilers