Apron_domain | Experimental binding for the numerical abstract domains provided by the APRON library: http://apron.cri.ensmp.fr/library For now, this binding only processes scalar integer variables. |
Builtins | Value analysis builtin shipped with Frama-C, more efficient than their equivalent in C |
Builtins_float | Builtins for standard floating-point functions. |
Builtins_malloc | Dynamic allocation related builtins. |
Builtins_memory | Nothing is exported, all the builtins are registered through |
Builtins_misc | Builtins for normalization and dumping of values or state. |
Builtins_print_c | Translate a Value state into a bunch of C assertions |
Builtins_split | |
Builtins_string | A builtin takes the state and a list of values for the arguments, and returns the offsetmap of the return value (None if bottom), and a boolean indicating the possibility of alarms. |
Builtins_watchpoint | |
Cvalue_domain | Main domain of the Value Analysis. |
Cvalue_init | Creation of the initial state for Value |
Cvalue_offsetmap | Auxiliary functions on cvalue offsetmaps, used by the cvalue domain. |
Cvalue_specification | No function exported. |
Cvalue_transfer | Transfer functions for the main domain of the Value analysis. |
Locals_scoping | Auxiliary functions to mark invalid (more precisely 'escaping') the references to a variable whose scope ends. |
Warn | Alarms and imprecision warnings emitted during the analysis. |
Equality | Equalities between syntactic lvalues and expressions. |
Equality_domain | Initial abstract state at the beginning of a call. |
Gauges_domain | Gauges domain ("Arnaud Venet: The Gauge Domain: Scalable Analysis of Linear Inequality Invariants. |
Numerors_domain |
Alarmset | Map from alarms to status. |
Eva | Analysis for values and pointers |
Eval | |
Register | Functions of the Value plugin registered in |
Value_parameters |
CilE | Value analysis alarms |
Cvalue | Representation of Value's abstract memory. |
Precise_locs | This module provides transient datastructures that may be more precise
than an |
Value_types | Declarations that are useful for plugins written on top of the results of Value. |
Widen_type | Widening hints for the Value Analysis datastructures. |
Abstract_domain | Abstract domains of the analysis. |
Domain_builder | Automatic builders to complete abstract domains from different simplified interfaces. |
Domain_lift | |
Domain_product | |
Domain_store | |
Hcexprs | Hash-consed expressions and lvalues. |
Inout_domain | Computation of inputs of outputs. |
Offsm_domain | |
Powerset | |
Printer_domain | An abstract domain built on top of the Simpler_domains.Simple_Cvalue interface that just prints the transfer functions called by the engine during an analysis. |
Sign_domain | Abstraction of the sign of integer variables. |
Simple_memory | Simple memory abstraction for scalar non-volatile variables, built upon a value abstraction. |
Simpler_domains | Simplified interfaces for abstract domains. |
Symbolic_locs | Domain that store information on non-precise l-values such as
|
Unit_domain |
Abstractions | Constructions of the abstractions used by Eva. |
Analysis | |
Compute_functions | Value analysis of entire functions, using Eva engine. |
Evaluation | |
Initialization | Creation of the initial state of abstract domain. |
Iterator | |
Mem_exec | |
Partition | A partition is a collection of states, each identified by a unique key. |
Partitioning_index | A partitioning index is a collection of states optimized to determine if a new state is included in one of the states it contains — in a more efficient way than to test the inclusion with all stored states. |
Partitioning_parameters | |
Recursion | Handling of recursion cycles in the callgraph |
Split_return | This module is used to merge together the final states of a function according to a given strategy. |
Subdivided_evaluation | Subdivision of the evaluation on non-linear expressions: for expressions in which some l-values appear multiple times, proceed by disjunction on their abstract value, in order to gain precision. |
Trace_partitioning | |
Transfer_logic | |
Transfer_specification | |
Transfer_stmt |
Gui_callstacks_filters | Filtering on analysis callstacks |
Gui_callstacks_manager | This module creates and manages the "Values" panel on the lower notebook of the GUI. |
Gui_eval | This module defines an abstraction to evaluate various things across multiple callstacks. |
Gui_red | Extension of the GUI in order to display red alarms emitted during the value analysis |
Gui_types | |
Register_gui | Extension of the GUI in order to support the value analysis. |
Eval_annots | |
Eval_op | Numeric evaluation. |
Eval_terms | Evaluation of terms and predicates |
Function_args | Nothing is exported; the function |
Per_stmt_slevel | Fine-tuning for slevel, according to |
Split_strategy |
Backward_formals | Functions related to the backward propagation of the value of formals at the end of a call. |
Eval_typ | |
Library_functions | |
Mark_noresults | |
Partitioning_annots | |
Red_statuses | |
State_import | Saving/loading of Value states, possibly among different ASTs. |
Structure | Gadt describing the structure of a tree of different data types, and providing fast accessors of its nodes. |
Value_perf | Call |
Value_results | This file will ultimately contain all the results computed by Value (which must be moved out of Db.Value), both per stack and globally. |
Value_util | |
Widen | Per-function computation of widening hints. |
Widen_hints_ext | Syntax extension for widening hints, used by Value. |
Abstract_location | Abstract memory locations of the analysis. |
Abstract_value | Abstract numeric values of the analysis. |
Cvalue_backward | Abstract reductions on Cvalue.V.t |
Cvalue_forward | Forward operations on Cvalue.V.t |
Location_lift | |
Main_locations | Main memory locations of Eva: |
Main_values | Main numeric values of Eva. |
Offsm_value | |
Sign_value | Sign domain: abstraction of integer numerical values by their signs. |
Value_product | Cartesian product of two value abstractions. |