E-ACSL built-in database.

Handling errors.

GMP Values.

Utilities for E-ACSL.

Register the plugin in the Frama-C kernel.

E-ACSL.

General module for E-ACSL analyses

Datatypes for analyses types

Types used by E-ACSL analyses

Module for preprocessing the quantified predicates.

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.

Interval inference for terms.

Pre-analysis for Labeled terms and predicates.

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.

Accessing the RTE plug-in easily.

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

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

Observation of global variables.

Calls to the GMP's API.

The E-ACSL main instrumentation step.

Code generation for libc functions

Observation of literal strings in C expressions.

Loop specific actions.

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

Convert quantifiers.

Generation of rational numbers.

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.

Prepare AST for E-ACSL generation.

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