Index of types

Type explaining how to manipulate the elements of the category.

Button for dialog options

true indicates that an alarm may have occurred

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.

type for functions adding a part of a behavior inside a contract.

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

Floating-point builtins may produce three kinds of alarms: APosInf when the result may contain +oo;, ANegInf when the result may contain -oo;, ANaN msg when the result is NaN; an explanation of why the argument is invalid is given., AAssume msg is a variant of ANaN for debugging purposes, mostly for internal use. Ignored when printing alarms. Builtins may sometimes raise Non_finite when no part of the result is finite.

Builtins return structured alarms, in the guise of a set of string explaining the problem.

Type for a Value builtin function

Rounding modes defined in the C99 standard.

Some functions of this module may optionally use internal caches.

Callback for the buttons that can be in the menus.

Kind of exceptions that are caught by a given clause.

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 for functions adding a part of a contract (either for global function or for a given stmt).

Whether a given preprocessor supports gcc options used in some configurations.

Type of the referenced value.

global declarations.

C locations.

dependencies of an assigned location.

Element in the collection.

Element in the category

The type of the set elements.

The type of the set elements.

Type of status emitted by analyzers.

Entry (a,b,v) maps range a..b (both inclued) to value v in the map.

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 *

GNU extended-asm information: a list of outputs, each of which is an lvalue with optional names and constraints., a list of input expressions along with constraints, clobbered registers, Possible destinations statements

some type for a function information

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.

for statement contract, the set of parent behavior for which the contract is active is part of its identification.

Only AAssert, AInvariant, or APragma.

Same as for Property.identified_behavior.

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

Specialization of a property at a given point.

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.

Type of keys of the map.

type of the keys

The type of the map keys.

Labels

logical expression.

The host part of an Cil_types.lval.

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.

Describes a location in a source file

Description of a constructor of a logic sum-type.

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.

Maps from Base.t to Lmap_sig.offsetmap

model field.

model field.

object that can be named (in particular predicates).

The offset part of an Cil_types.lval.

We want to find a symbolic offset that corresponds to a numeric one, with one additional criterion:

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 the local 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 traces.

Type of internal representations of OCaml type.

Type of a state selection.

Proxy type.

Type of the state to register.

The type of range maps, containing of collection of 'a entry.

Same constructor than Consolidation.t, without argument.

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

\tau t is the type of a category for the type \tau.

This type should be considered private

Mapping from bases to bytes-expressed offsets

This type should be considered private

Json Objects

The type of sets.

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.

Datatype for the offsetmaps

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 stored in the offsetmap

type of the values associated to a location

type of the values

Type of the values associated to the keys.

Validity for variables that might change size.

variant for loop or recursive function.

variant of a loop or a recursive function.

Information about a variable.

Different visiting actions.

Visitor behavior

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

This type represents a list; Nil is the empty list, Node conses a single element, while Component conses a whole component.