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
Environments.
Env [Interval]
Environment which maps logic variables to intervals.
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
Calls to the GMP's API.
Gmp_only [Options]
Gmp_types
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
Move all labels of the old stmt onto the new stmt.
Libc [Functions]
Literal_strings
Associate literal strings to fresh varinfo.
Local_config
Logic_binding [Env]
Logic_functions
Generate C implementations of user-defined 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
Compute a sound over-approximation of what left-values must be tracked by the memory model library
Mmodel_translate

O
Options
implementation of Log.S for E-ACSL

P
Prepare [Options]
Prepare_ast
Prepare AST for E-ACSL generation.
Project_name [Options]

Q
Q [Gmp_types]
Representation of the rational type at runtime
Quantif
Convert quantifiers.

R
RTL [Functions]
Rational
Generation of rational numbers.
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_* translates a given ACSL annotation into the corresponding C statement (if any) for runtime assertion checking.
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
Visit

Z
Z [Gmp_types]
Representation of the unbounded integer type at runtime