package frama-c

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

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

open Cil_types

include Plugin.Register
    (struct
      let name = "dive"
      let shortname = "dive"
      let help = "An interactive imprecision graph generator for Eva."
    end)

module OutputDot = Filepath
    (struct
      let option_name = "-dive-output-dot"
      let arg_name = "output.dot"
      let file_kind = "DOT"
      let existence = Fclib.Filepath.Indifferent
      let help = "Outputs the built graph in DOT format to the specified file."
    end)

module OutputJson = Filepath
    (struct
      let option_name = "-dive-output-json"
      let arg_name = "output.json"
      let file_kind = "JSON"
      let existence = Fclib.Filepath.Indifferent
      let help = "Outputs the built graph in JSON format to the specified."
    end)

module DepthLimit = Int
    (struct
      let option_name = "-dive-depth-limit"
      let help = "Build dependencies up to a depth of N."
      let arg_name = "N"
      let default = 3
    end)

module FromFunctionAlarms = Kernel_function_set
    (struct
      let option_name = "-dive-from-alarms"
      let help = "Build the graph from the alarms emitted in the given functions."
      let arg_name = "f1,..."
    end)

module Varinfo =
struct
  include Cil_datatype.Varinfo

  let of_string s =
    let regexp = Str.regexp "^\\([_a-zA-Z0-9]+\\)::\\([_a-zA-Z0-9]+\\)$" in
    if Str.string_match regexp s 0 then
      let function_name = Str.matched_group 1 s
      and variable_name = Str.matched_group 2 s in
      let kf = try Globals.Functions.find_by_name function_name
        with Not_found ->
          raise (Cannot_build ("no function '" ^ function_name ^ "'"))
      in
      try [ Globals.Vars.find_from_astinfo variable_name (Whole_function kf) ]
      with Not_found ->
      try [ Globals.Vars.find_from_astinfo variable_name (Formal kf) ]
      with Not_found ->
        raise (Cannot_build ("no variable '" ^ variable_name ^ "' in function "
                             ^ function_name))
    else
      let regexp = Str.regexp "^[_a-zA-Z0-9]+$" in
      if not (Str.string_match regexp s 0) then
        raise (Cannot_build ("wrong syntax: '" ^ s ^ "'"));
      match Globals.Syntactic_search.find_in_scope s Cil_types.Program with
      | Some vi -> [ vi ]
      | None ->
        raise (Cannot_build ("no global variable '" ^ s ^ "'"))

  let to_string vi =
    match Kernel_function.find_defining_kf vi with
    | None -> vi.vname
    | Some kf -> Kernel_function.get_name kf ^ "::" ^ vi.vname
end

module type Varinfo_set = Parameter_sig.Set
  with type elt = Cil_types.varinfo
   and type t = Cil_datatype.Varinfo.Set.t

module Varinfo_set (X: Parameter_sig.Input_with_arg) =
  Make_set
    (Varinfo)
    (struct
      include X
      let dependencies = []
      let default = Cil_datatype.Varinfo.Set.empty
    end)

module FromBases = Varinfo_set
    (struct
      let option_name = "-dive-from-variables"
      let help = "Build the graph from these local variables."
      let arg_name = "f::v,..."
    end)

module UnfoldedBases = Varinfo_set
    (struct
      let option_name = "-dive-unfold"
      let help = "Defines the composite variables which should be \
                  unfolded into individual cells."
      let arg_name = "f::v,..."
    end)

module HiddenBases = Varinfo_set
    (struct
      let option_name = "-dive-hide"
      let help = "Defines the variables which must not be \
                  displayed in the graph. The dependencies for these bases \
                  are not computed either."
      let arg_name = "f::v,..."
    end)