Builtins | E-ACSL built-in database. |
Dup_functions | |
E_ACSL | E-ACSL. |
Env | |
Error | Handling errors. |
Exit_points | E-ACSL tracks a local variable by injecting: a call to |
Functions | |
Gmpz | GMP Values. |
Interval | Interval inference for terms. |
Keep_status | Make the property statuses of the initial project accessible when doing the main translation |
Label | |
Literal_strings | Associate literal strings to fresh varinfo. |
Local_config | |
Loops | Loop specific actions. |
Main | |
Misc | Utilities for E-ACSL. |
Mmodel_analysis | |
Options | |
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 | |
Typing | Type system which computes the smallest C type that may contain all the possible values of a given integer term or predicate. |
Visit |