Index of modules

General module for E-ACSL analyses

Datatypes for analyses types

Types used by E-ACSL analyses

Module with the context to hold the data contributing to an assertion and general functions to create assertion statements.

Module for preprocessing the quantified predicates.

E-ACSL built-in database.

E-ACSL.

Environment which maps logic variables to intervals.

Handling errors.

E-ACSL tracks a local variable by injecting: a call to __e_acsl_store_block at the beginning of its scope, and, a call to __e_acsl_delete_block at the end of the scope. This is not always sufficient to track variables because execution may exit a scope early (for instance via a goto or a break statement). This module computes program points at which extra delete_block statements need to be added to handle such early scope exits.

Observation of global variables.

Calls to the GMP's API.

GMP Values.

Datatype for terms that relies on physical equality.

The E-ACSL main instrumentation step.

Interval inference for terms.

Datatype for the keys of the hashtbl.

Datatype for the keys of the map.

Pre-analysis for Labeled terms and predicates.

Code generation for libc functions

Observation of literal strings in C expressions.

Associate literal strings to fresh varinfo.

This module is dedicated to some preprocessing on the predicates: It guards all the Pvalid and Pvalid_read clauses with an adequate Pinitialized clause;, It replaces all the applications Papp by a corresponding term obtained as an application Tapp The predicates that have undergone these changed are called the preprocessed predicates.

Loop specific actions.

Register the plugin in the Frama-C kernel.

Build a datatype of the hashtbl according to the datatype of values in the hashtbl.

Build a datatype of the map according to the datatype of values in the map.

Functor to build an Error module for a given phase.

Extend the environment with statements which allocate/deallocate memory blocks.

Utilities for E-ACSL.

Prepare AST for E-ACSL generation.

Representation of the rational type at runtime

Convert quantifiers.

Generation of rational numbers.

Accessing the RTE plug-in easily.

This module links the E-ACSL's RTL to the user source code.

Tables that contain RTL's symbols.

Transformations to detect temporal memory errors (e.g., dereference of stale pointers).

Generate C implementations of E-ACSL \at() terms and predicates.

Generate C implementations of E-ACSL predicates.

Generate and translate RTE annotations.

Generate C implementations of E-ACSL terms.

Utility functions for generating C implementations.

Manipulate the type of numbers.

Type system which computes the smallest C type that may contain all the possible values of a given integer term or predicate.

Representation of the unbounded integer type at runtime