Index of modules

A
Analyses

General module for E-ACSL analyses

Analyses_datatype

Datatypes for analyses types

Analyses_types

Types used by E-ACSL analyses

Annotation_kind [Analyses_datatype]
Assert

Module with the context to hold the data contributing to an assertion and general functions to create assertion statements.

Assert_print_data [Options]
Assigns
At_data [Analyses_datatype]
B
Bound_variables

Module for preprocessing the quantified predicates.

Builtins

E-ACSL built-in database.

Builtins [Options]
C
Concurrency [Functions]
Concurrency [Options]
Context [Env]
Contract
Contract_types
D
D [Lscope]
Dkey [Options]
E
E_ACSL

E-ACSL.

E_acsl_visitor
Env
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 [Translate_ats]
Full_mtracking [Options]
Function_params_ty [Typing]
Functions
Functions [Options]
Functions [E_ACSL]
G
Global_observer

Observation of global variables.

Gmp

Calls to the GMP's API.

Gmp_only [Options]
Gmp_types

GMP Values.

H
Hashtbl [Datatype.S_with_collections]
I
Id_term [Misc]

Datatype for terms that relies on physical equality.

Injector

The E-ACSL main instrumentation step.

Instrument [Options]
Interval

Interval inference for terms.

K
Key [Datatype.Hashtbl]

Datatype for the keys of the hashtbl.

Key [Datatype.Map]

Datatype for the keys of the map.

L
Labels

Pre-analysis for Labeled terms and predicates.

Libc

Code generation for libc functions

Libc [Functions]
Literal_observer

Observation of literal strings in C expressions.

Literal_strings

Associate literal strings to fresh varinfo.

Local_config
Local_vars [Env]
Logic_aggr
Logic_array
Logic_binding [Env]
Logic_functions
Logic_normalizer

This module is dedicated to some preprocessing on the predicates: It guards all the Pvalid and Pvalid_read clauses with an adequate Pinitialized clause;, It replaces all the applications Papp by a corresponding term obtained as an application Tapp The predicates that have undergone these changed are called the preprocessed predicates.

Logic_scope [Env]
Loops

Loop specific actions.

Lscope
M
Main

Register the plugin in the Frama-C kernel.

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.

Make [Error]

Functor to build an Error module for a given phase.

Malloc [Translate_ats]
Map [Datatype.S_with_collections]
Memory_observer

Extend the environment with statements which allocate/deallocate memory blocks.

Memory_tracking
Memory_translate
Misc

Utilities for E-ACSL.

O
Options
Options [E_ACSL]
P
Pred_or_term [Analyses_datatype]
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]
RTL [E_ACSL.Functions]
Rational

Generation of rational numbers.

Replace_libc_functions [Options]
Rte

Accessing the RTE plug-in easily.

Rtl

This module links the E-ACSL's RTL to the user source code.

Run [Options]
S
Set [Datatype.S_with_collections]
Smart_exp
Smart_stmt
Symbols [Rtl]

Tables that contain RTL's symbols.

T
Temporal

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

Temporal_validity [Options]
Translate_annots
Translate_ats

Generate C implementations of E-ACSL \at() terms and predicates.

Translate_predicates

Generate C implementations of E-ACSL predicates.

Translate_predicates [E_ACSL]
Translate_rtes

Generate and translate RTE annotations.

Translate_terms

Generate C implementations of E-ACSL terms.

Translate_terms [E_ACSL]
Translate_utils

Utility functions for generating C implementations.

Translation_error
Typed_number

Manipulate the type of numbers.

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
Z
Z [Gmp_types]

Representation of the unbounded integer type at runtime