package frama-c

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

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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

(** Plug-in states and options. *)

let plugin_name="Volatile"

include Plugin.Register
    (struct
      let name = plugin_name
      let shortname = "volatile"
      let help = "support for volatile accesses and calls through function pointers"
    end)

(** {1 Messages and warning categories} *)

module Keys = struct

  let dkey_binding =
    register_category
      ~help:"Prints debug messages related to volatile operations"
      "binding"

  let dkey_binding_table =
    register_category
      ~help:"Prints debug messages related to volatile operations on internal tables"
      "binding-table"

  let dkey_volatile_table =
    register_category
      ~help:"Prints Volatile internal tables"
      "volatile-table"

  let dkey_transformation_action =
    register_category
      ~help:"Prints information on generated code"
      "transformation-action"

  let dkey_transformation_visit =
    register_category
      ~help:"Prints visitor information during the transformation"
      "transformation-visit"

  let wkey name status =
    let wkey = register_warn_category name in
    set_warn_status wkey status;
    wkey

  let wkey_invalid_binding_function =
    wkey "invalid-binding-function" Log.Werror
  let wkey_unsupported_volatile_clause =
    wkey "unsupported:volatile-clause" Log.Werror
  let wkey_duplicated_access_function =
    wkey "duplicated-access-function" Log.Werror

  let wkey_volatile_cast = wkey "cast:volatile" Log.Wfeedback
  let wkey_cast_insertion =
    wkey "cast:insertion" Log.Wfeedback

  let wkey_transformed_access_lvalue_volatile =
    wkey "transformed-access:lvalue-volatile" Log.Wfeedback
  let wkey_transformed_access_lvalue_partially_volatile =
    wkey "transformed-access:lvalue-partially-volatile" Log.Wfeedback

  let wkey_untransformed_access_lvalue_volatile =
    wkey "untransformed-access:lvalue-volatile" Log.Wactive
  let wkey_untransformed_access_lvalue_partially_volatile =
    wkey "untransformed-access:lvalue-partially-volatile" Log.Wactive

  let wkey_untransformed_call = wkey "untransformed-call" Log.Wactive
  let wkey_untransformed_call_function_not_found =
    wkey "untransformed-call:function_not_found" Log.Wactive

  let wkey_transformed_call = wkey "transformed-call" Log.Wfeedback
  let wkey_transformed_call_skipped_parameters =
    wkey "transformed-call:skipped-parameters" Log.Wactive
  let wkey_transformed_call_missing_parameters =
    wkey "transformed-call:missing-parameters" Log.Wactive

end

(** {1 Plug-in options.} *)

module Enabled =
  False (struct
    let option_name = "-volatile"
    let help =
      "builds a new project (named \"" ^ plugin_name
      ^"\") where volatile accesses are simulated by function calls"
  end)

module Process =
  String_set (struct
    let option_name = "-volatile-fct"
    let arg_name = "f,..."
    let help = "Only process the given function(s)"
  end)

module CallPtr =
  String_list (struct
    let option_name = "-volatile-call-pointer"
    let arg_name = "f,..."
    let help = "stub call to pointer functions to the provided functions \
                (indexed by type)"
  end)

module Base =
  False (struct
    let option_name = "-volatile-basetype"
    let help = "use base-type for int, float and enums for the instrumentation \
                related to -volatile-binding option"
  end)

module Binding =
  String_list (struct
    let option_name = "-volatile-binding"
    let arg_name = "f,..."
    let help = "allows binding of volatile accesses to functions <f,...>"
  end)

module BindingAuto =
  False (struct
    let option_name = "-volatile-binding-auto"
    let help = "allows automatic binding of volatiles accesses to functions: \
                <prefix>Rd_<typename> and <prefix>Wr_<typename>"
  end)

module BindingCall =
  False (struct
    let option_name = "-volatile-binding-call-pointer"
    let help = "replaces calls through function pointers by direct calls to \
                functions: <prefix>Call_<result-type>_<param-types>"
  end)

module BindingPrefix =
  String (struct
    let option_name = "-volatile-binding-prefix"
    let arg_name = "str"
    let default = "c2fc2_"
    let help = "adds <str> as prefix to function names for automatic binding"
  end)
let () = BindingPrefix.add_set_hook
    (fun _t -> function
       | "" -> error "empty string cannot be used as binding prefix@."
       | str ->  let rx = Str.regexp "^[a-zA-Z_][a-zA-Z0-9_$]*$" in
         if (not (Str.string_match rx str 0)) then
           error "binding prefix %S does not match C identifier regexp@."str;
    )