Index of types

allocates and frees.

This is the type of the elements of the alpha renaming table.

all kind of annotations

assignment performed by a C function.

zone assigned with its dependencies.

Various classes of attributes

Attributes are lists sorted by the attribute name.

The type of parameters of attributes

Behavior of a function.

assigns can belong either to a contract or a loop annotation

arithmetic and logic binary operators.

Binary operations

This is used to cache the computation of the size of types in bits.

A block is a sequence of statements with the control falling through from one element to the next

Type for a Value builtin function

Some functions of this module may optionally use internal caches.

Results of a a call to a function

Callback for the buttons that can be in the menus.

a call graph is a hashtable, mapping a function name to the node which describes that function's call structure

a call node describes the local calling structure for a single function: which functions it calls, and which functions call it

Value callstacks, as used e.g.

category for debugging/verbose messages.

The created widget is packed in the box.

Internal representation of decorated C functions

all annotations that can be found in the code.

code annotation with an unique identifier.

type of registered code transformations

The definition of a structure or union type.

The configuration data can be of several types *

logic constants.

Literal constants

Type of the referenced value.

global declarations.

C locations.

dependencies of an assigned location.

The type of the set elements.

Type of status emitted by analyzers.

Information about an enumeration.

A datatype to be used in conjunction with existsType

Expressions (Side-effect free)

Additional information on an expression

ACSL extension for external spec file *

some type for a function information

To be able to add/remove features easily, each feature should be package as an interface with the following interface.

The expansible attribute of a field.

Information about a struct/union field.

The top-level representation of a CIL source file (and the result of the parsing and elaboration).

the string is a file name, and then the list of toplevel forms.

Various kinds of floating-point numbers

The type of argument for the interpreter

behavior of a function.

Function definitions.

function contract.

The main type for representing global declarations and definitions.

global annotations, not attached to a statement or a function.

For if statements

For if statements

How to journalize the given function.

Only AAssert, AInvariant, or APragma.

code_annotation is None for decreases and Some { AVariant } for loop variant.

predicate with an unique identifier.

None, Kglobal --> global property None, Some kf --> impossible Some kf, Kglobal --> property of a function without code Some kf, Kstmt stmt --> reachability of the given stmt (and the attached properties)

tsets with an unique identifier.

Various kinds of integers

Pragmas for the impact plugin of Frama-C.

Initializers for global variables.

We want to be able to update an initializer in a global variable, so we define it as a mutable field

Instructions.

Except field fundec, do not use the other fields directly.

The type of the map keys.

The type of the map keys.

Labels

logical expression.

The host part of an Cil_types.lval.

Styles of printing line directives

Styles of printing line directives

local information needed to typecheck expressions and statements

The kind of object that can be selected in the source viewer.

A Location_Bits.t and a size in bits.

Type for source-file locations

Describes a location in a source file

Description of a constructor of a logic sum-type.

Dependencies for the evaluation of a term or a predicate: for each program point involved, sets of zones that must be read

description of a logic function or predicate.

logic label referring to a particular program point.

Real constants.

logic types.

Types of logic terms.

Description of a logic type.

description of a logic variable

origin of a logic variable.

Pragmas for the value analysis plugin of Frama-C.

model field.

model field.

object that can be named (in particular predicates).

The offset part of an Cil_types.lval.

type of the maps associated to a base

An ordered_stmt is an int representing a stmt in a particular function.

As ordered_stmts are contiguous and start from 0, they are suitable for use by index in a array.

Types of conversion tables between stmt and ordered_stmt.

List of possible origins.

Only signed overflows int are really RTEs.

Structural descriptor used inside structures.

Type of the parameter of the functions registered in the hook.

If s is parsed as (n, l, u), then n is the nearest approximation of s with the desired precision.

kind of expression.

who do the job and, for each of them, who find which issues.

Only iterable parameters (see do_iterate and do_not_iterate) are registered in the field p_parameters.

Type of the polymorphic type (for instance 'a list).

The various kinds of pragmas.

Precedences used for generating the minimal number of parenthesis in combination with function Type.par below.

predicates

Does the given predicate hold or not.

Existential (||) or universal (&&) predicates.

Generic type for the various logging channels which are not aborting Frama-C.

some type for the whole project information

Type of a project.

quantifier-bound variables

variables bound by a quantifier.

The type of maps from type key to type value.

Type used for handling (possibly mutually) recursive structural descriptors.

comparison operators.

comparison relations

Type of the result of the functions.

Set of colored selections.

Shape of the set, ie.

Shareable tasks.

Pragmas for the slicing plugin of Frama-C.

specification of a C function.

Function contract.

The different stages, from the first to be executed to the last one.

To call when the source buffer is about to be discarded

Internal state of the value analysis.

Type of known precise status of a property.

Statements.

Storage-class information

Description with details.

Type of the widget containing the warnings.

Static polymorphic type corresponding to its dynamic counterpart to register.

Type of heterogeneous (hash)tables indexed by values of type Key.t.

Type of type values.

Type of internal representations of OCaml type.

Type of a state selection.

Proxy type.

Type of the state to register.

Same constructor than Consolidation.t, without argument.

the type to be serialized

Type of the parameter (an int, a string, etc).

The type of sets.

The type of maps from type key to type 'a.

Type of a type descriptor.

Abtract data type for function slice.

Internal selection.

Abtract data type for mark value.

Abstract data type for slicing project.

PDG type

Internal representation of a value.

Type for this datatype

Values associated to each datatype.

The type of the data we compute for each block start.

The type of the data we compute for each block start.

The type of the data we compute for each block start.

The type of the data we compute for each block start.

type for the return value of many find_xxx functions when the answer can be a list of (node, z_part) and an undef zone.

list of zones at some program points.

Logic terms.

base address of an lvalue.

lvalue: base address and offset.

the various kind of terms.

offset of an lvalue.

kind of termination a post-condition applies to.

type invariant.

Concrete type definition.

Information about a defined type.

Functions that can be called when type-checking an extension of ACSL.

This is the type of the elements that are recorded by the alpha conversion functions in order to be able to undo changes to the tables they modify.

unary operators.

Unary operators

Type of the values stored in the offsetmap

type of the values associated to a location

the real type for the option

variant for loop or recursive function.

variant of a loop or a recursive function.

Information about a variable.

Different visiting actions.

Visitor behavior

An argument of type warn_mode is required by some of the access functions in Db.Value (the interface to the value analysis).

Where to put a new entry.

Bases that must be widening in priority, plus widening hints for each base.

hints for the widening

widening hints for each base