metrics_parameters.ml 4.05 KB
Newer Older
1
2
3
4
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
Andre Maroneze's avatar
Andre Maroneze committed
5
(*  Copyright (C) 2007-2020                                               *)
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
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

include Plugin.Register
    (struct
       let name = "metrics"
       let shortname = "metrics"
       let help = "syntactic metrics"
     end)

module Enabled =
  WithOutput
    (struct
      let option_name = "-metrics"
      let help = "activate metrics computation"
      let output_by_default = true
     end)

module ByFunction =
  WithOutput
    (struct
      let option_name = "-metrics-by-function"
      let help = "also compute metrics on a per-function basis"
      let output_by_default = true
     end)

module OutputFile =
  Empty_string
    (struct
      let option_name = "-metrics-output"
      let arg_name = "filename"
      let help = "print some metrics into the specified file; \
52
53
                  the output format is recognized through the extension: \
                  .text/.txt for text, .html/.htm for HTML, or .json for JSON."
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
     end)

module ValueCoverage =
  WithOutput (
    struct
      let option_name = "-metrics-eva-cover"
      let help = "estimate Eva coverage w.r.t. \
                  to reachable syntactic definitions"
      let output_by_default = true
    end)
let () = ValueCoverage.add_aliases [ "-metrics-value-cover" ]

module AstType =
  String
    (struct
      let option_name = "-metrics-ast"
      let arg_name = "[cabs | cil | acsl]"
      let help = "apply metrics to Cabs or CIL AST, or to ACSL specs"
      let default = "cil"
     end
    )

module Libc =
  False
    (struct
      let option_name = "-metrics-libc"
      let help = "show functions from Frama-C standard C library in the \
                  results; deactivated by default."
     end
    )


let () = AstType.set_possible_values ["cil"; "cabs"; "acsl"]

module SyntacticallyReachable =
  Kernel_function_set
    (struct
      let option_name = "-metrics-cover"
      let arg_name = "f1,..,fn"
      let help = "compute an overapproximation of the functions reachable from \
                  f1,..,fn."
     end
    )

module LocalsSize =
  Kernel_function_set
    (struct
      let option_name = "-metrics-locals-size"
      let arg_name = "f1,...,fn"
      let help = "prints the size of local variables for functions f1,...,fn, \
                  and for the functions called within them \
                  (does not support recursive calls)"
    end)

module UsedFiles =
  False
    (struct
      let option_name = "-metrics-used-files"
      let help = "list files containing global definitions reachable by main"
    end)

(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)