A | |
At_with_lscope | |
B | |
Builtins |
E-ACSL built-in database.
|
Builtins [Options] | |
C | |
Check [Options] | |
Constructor |
Smart constructors for building C code.
|
Context [Env] | |
D | |
Datatype [Typing] | |
E | |
E_ACSL |
E-ACSL.
|
Env |
Environments.
|
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
__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.
|
F | |
Free [At_with_lscope] | |
Full_mmodel [Options] | |
Functions | |
Functions [Options] | |
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 | |
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 |
Move all labels of the
old stmt onto the new stmt .
|
Libc [Functions] | |
Literal_observer |
Observation of literal strings in C expressions.
|
Literal_strings |
Associate literal strings to fresh varinfo.
|
Local_config | |
Logic_binding [Env] | |
Logic_functions |
Generate C implementations of user-defined 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] | |
Memory_observer |
Extend the environment with statements which allocate/deallocate memory
blocks.
|
Misc |
Utilities for E-ACSL.
|
Mmodel_analysis |
Compute a sound over-approximation of what left-values must be tracked by
the memory model library
|
Mmodel_translate | |
O | |
Options |
implementation of Log.S for E-ACSL
|
P | |
Prepare [Options] | |
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] | |
Rational |
Generation of rational numbers.
|
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_* translates a given ACSL annotation into the corresponding C
statement (if any) for runtime assertion checking.
|
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 | |
Z | |
Z [Gmp_types] |
Representation of the unbounded integer type at runtime
|