A | |
Analyses | General module for E-ACSL analyses |
Analyses_datatype | Datatypes for analyses types |
Analyses_types | Types used by E-ACSL analyses |
Annotation_kind [Analyses_datatype] | |
Assert | Module with the context to hold the data contributing to an assertion and general functions to create assertion statements. |
Assert_print_data [Options] | |
Assigns | |
At_data [Analyses_datatype] | |
B | |
Bound_variables | Module for preprocessing the quantified predicates. |
Builtins | E-ACSL built-in database. |
Builtins [Options] | |
C | |
Concurrency [Functions] | |
Concurrency [Options] | |
Context [Env] | |
Contract | |
Contract_types | |
D | |
D [Lscope] | |
Dkey [Options] | |
E | |
E_ACSL | E-ACSL. |
E_acsl_visitor | |
Env | |
Env [Interval] | Environment which maps logic variables to intervals. |
Error | Handling errors. |
Error [E_ACSL] | |
Exit_points | E-ACSL tracks a local variable by injecting: a call to |
F | |
Free [Translate_ats] | |
Full_mtracking [Options] | |
Function_params_ty [Typing] | |
Functions | |
Functions [Options] | |
Functions [E_ACSL] | |
G | |
Global_observer | Observation of global variables. |
Gmp | Calls to the GMP's API. |
Gmp_only [Options] | |
Gmp_types | GMP Values. |
H | |
Hashtbl [Datatype.S_with_collections] | |
I | |
Id_term [Misc] | Datatype for terms that relies on physical equality. |
Injector | The E-ACSL main instrumentation step. |
Instrument [Options] | |
Interval | Interval inference for terms. |
K | |
Key [Datatype.Hashtbl] | Datatype for the keys of the hashtbl. |
Key [Datatype.Map] | Datatype for the keys of the map. |
L | |
Labels | Pre-analysis for Labeled terms and predicates. |
Libc | Code generation for libc functions |
Libc [Functions] | |
Literal_observer | Observation of literal strings in C expressions. |
Literal_strings | Associate literal strings to fresh varinfo. |
Local_config | |
Local_vars [Env] | |
Logic_aggr | |
Logic_array | |
Logic_binding [Env] | |
Logic_functions | |
Logic_normalizer | This module is dedicated to some preprocessing on the predicates: It guards all the |
Logic_scope [Env] | |
Loops | Loop specific actions. |
Lscope | |
M | |
Main | Register the plugin in the Frama-C kernel. |
Make [Datatype.Hashtbl] | Build a datatype of the hashtbl according to the datatype of values in the hashtbl. |
Make [Datatype.Map] | Build a datatype of the map according to the datatype of values in the map. |
Make [Error] | Functor to build an |
Malloc [Translate_ats] | |
Map [Datatype.S_with_collections] | |
Memory_observer | Extend the environment with statements which allocate/deallocate memory blocks. |
Memory_tracking | |
Memory_translate | |
Misc | Utilities for E-ACSL. |
O | |
Options | |
Options [E_ACSL] | |
P | |
Pred_or_term [Analyses_datatype] | |
Prepare_ast | Prepare AST for E-ACSL generation. |
Project_name [Options] | |
Q | |
Q [Gmp_types] | Representation of the rational type at runtime |
Quantif | Convert quantifiers. |
R | |
RTL [Functions] | |
RTL [E_ACSL.Functions] | |
Rational | Generation of rational numbers. |
Replace_libc_functions [Options] | |
Rte | Accessing the RTE plug-in easily. |
Rtl | This module links the E-ACSL's RTL to the user source code. |
Run [Options] | |
S | |
Set [Datatype.S_with_collections] | |
Smart_exp | |
Smart_stmt | |
Symbols [Rtl] | Tables that contain RTL's symbols. |
T | |
Temporal | Transformations to detect temporal memory errors (e.g., dereference of stale pointers). |
Temporal_validity [Options] | |
Translate_annots | |
Translate_ats | Generate C implementations of E-ACSL |
Translate_predicates | Generate C implementations of E-ACSL predicates. |
Translate_predicates [E_ACSL] | |
Translate_rtes | Generate and translate RTE annotations. |
Translate_terms | Generate C implementations of E-ACSL terms. |
Translate_terms [E_ACSL] | |
Translate_utils | Utility functions for generating C implementations. |
Translation_error | |
Typed_number | Manipulate the type of numbers. |
Typing | Type system which computes the smallest C type that may contain all the possible values of a given integer term or predicate. |
V | |
Valid [Options] | |
Validate_format_strings [Options] | |
Varname | |
Z | |
Z [Gmp_types] | Representation of the unbounded integer type at runtime |