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-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

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

Module `Wp.Memory`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

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 =

| 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
*)
| Minit of s_lval
(*
The value is the init state of an l-value in current memory
*)
| Mchunk of Sigma.Chunk.t
(*
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 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