E_ACSL plugin


Directory plugins

Section E-acsl (in plugins/e-acsl)


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.
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