Index of modules

E-ACSL built-in database.

E-ACSL.

Environment which maps logic variables to intervals.

Environments.

Handling errors.

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.

GMP Values.

Interval inference for terms.

Move all labels of the old stmt onto the new stmt.

Associate literal strings to fresh varinfo.

Loop specific actions.

Utilities for E-ACSL.

Compute a sound over-approximation of what left-values must be tracked by the memory model library

implementation of Log.S for E-ACSL

Prepare AST for E-ACSL generation.

Convert quantifiers.

Accessing the RTE plug-in easily.

translate_* translates a given ACSL annotation into the corresponding C statement (if any) for runtime assertion checking.

Type system which computes the smallest C type that may contain all the possible values of a given integer term or predicate.