Source file meta_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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's MetACSL plug-in.                   *)
(*                                                                        *)
(*  Copyright (C) 2018-2025                                               *)
(*    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 LICENSE)                       *)
(*                                                                        *)
(**************************************************************************)

let help_msg = "This plugin translates the metaproperties in the code to native ACSL annotations" ^
               "that can then be checked."

let () = Plugin.is_share_visible()
module Self = Plugin.Register (struct
    let name = "MetAcsl"
    let shortname = "meta"
    let help = help_msg
  end)

let () = Parameter_customize.do_not_projectify ()
module Enabled = Self.False (struct
    let option_name = "-meta"
    let help = "Enable translation of metaproperties"
  end)

module Check_External = Self.True (struct
    let option_name = "-meta-check-ext"
    let help = "Calls to external functions (such as memcpy) are treated as \
                modifying/accessing the state inside the caller's body"
  end)

let () = Parameter_customize.argument_may_be_fundecl()
module Check_Callee_Assigns = Self.Kernel_function_set (struct
    let option_name = "-meta-check-callee-assigns"
    let arg_name = "f,..."
    let help = "Reading and writing metaproperties are instantiated for calls \
                to listed functions from non-listed ones based on the \
                assigns...from clauses of the callee (possibly in addition to \
                their instantiation inside the callee when it is in the target set)."
  end)

module Targets = Self.String_set (struct
    let option_name = "-meta-set"
    let arg_name = "targets"
    let help = "Define the set of meta-properties to process. Defaults to \
                every meta-property"
  end)

module Simpl = Self.True (struct
    let option_name = "-meta-simpl"
    let help = "Discard annotations that are obviously true"
  end)

module Number_assertions = Self.False (struct
    let option_name = "-meta-number-assertions"
    let help = "Add an unique number to each instance of a meta-propery."
  end)

module Prefix_meta = Self.True (struct
    let option_name = "-meta-add-prefix"
    let help = "Prefix meta: to the name of each generated property."
  end)

module List_targets = Self.False (struct
    let option_name = "-meta-list-targets"
    let help = "Detail the list of targets for every meta-property"
  end)

module Keep_proof_files = Self.False (struct
    let option_name = "-meta-keep-proof-files"
    let help = "Keep .why files after deduction attempts"
  end)

module Static_bindings = Self.Int (struct
    let option_name = "-meta-static-bindings"
    let arg_name = "array_size"
    let default = 0
    let help = "Use static arrays with the given size for bindings instead \
                of dynamic arrays"
  end)

module Separate_annots = Self.False (struct
    let option_name = "-meta-separate-annots"
    let help =
      "When set, each generated statement annotation will be tied to its own \
       (nop) instruction. Otherwise (default), all annotations generated for \
       a given statement will be tied to this statement."
  end)

let () = Parameter_customize.set_negative_option_name "-meta-checks"
module Default_to_assert = Self.True (struct
    let option_name = "-meta-asserts"
    let help = "Default to using assertions instead of checks when translating, \
                unless specified otherwise in a meta-property"
  end)

let unknown_func_wkey = Self.register_warn_category "unknown-func"
let () = Self.set_warn_status unknown_func_wkey Log.Wabort

type meta_flags = {
  check_external : bool;
  check_callee_assigns: Kernel_function.Set.t;
  simpl : bool;
  static_bindings : int option;
  target_set : Meta_utils.StrSet.t option;
  number_assertions : bool;
  prefix_meta : bool;
  list_targets : bool;
  keep_proof_files : bool;
  default_to_assert : bool;
}