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

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