package frama-c

  1. Overview
  2. Docs

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
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

(** Eva public API.

    The main modules are:
    - Analysis: run the analysis.
    - Results: access analysis results, especially the values of expressions
      and memory locations of lvalues at each program point.

    The following modules allow configuring the Eva analysis:
    - Parameters: change the configuration of the analysis.
    - Eva_annotations: add local annotations to guide the analysis.
    - Builtins: register ocaml builtins to be used by the cvalue domain
      instead of analysing the body of some C functions.

    Other modules are for internal use only. *)
(* This file is generated. Do not edit. *)

module Analysis = Analysis
module Callstack = Callstack
module Deps = Deps
module Results = Results
module Parameters = Parameters
module Eva_perf = Eva_perf
module Statistics = Statistics
module Export = Export
module Eva_annotations = Eva_annotations
module Eval = Eval
module Assigns = Assigns
module Eva_ast = Eva_ast
module Builtins = Builtins
module Cvalue_callbacks = Cvalue_callbacks
module Logic_inout = Logic_inout
module Eva_results = Eva_results
module Unit_tests = Unit_tests