E_ACSL plugin

Chapter 2. Libraries

Section Libraries (in src/libraries/libraries)


Builtins

E-ACSL built-in database.

Error

Handling errors.

Functions
Gmp_types

GMP Values.

Logic_aggr
Misc

Utilities for E-ACSL.

Varname

Directory e-acsl

Section Src (in e-acsl/src)


Local_config
Main

Register the plugin in the Frama-C kernel.

Options

Directory plugins

Section E-acsl (in plugins/e-acsl)


E_ACSL

E-ACSL.

Directory src

Section Analyses (in src/analyses)


Analyses

General module for E-ACSL analyses

Analyses_datatype

Datatypes for analyses types

Analyses_types

Types used by E-ACSL analyses

Bound_variables

Module for preprocessing the quantified predicates.

E_acsl_visitor
Exit_points

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

Interval inference for terms.

Labels

Pre-analysis for Labeled terms and predicates.

Literal_strings

Associate literal strings to fresh varinfo.

Logic_normalizer

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.

Lscope
Memory_tracking
Rte

Accessing the RTE plug-in easily.

Typing

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

Section Code_generator (in src/code_generator)


Assert

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

Assigns
Contract
Contract_types
Env
Global_observer

Observation of global variables.

Gmp

Calls to the GMP's API.

Injector

The E-ACSL main instrumentation step.

Libc

Code generation for libc functions

Literal_observer

Observation of literal strings in C expressions.

Logic_array
Logic_functions
Loops

Loop specific actions.

Memory_observer

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

Memory_translate
Quantif

Convert quantifiers.

Rational

Generation of rational numbers.

Smart_exp
Smart_stmt
Temporal

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

Translate_annots
Translate_ats

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

Translate_predicates

Generate C implementations of E-ACSL predicates.

Translate_rtes

Generate and translate RTE annotations.

Translate_terms

Generate C implementations of E-ACSL terms.

Translate_utils

Utility functions for generating C implementations.

Translation_error
Typed_number

Manipulate the type of numbers.

Section Project_initializer (in src/project_initializer)


Prepare_ast

Prepare AST for E-ACSL generation.

Rtl

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