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

let help_msg = "generates annotations for runtime error checking"

include Plugin.Register
    (struct
      let name = "RteGen"
      let shortname = "rte"
      let help = help_msg
    end)

(* enabling/disabling plugin *)
module Enabled =
  False
    (struct
      let option_name = "-rte"
      let help = "when on (off by default), " ^ help_msg
    end)

(* annotates division by zero (undefined behavior) *)
module DoDivMod =
  True
    (struct
      let option_name = "-rte-div"
      let help = "when on (default), annotate for modulo and division by zero"
    end)

(* annotates left and right shifts (undefined behavior) *)
module DoShift =
  True
    (struct
      let option_name = "-rte-shift"
      let help = "when on (default), annotate for left and right shifts by a value out of bounds"
    end)

(* annotates casts from floating-point to integer (undefined behavior) *)
module DoFloatToInt =
  True
    (struct
      let option_name = "-rte-float-to-int"
      let help = "when on (default), annotate casts from floating-point to \
                  integer"
    end)

(* annotates local variables and pointers read (aside from globals) initialization *)
module DoInitialized =
  Kernel_function_set
    (struct
      let option_name = "-rte-initialized"
      let arg_name = "fct"
      let help = "for each function in 'fct', annotates reads of non struct or \
                  union values from local variables and pointers with \
                  initialization tests, see documentation for more details"
    end)

(* annotates invalid memory access (undefined behavior) *)
module DoMemAccess =
  True
    (struct
      let option_name = "-rte-mem"
      let help = "when on (default), annotate for valid pointer or \
                  array access"
    end)

(* annotates calls through pointers *)
module DoPointerCall =
  True
    (struct
      let option_name = "-rte-pointer-call"
      let help = "when on, annotate functions calls through pointers"
    end)

(* uses results of basic constant propagation in order to check
   validity / invalidity of generated assertions, emitting a status if possible.
   Notice that annotations that can be considered valid from syntactical rules
   are also considered as trivial.
*)
module Trivial =
  False
    (struct
      let option_name = "-rte-trivial-annotations"
      let help = "generate all annotations even if they trivially hold \
                  (from evaluation of constant expressions, syntactical rules...)"
      (* if on, evaluates constants in order to check if assertions
         are trivially true / false *)
    end)

(* emits a warning when an assertion generated by rte is clearly invalid
   (using constant folding, see ConstFold *)
module Warn =
  True
    (struct
      let option_name = "-rte-warn"
      let help = "when on (default), emits warning on broken asserts"
    end)

(* this option allows the user to select a set of functions on which
   the plug-in performs its jobs (and only those).
   By default all functions are annotated *)
module FunctionSelection =
  Kernel_function_set
    (struct
      let option_name = "-rte-select"
      let arg_name = "fun"
      let help = "select <fun> for analysis (default all functions)"
    end)

let dkey_annot =
  register_category "annot" ~default:true
    ~help:"message about function annotations"

let () =
  if not Eva_analysis.is_available
  then Parameter_customize.is_invisible ()

module UseEvaResults =
  Bool
    (struct
      let option_name  = "-rte-use-eva-results"
      let default = Eva_analysis.is_available
      let help =
        "When enabled, do not emit annotations on functions analyzed by Eva"
    end)

let use_eva_results () =
  if UseEvaResults.get () && not Eva_analysis.is_available then
    warning ~once:true
      "-rte-use-eva-results is set while Eva is not available, ignoring" ;
  UseEvaResults.get ()