Index of types

Abstraction to be registered.

These actions redefine the partitioning by updating keys or spliting states.

Three modes to handle the alarms when evaluating a logical term.

What is used for the analysis of a given function: a Cvalue builtin (and other domains use the specification), the function specification, the function body. The boolean indicates whether the resulting states must be recorded at each statement of this function.

Argument of a function call.

Assigned values.

Junction branch id in the control flow

Type of a cvalue builtin, whose arguments are: the memory state at the beginning of the function call;, the list of arguments of the function call.

A builtin is an ocaml function for the interpretation of a whole C function: it takes the list of value arguments, and returns the result (that can be bottom).

Type of a cvalue builtin, whose arguments are: the memory state at the beginning of the function call;, the list of arguments of the function call.

Can the results of a builtin be cached? See for more details.

Can the results of a function call be cached with memexec?

Can the results of a builtin be cached? See for more details.

Can the results of a function call be cached with memexec?

A function call.

If not None, the froms of the function, and its sure outputs; i.e.

The result of a builtin can be given in different forms.

The result of a builtin can be given in different forms.

Value call-site.

A call site: the function called, and the call statement (or Kglobal for the main function.

Value callstacks, as used e.g.

Set of bases that might contain a reference to a local or formal variable.

Computation state of the analysis.

A simpler functional interface for valuations.

Type of the referenced value.

Type of domain to be registered: either a leaf module with 'v as value abstraction, or a functor building a domain from any value abstraction.

The type of the equality elements.

Equality witness between types.

Evaluation environment.

Most forward evaluation functions return the set of alarms resulting from the operations, and a result which can be `Bottom, if the evaluation fails, or the expected value.

Context from the engine evaluation about a domain query.

This is the record that encapsulates all evaluation functions

Filters on callstacks.

Flag for an abstract domain.

Right values with 'undefined' and 'escaping addresses' flags.

A set of states which are currently propagated

Split/merge annotations for value partitioning.

Split/merge annotations for value partitioning.

A function associated with an analysis mode.

Type of widening hints: a special kind of lval for which the hints will apply and a list of names (e.g.

Value for the initialization of variables.

Abstraction of an integer type, more convenient than an ikind because it can also be used for bitfields.

The type of the map keys.

Partitioning keys attached to states.

Type of keys of the map.

Reason of the replacement of an lvalue lval: Modified means that the value of lval has been modified (in which case &lval is unchanged), and Deleted means that lval is no longer in scope (in which case &lval raises the NonExchangeable error).

Lvalue with its location and type.

Location of an lvalue.

Abstract memory location.

Abstract memory locations associated to left values.

abstract locations

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

The logic dependency of an ACSL assigns clause.

Dependencies needed to evaluate a term or a predicate

Environment for the logical evaluation of predicates.

Error during the evaluation of a term or a predicate

stack of open loops

Mode for the analysis of a function f: current is the read/write permission for f., calls is the read/write permission for all functions called from f.

abstract offsets

The origin is used by the domain combiners to track the origin of a value.

Origin of values.

Origin of values.

Collection of states, each identified by a unique key.

Permission for an abstract domain to read/write its state.

For the moment, all domains must use precise_loc as their location abstraction, and no new location abstraction can be registered for an analysis.

Evaluating a predicate.

Rationing are used to keep separate the n first states propagated at a point, by creating unique stamp until the limit is reached.

List.rev on a callstack, enforced by strong typing outside of this module

Data record associated to each evaluated left-value.

Data record associated to each evaluated expression.

Information needed to interpret a recursive call.

Most backward evaluation function returns `Bottom if the reduction leads to an invalid state, `Unreduced if no reduction can be performed, or the reduced value.

State of reduction of an abstract value.

Kind of results for the analysis of a function body.

Kind of results for the analysis of a function body.

Abstraction of scalar types -- in particular, all those that can be involved in a cast.

Both the formal argument of a called function and the concrete argument at a call site.

Simple information about a function call.

Annotations tweaking the behavior of the -eva-slevel parameter.

Annotations tweaking the behavior of the -eva-slevel parameter.

Splits on an expression can be static or dynamic: static splits are processed once: the expression is only evaluated at the split point, and the key is then kept unchanged until a merge., dynamic splits are regularly redone: the expression is re-evaluated, and states are then split or merged accordingly.

Split monitor: prevents splits from generating too many states.

Splits can be performed according to a C expression or an ACSL predicate.

Domain state.

State of abstract domain.

The states being partitioned

The storage of all states ever met at a control point

The gadt, based on keys giving the type of each node.

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

Semantics of the constructors: C_init_*: definitely initialized, C_uninit_*: possibly uninitialized, C_*_noesc: never contains escaping addresses, C_*_esc: may contain escaping addresses C_uninit_noesc V.bottom: guaranteed to be uninitialized, C_init_esc V.bottom: guaranteed to be an escaping address, C_uninit_esc V.bottom: either uninitialized or an escaping address C_init_noesc V.bottom: "real" bottom, with an empty concretization. Corresponds to an unreachable state.

Type of states.

The set of states that remains to propagate from a control point.

Type for the truth value of an assertion in a value abstraction.

Loop unroll annotations.

Loop unroll annotations.

The unroll limit of a loop.

Results of an evaluation: the results of all intermediate calculation (the value of each (sub)expression and the location of each lvalue) are available to the domain.

Numerical values to which the expressions are evaluated.

Module types of value abstractions: either a single leaf module, or a compound of several modules described by a structure.

Numeric values to which the expressions are evaluated.

Abstract value.

Type of the values associated to the keys.

Reduced product between two value abstractions, identified by their keys.

An argument of type warn_mode can be supplied to some of the access functions in Db.Value (the interface to the value analysis).

Widening information

A type and a set of alarms.

Information about a registered abstraction.