package frama-c

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

Source file mt_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
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-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 licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

let () = Plugin.is_share_visible ()
module MThread = Plugin.Register (
  struct
    let name = "mthread"
    let shortname = "mt"
    let help = "Experimental tools for multi-threaded programs"
  end)
;;
(* Including this module directly is a bad idea, as this hides the
   "String" module of the standard library... *)

(* Reexport useful values *)
include (MThread: Log.Messages)

let debug_level () = MThread.Debug.get ()

open MThread

let grp_models = add_group "Extraction of models"
let grp_debug = add_group "Debug"
let grp_cfg = add_group "Multithreaded control-flow-graph"
(*let grp_misc = add_group "Misc"*)
let grp_analysis = add_group "Analysis"

module Enabled =
  False (struct
    let option_name = "-mthread"
    let help = "enable analysis of multi-threaded programs through the Mthread plugin"
  end)
;;

let () = Parameter_customize.set_group grp_debug
module KeepProjects =
  String (struct
    let option_name = "-mt-keep-analyses"
    let help = "keep a copy of the analyses done for each thread"
    let default = "last"
    let arg_name = "all|last|none"
  end)
;;
let () = KeepProjects.set_possible_values ["all"; "last"; "none"]

let () = Parameter_customize.set_group grp_debug
let () = Parameter_customize.set_negative_option_name "-mt-projects-together"
module ToDisk =
  False (struct
    let option_name = "-mt-projects-on-disk"
    let help = "Save the copies of the analyses in a separate file, instead of all together"
  end)
;;

let () = Parameter_customize.set_group grp_debug
let () = Parameter_customize.set_negative_option_name "-mt-consider-null"
module IgnoreNull =
  False (struct
    let option_name = "-mt-ignore-null"
    let help = "Ignore shared accesses to numeric memory (NULL base)"
  end)
;;


let () = Parameter_customize.set_group grp_debug
module ToDiskPrefix =
  String
    (struct
      let option_name = "-mt-projects-on-disk-prefix"
      let arg_name = "prefix"
      let default = "th"
      let help = "Prepend <prefix> to the project's filename saved by -mt-projects-on-disk (defaults to th)"
    end)



let () = Parameter_customize.set_group grp_analysis
module WriteWriteRaces =
  False (struct
    let option_name = "-mt-write-races"
    let help = "Display memory on which there is a write-only race condition"
  end)

let () = Parameter_customize.set_group grp_analysis
module DumpSharedVarsValues =
  Int (struct
    let default = 0
    let option_name = "-mt-shared-values"
    let help = "Show what threads read and write in shared memory at the end of each iteration\n\
                0: values not shown\n\
                1: values shown\n\
                2: values shown with the stack at which the operation occurs"
    let arg_name = "level"
  end)
let () = DumpSharedVarsValues.set_range ~min:0 ~max:2

let () = Parameter_customize.set_group grp_analysis
module CheckProtections =
  False (struct
    let help = "more precise inference of which mutexes protect shared memory"
    let option_name = "-mt-shared-accesses-synchronization"
  end)

let () = Parameter_customize.set_group grp_analysis
module InterruptHandlers =
  Kernel_function_set (struct
    let option_name = "-mt-interrupt-handlers"
    let arg_name = "functions"
    let help = "Specify functions that will be treated as handlers for \
                interrupts."
  end)

let () = Parameter_customize.set_group messages
module ModerateWarnings =
  True (struct
    let option_name = "-mt-moderate-warnings"
    let help = "Show semi-important warnings during analysis."
  end)

let () = Parameter_customize.set_group messages
module PrintCallstacks  =
  False (struct
    let option_name = "-mt-print-callstacks"
    let help = "Print the callstacks at which concurrent events occur"
  end)

let () = Parameter_customize.set_group grp_debug
module ShowTime =
  False (struct
    let option_name = "-mt-time"
    let help = "Show time taken by thread computation"
  end)
;;

let () = Parameter_customize.set_group grp_debug
module SkipThreads =
  String_set
    (struct
      let option_name = "-mt-skip-threads"
      let arg_name = "th1,...,thn"
      let help = "do not execute the specified threads"
    end)
;;

let () = Parameter_customize.set_group grp_debug
module OnlyThreads =
  String_set
    (struct
      let option_name = "-mt-only-threads"
      let arg_name = "th1,...,thn"
      let help = "only execute the specified threads"
    end)
;;



let () = Parameter_customize.set_group grp_debug
module StopAfter =
  Int (struct
    let default = max_int
    let option_name = "-mt-stop-after"
    let help = "Only perform at most i iterations"
    let arg_name = "i"
  end)
;;


let () = Parameter_customize.set_group grp_debug
module ConcatDotFilesTo =
  Filepath
    (struct
      let option_name = "-mt-concat-dot-files-to"
      let arg_name = "filename"
      let existence = Fc_Filepath.Indifferent
      let file_kind = "dot"
      let help = "Concatenate dot files generated by the html output into a \
                  single file."
    end)


let () = Parameter_customize.set_group grp_models
module ExtractModels =
  String_set
    (struct
      let option_name = "-mt-extract"
      let arg_name = "[html]"
      let help = "extraction of models"
    end)
;;

let () = Parameter_customize.set_group grp_cfg
module FullCfg =
  False (struct
    let option_name = "-mt-full-cfg"
    let help = "Do not simplify cfg and show all statements (can be costly)"
  end)
;;

let () = Parameter_customize.set_group grp_cfg
module KeepWhiteNodes =
  False (struct
    let option_name = "-mt-non-shared-accesses"
    let help = "Keep accesses to false shared variables in the cfg"
  end)
;;

let () = Parameter_customize.set_group grp_cfg
module KeepGreenNodes =
  True (struct
    let option_name = "-mt-non-concurrent-accesses"
    let help = "Keep non-concurrent accesses to shared variables in the cfg"
  end)
;;

let () = Parameter_customize.set_group grp_cfg
module ShowReturnEdges =
  True (struct
    let option_name = "-mt-return-edges"
    let help = "Show link between a call an a return instruction as a dotted line"
  end)
;;

let () = Parameter_customize.set_group grp_cfg
module PopTopFunctionForCallbacks =
  False (struct
    let option_name = "-mt-inline-callbacks"
    let help = "Do not show the names of concurrent primitives, only their effect"
  end)
;;
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct