Index of types

Kind of memory access.

Access kind: read/write of k bits, or no access.

Type explaining how to manipulate the elements of the category.

Extension to standard ACSL clause with an unique identifier.

Button for dialog options

possible kinds of action for backward analysis

Table columns alignment

allocates and frees.

allocates and frees.

type for alpha conversion table.

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

all kind of annotations

size of logic array.

zone assigned with its dependencies.

zone assigned with its dependencies.

Various classes of attributes

Attributes are lists sorted by the attribute name.

The type of parameters of attributes

Behavior in a specification.

Behavior of a function or statement.

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

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

context in which a block will be printed.

A packed widget with its layout directives

Buffer for creating messages.

A text buffer to compose labels and attributes.

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.

all annotations that can be found in the code.

type of registered code transformations

The definition of a structure or union type.

Each component of the graph is either an individual node of the graph (without) self loop, or a strongly connected component where a node is designed as the head of the component and the remaining nodes are given by a list of components topologically ordered.

The configuration data can be of several types *

Literal constants

type for functions adding a part of a contract (either for global function or for a given stmt).

Control flow informations for outgoing edges, if any.

possible correspondances between new items and original ones.

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

Registered daemon on progress.

Type of the referenced value.

Whether the allocated base has been obtained via calls to malloc/calloc/realloc (Malloc), alloca (Alloca), or is related to a variable-length array (VLA).

global declarations.

Contents of a variable when it is not present in the state.

dependencies of an assigned location.

dependencies of an assigned location.

Buffer to a dot file with a graph environment (nodes, edges, etc.)

The type of the elements that are hash-consed

Element in the collection.

Element in the category

Type of status emitted by analyzers.

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

Information about an enumeration.

Existence requirement on a file.

A datatype to be used in conjunction with existsType

Expressions (Side-effect free)

Expansion Modes.

Where are we expected to find corresponding extension keyword.

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

Untyped ACSL extensions transformers

Pretty printers for ACSL extensions

Transformers from untyped to typed ACSL extension

Visitor functions for ACSL extensions

some type for a function information

The expansible attribute of a field.

Information about a struct/union field.

File type, according to how it will be preprocessed.

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

the file name, and then the list of toplevel forms.

Various kinds of floating-point numbers

Type of the interval bounds.

The type of argument for the interpreter

behavior of a function.

Function definitions.

generic accessor type

The main type for representing global declarations and definitions.

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

For if statements

How to journalize the given function.

Local refs and URLs

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, identified by a statement and a function, along with the predicate transposed at this point (if it can be) and the original property.

predicate with an unique identifier.

None, Kglobal --> global property None, Some ki --> 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.

Pragmas for the impact plugin of Frama-C.

possible causes for raising Cil.LenOfArray

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.

Json Objects

Only field fundec can be used directly.

The type of the map keys.

Type of keys of the map.

type of the keys

Type of the keys.

Labels

Maps binding the labels from an annotation to the vertices they refer to in the graph.

logical expression.

Kind of expression

The host part of an Cil_types.lval.

Styles of printing line directives

local information needed to typecheck expressions and statements

Initializers for local variables.

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

builtin logic labels defined in ACSL.

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.

Definition of a machine model (architecture + compiler).

Maps from Base.t to Lmap_sig.offsetmap

Type of the maps from type key to type 'v.

Margin accumulator (low-level API to pp_items).

Message with tags

model field.

model field.

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 and pointer downcasts are really RTEs.

Structural descriptor used inside structures.

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

Generic type for parsing functions built on tip of the lexer.

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

for kernel function, we are a bit more precise than a yes/no answer.

A list of strongly connected components, sorted topologically

construct inside a functional update.

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

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

Describes a position in a source file.

The various kinds of pragmas.

The various kinds of pragmas.

Precision of floating-point numbers: the 'single', 'double' and 'long double' C types;, the ACSL 'real' type.

Precision of the intervals.

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

predicates with a location and an optional list of names

predicates

Does the given predicate hold or not.

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

Partial order of preference for the choice of the head of a loop.

Undocumented.

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.

Rounding modes defined in the C99 standard.

Sets whose cardinal exceeds a certain limit must be converted into intervals.

Shareable tasks.

Pragmas for the slicing plugin of Frama-C.

Pragmas for the slicing plugin of Frama-C.

Function or statement contract.

Function or statement contract.

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

Internal state of the value analysis.

Type of the local status of a property.

Statements.

Storage-class information

Description with details.

Type used for the substitution between bases.

Various syntactic scopes through which an identifier might be searched.

Type of the widget containing the warnings.

How the visitor should behave in front of mutable fields: in place modification or copy of the structure.

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.

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.

Mapping from bases to bytes-expressed offsets

States propagated by the dataflow analysis.

Type of intervals.

Type of a type descriptor.

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 normalized (absolute) path.

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.

Inline elements separated by spaces

main statement of an annotation.

Each transition can either be a skip (do nothing), a return, a guard represented by a Cil expression, a Cil instruction, an ACSL annotation or entering/leaving a block.

type invariant.

The different namespaces a C type can belong to, used when we are searching a type by its name.

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 of a loop or a recursive function.

variant of a loop or a recursive function.

Information about a variable.

Different visiting actions.

Same as above, but for warnings

status of a warning category

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

Type of the widen hints.

A weak topological ordering where nodes are Cil statements

Weak Topological Order is given by a list (in topological order) of components of the graph, which are themselves WTOs

the position of a statement in a wto given as the list of component heads

the position of a statement in a wto given as the list of component heads