A | |
At_with_lscope | |
B | |
Builtins | E-ACSL built-in database. |
Builtins [Options] | |
C | |
Check [Options] | |
Context [Env] | |
D | |
Datatype [Typing] | |
Dup_functions | |
E | |
E_ACSL | E-ACSL. |
Env [Interval] | Environment which maps logic variables to intervals. |
Env | |
Error | Handling errors. |
Error [E_ACSL] | |
Exit_points | E-ACSL tracks a local variable by injecting: a call to |
F | |
Free [At_with_lscope] | |
Full_mmodel [Options] | |
Functions | |
Functions [Options] | |
G | |
Gmp_only [Options] | |
Gmpz | GMP Values. |
H | |
Hashtbl [Datatype.S_with_collections] | |
I | |
Instrument [Options] | |
Interval | Interval inference for terms. |
K | |
Keep_status | Make the property statuses of the initial project accessible when doing the main translation |
Key [Datatype.Hashtbl] | Datatype for the keys of the hashtbl. |
Key [Datatype.Map] | Datatype for the keys of the map. |
L | |
Label | |
Libc [Functions] | |
Literal_strings | Associate literal strings to fresh varinfo. |
Local_config | |
Logic_binding [Env] | |
Logic_functions | |
Logic_scope [Env] | |
Loops | Loop specific actions. |
Lscope | |
M | |
Main | |
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. |
Malloc [At_with_lscope] | |
Map [Datatype.S_with_collections] | |
Misc | Utilities for E-ACSL. |
Mmodel_analysis | |
Mmodel_translate | |
O | |
Options | |
P | |
Prepare [Options] | |
Prepare_ast | Prepare AST for E-ACSL generation. |
Project_name [Options] | |
Q | |
Quantif | Convert quantifiers. |
R | |
RTL [Functions] | |
Replace_libc_functions [Options] | |
Resulting_projects [Main] | |
Rte | Accessing the RTE plug-in easily. |
Run [Options] | |
S | |
Set [Datatype.S_with_collections] | |
T | |
Temporal | Transformations to detect temporal memory errors (e.g., dereference of stale pointers). |
Temporal_validity [Options] | |
Translate | |
Translate [E_ACSL] | |
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 [Env] | |
Visit |