Source file `Eva.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

(** Eva public API.

    Apart from [Analysis] and [Results], all modules exported here are
    development interfaces which may change with each Frama-C release. *)


(** {2 Main stable API} *)

(** Run the analysis and check analysis status. *)
module Analysis = Analysis

(** Main API to access the results of an analysis, such as the possible values
    of expressions and memory locations of lvalues at each program point. *)
module Results = Results


(** {2 Statistics} *)

(** Statistics about the analysis performance. *)
module Eva_perf = (Eva_perf : Eva_perf_sig.API)

(** Various statistics collected during an analysis. *)
module Statistics = Statistics


(** {2 Types used in Eva} *)

(** AST used by Eva. *)
module Eva_ast = Eva_ast

(** Position in the analysis *)
module Position = Position

(** Types of callstack. *)
module Callstack = Callstack

(** Types for the memory dependencies of an expression or lvalue. *)
module Deps = Deps


(** {2 Configuration of the analysis} *)

(** Command-line parameters of the analysis. *)
module Parameters = Parameters

(** Add local annotations to guide the analysis. *)
module Eva_annotations = Eva_annotations

(** Register OCaml builtins to be used by the cvalue domain instead of analysing
    the body of some C functions. *)
module Builtins = (Builtins : Builtins_sig.API)


(** {2 Registration of new abstractions} *)

(** Various types used in abstract domain signature. *)
module Eval = Eval

(** Signature of abstract domains, inferring properties about the program
    during the analysis. *)
module Abstract_domain = Abstract_domain

(** Signature of abstract numerical values, representing the set of possible
    values of an expression or lvalue. Used to exchange information between
    abstract domains. *)
module Abstract_value = Abstract_value

(** Signature of abstract memory locations, representing the set of possible
    memory locations pointed to by an lvalue. *)
module Abstract_location = Abstract_location

(** Signature of abstract state, which can be used to transfer information from
    states of abstract domains to abstract values. *)
module Abstract_context = Abstract_context

(** Empty context. *)
module Unit_context = Unit_context

(** Automatic builders to complete abstract domains from different
    simplified interfaces. *)
module Domain_builder = Domain_builder

(** Simplified interfaces for abstract domains. Complete abstract domains can be
    built from these interfaces through the functors in {!Domain_builder}. *)
module Simpler_domains = Simpler_domains

(** Build a domain upon a value abstraction with a very simple memory model
    for scalar non-volatile variables. *)
module Simple_memory = Simple_memory

(** Register new abstract domains. *)
module Domain = Abstractions.Domain

(** Common value abstractions shared by many abstract domains. *)
module Main_values = Main_values

(** Common location abstractions shared by many abstract domains. *)
module Main_locations = Main_locations


(** {2 Internal API}

    These modules are for internal use only.
    They may be modified or removed in future versions.
    Please contact us if you need features from these modules.  *)

(** Generation of annotations. *)
module Export = Export

(** Types and operations for the From plugin. *)
module Assigns = Assigns

(** Register hooks called during the analysis with states of the cvalue domain. *)
module Cvalue_callbacks = (Cvalue_callbacks : Cvalue_callbacks_sig.API)

(** Interpretation of predicates and assigns clauses for Inout and From plugins. *)
module Logic_inout = Logic_inout

(** Undocumented. *)
module Eva_results = Eva_results

(** Unit testing. *)
module Unit_tests = Unit_tests