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
Options

Directory plugins

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


E_ACSL

E-ACSL.

Directory src

Section Analyses (in src/analyses)


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.

Literal_strings

Associate literal strings to fresh varinfo.

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)


At_with_lscope
Contract
Contract_types
Env
Global_observer

Observation of global variables.

Gmp

Calls to the GMP's API.

Injector

The E-ACSL main instrumentation step.

Label
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
Translate_annots
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.