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.
Misc
Utilities for E-ACSL.
Varname

Directory e-acsl

Section Src (in e-acsl/src)


Local_config
Main
Options
implementation of Log.S for E-ACSL

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
Mmodel_analysis
Compute a sound over-approximation of what left-values must be tracked by the memory model library
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
Constructor
Smart constructors for building C code.
Env
Environments.
Global_observer
Observation of global variables.
Gmp
Calls to the GMP's API.
Injector
The E-ACSL main instrumentation step.
Label
Move all labels of the old stmt onto the new stmt.
Literal_observer
Observation of literal strings in C expressions.
Logic_functions
Generate C implementations of user-defined logic functions.
Loops
Loop specific actions.
Memory_observer
Extend the environment with statements which allocate/deallocate memory blocks.
Mmodel_translate
Quantif
Convert quantifiers.
Rational
Generation of rational numbers.
Temporal
Transformations to detect temporal memory errors (e.g., dereference of stale pointers).
Translate
translate_* translates a given ACSL annotation into the corresponding C statement (if any) for runtime assertion checking.

Section Project_initializer (in src/project_initializer)


Keep_status
Make the property statuses of the initial project accessible when doing the main translation
Prepare_ast
Prepare AST for E-ACSL generation.