| Builtins |
E-ACSL built-in database.
|
| Dup_functions | |
| E_ACSL |
E-ACSL.
|
| Env |
Environments.
|
| Error |
Handling errors.
|
| 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.
|
| Gmpz |
GMP Values.
|
| Interval |
Interval inference for terms.
|
| Label |
Move all labels of the
old stmt onto the new stmt.
|
| Literal_strings |
Associate literal strings to fresh varinfo.
|
| Local_config | |
| Loops |
Loop specific actions.
|
| Main | |
| Misc |
Utilities for E-ACSL.
|
| Mmodel_analysis |
Compute a sound over-approximation of what left-values must be tracked by
the memory model library
|
| Options |
implementation of Log.S for E-ACSL
|
| Prepare_ast |
Prepare AST for E-ACSL generation.
|
| Quantif |
Convert quantifiers.
|
| Rte |
Accessing the RTE plug-in easily.
|
| Temporal |
Transformations to detect temporal memory errors (e.g., derererence of
stale pointers).
|
| Translate | translate_* translates a given ACSL annotation into the corresponding C
statement (if any) for runtime assertion checking.
|
| Typing |
Type system which computes the smallest C type that may contain all the
possible values of a given integer term or predicate.
|
| Visit |