Index of modules

Value analysis builtin shipped with Frama-C, more efficient than their equivalent in C

Builtins for standard floating-point functions.

Non-free Value builtins.

Non-free Value builtins for deterministic code.

Dynamic allocation related builtins.

Translate a Value state into a bunch of C assertions

Estimation of the cardinal of the concretization of an abstract state or value.

Value analysis alarms

Representation of Value's abstract memory.

Values bound by default to a variable.

Statuses for code annotations and function contracts

Reduction by operators condition

Value analysis of entire functions.

Evaluation of non-linear expressions.

Numeric evaluation.

Mark the analysis as aborted.

Value analysis of statements and functions bodies

Evaluation of terms and predicates

This module contains functions related to type conversions

For all formals of kf whose address is taken, merge their values in prev_state and new_state, and update new_state.

Filtering on analysis callstacks

This module defines an abstraction to evaluate various things across multiple callstacks.

Creation of the initial state for Value

Datatype for the keys of the hashtbl.

Datatype for the keys of the map.

Associates kernel_function to a fresh base for the address returned by the kernel_function.

Auxiliary functions to mark invalid (more precisely 'escaping') the references to a variable whose scope ends.

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

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

This module memorizes the analysis of entire calls to a function, so that those analyzes can be reused later on.

Does the evaluation of stmt modifies the eventual value of X.lv?

Memories.

Fine-tuning for slevel, according to //@ slevel directives.

This module provides transient datastructures that may be more precise than an Ival.t, Locations.Location_Bits.t and Locations.location respectively, typically for l-values such as t[i][j], p->t[i], etc.

Function of the value plugin registered in the kernel

Extension of the GUI in order to support the value analysis.

This module is used to merge together the final states of a function according to a given strategy.

Sets of Cvalue.Model.t implemented imperatively.

Functional sets of Cvalue.Model.t, currently implemented as lists without repetition.

Values.

Memory slices.

Values with 'undefined' and 'escaping addresses' flags.

division.

Analysis for values and pointers

Subtype of Value_types.call_res

UNDOCUMENTED.

Call start_doing when starting analyzing a new function.

This file will ultimately contain all the results computed by Value (which must be moved out of Db.Value), both per stack and globally.

Declarations that are useful for plugins written on top of the results of Value.

A call_stack is a list, telling which function was called at which site.

This function should be used to treat a call lv = kf(...).

Widening hints for the Value Analysis datastructures.