package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file dive_types.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2023                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

type node_kind =
  | Scalar of Cil_types.varinfo * Cil_types.typ * Cil_types.offset
  | Composite of Cil_types.varinfo
  | Scattered of Cil_types.lval * Cil_types.stmt
  | Unknown of Cil_types.lval * Cil_types.stmt
  | Alarm of Cil_types.stmt * Alarms.alarm
  | AbsoluteMemory
  | String of int * Base.cstring
  | Const of Cil_types.exp
  | Error of string

type callstack = Callstack.t

type node_locality = {
  loc_file : string;
  loc_callstack : callstack;
}

type node_range =
  | Empty (* No values assigned to the node *)
  | Singleton (* A unique value ever assigned *)
  | Normal of int (* From 0 = almost singleton to 100 = almost all possible values *)
  | Wide (* Too many values for the type to be reasonable *)

type computation = NotDone | Partial of (unit Seq.t) | Done

type origin = Studia.Writes.t

type node = {
  node_key : int;
  node_kind : node_kind;
  node_locality : node_locality;
  mutable node_is_root : bool;
  mutable node_hidden : bool;
  mutable node_values : Cvalue.V.t option;
  mutable node_range : node_range;
  mutable node_taint : Eva.Results.taint option;
  mutable node_writes_computation : computation;
  mutable node_reads_computation : computation;
  mutable node_writes : origin list;
}

type dependency_kind = Callee | Data | Address | Control | Composition

type dependency = {
  dependency_key : int;
  dependency_kind : dependency_kind;
  mutable dependency_origins : origin list;
}

type graph_diff = {
  last_root: node option;
  added_nodes: node list;
  removed_nodes: node list;
}

type 'a range = {
  backward: 'a;
  forward: 'a;
}

type window = {
  perception: int option range; (* depth of exploration *)
  horizon: int option range; (* hide beyond horizon ; None for infinite *)
}