Index of modules

A
At_with_lscope
B
Builtins

E-ACSL built-in database.

Builtins [Options]
C
Check [Options]
Context [Env]
D
Datatype [Typing]
Dup_functions
E
E_ACSL

E-ACSL.

Env [Interval]

Environment which maps logic variables to intervals.

Env
Error

Handling errors.

Error [E_ACSL]
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.

F
Free [At_with_lscope]
Full_mmodel [Options]
Functions
Functions [Options]
G
Gmp_only [Options]
Gmpz

GMP Values.

H
Hashtbl [Datatype.S_with_collections]
I
Instrument [Options]
Interval

Interval inference for terms.

K
Keep_status

Make the property statuses of the initial project accessible when doing the main translation

Key [Datatype.Hashtbl]

Datatype for the keys of the hashtbl.

Key [Datatype.Map]

Datatype for the keys of the map.

L
Label
Libc [Functions]
Literal_strings

Associate literal strings to fresh varinfo.

Local_config
Logic_binding [Env]
Logic_functions
Logic_scope [Env]
Loops

Loop specific actions.

Lscope
M
Main
Make [Datatype.Hashtbl]

Build a datatype of the hashtbl according to the datatype of values in the hashtbl.

Make [Datatype.Map]

Build a datatype of the map according to the datatype of values in the map.

Malloc [At_with_lscope]
Map [Datatype.S_with_collections]
Misc

Utilities for E-ACSL.

Mmodel_analysis
Mmodel_translate
O
Options
P
Prepare [Options]
Prepare_ast

Prepare AST for E-ACSL generation.

Project_name [Options]
Q
Quantif

Convert quantifiers.

R
RTL [Functions]
Replace_libc_functions [Options]
Resulting_projects [Main]
Rte

Accessing the RTE plug-in easily.

Run [Options]
S
Set [Datatype.S_with_collections]
T
Temporal

Transformations to detect temporal memory errors (e.g., dereference of stale pointers).

Temporal_validity [Options]
Translate
Translate [E_ACSL]
Typing

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

V
Valid [Options]
Validate_format_strings [Options]
Varname [Env]
Visit