Builtins | E-ACSL built-in database. |
Error | Handling errors. |
Functions | |
Gmp_types | GMP Values. |
Logic_aggr | |
Misc | Utilities for E-ACSL. |
Varname |
Local_config | |
Main | Register the plugin in the Frama-C kernel. |
Options |
E_ACSL | E-ACSL. |
Bound_variables | Module for preprocessing the quantified predicates. |
E_acsl_visitor | |
Exit_points | E-ACSL tracks a local variable by injecting: a call to |
Interval | Interval inference for terms. |
Literal_strings | Associate literal strings to fresh varinfo. |
Logic_normalizer | This module is dedicated to some preprocessing on the predicates: It guards all the |
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. |
Assert | Module with the context to hold the data contributing to an assertion and general functions to create assertion statements. |
Assigns | |
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 | |
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 | Generate C implementations of E-ACSL predicates and terms. |
Translate_annots | |
Typed_number | Manipulate the type of numbers. |
Prepare_ast | Prepare AST for E-ACSL generation. |
Rtl | This module links the E-ACSL's RTL to the user source code. |