kernel.mli 17.6 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
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

(** Provided services for kernel developers.
    @plugin development guide *)

(* ************************************************************************* *)
(** {2 Log Machinery} *)
(* ************************************************************************* *)

include Plugin.S

(* ************************************************************************* *)
(** {2 Message and warning categories} *)
(* ************************************************************************* *)

val dkey_alpha: category

val dkey_alpha_undo: category

val dkey_asm_contracts: category

val dkey_ast: category

val dkey_check: category

46
47
val dkey_constfold: category

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
val dkey_comments: category

val dkey_compilation_db: category

val dkey_dataflow: category

val dkey_dataflow_scc: category

val dkey_dominators: category

val dkey_emitter: category

val dkey_emitter_clear: category

val dkey_exn_flow: category

val dkey_file_transform: category

val dkey_file_print_one: category

val dkey_file_annot: category

val dkey_filter: category

val dkey_globals: category

val dkey_kf_blocks: category

val dkey_linker: category

val dkey_linker_find: category

val dkey_loops: category

val dkey_parser: category

val dkey_pp: category

val dkey_print_attrs: category

val dkey_print_bitfields: category

val dkey_print_builtins: category

val dkey_print_logic_coercions: category

val dkey_print_logic_types: category

val dkey_print_sid: category

val dkey_print_unspecified: category

val dkey_print_vid: category

102
103
val dkey_print_field_offsets: category

104
105
106
107
108
109
110
111
112
113
114
115
val dkey_prop_status: category

val dkey_prop_status_emit: category

val dkey_prop_status_merge: category

val dkey_prop_status_graph: category

val dkey_prop_status_reg: category

val dkey_rmtmps: category

116
117
val dkey_referenced: category

118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
val dkey_task: category

val dkey_typing_global: category

val dkey_typing_init: category

val dkey_typing_chunk: category

val dkey_typing_cast: category

val dkey_typing_pragma: category

val dkey_ulevel: category

val dkey_visitor: category

val wkey_annot_error: warn_category
(** error in annotation. If only a warning, annotation will just be ignored. *)

137
138
139
140
val wkey_ghost_already_ghost: warn_category
(** ghost element is qualified with \ghost while this is already the case
    by default *)

141
142
143
val wkey_ghost_bad_use: warn_category
(** error in ghost code *)

144
145
val wkey_acsl_float_compare: warn_category

146
147
148
149
val wkey_conditional_feature: warn_category
(** parsing feature that is only supported in specific modes
    (e.g. C11, gcc, ...). *)

150
151
152
153
154
155
156
157
val wkey_drop_unused: warn_category

val wkey_implicit_conv_void_ptr: warn_category

val wkey_incompatible_types_call: warn_category

val wkey_incompatible_pointer_types: warn_category

158
159
val wkey_inconsistent_specifier: warn_category

160
161
val wkey_int_conversion: warn_category

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
val wkey_cert_exp_46: warn_category

val wkey_cert_msc_38: warn_category

val wkey_cert_exp_10: warn_category

val wkey_check_volatile: warn_category

val wkey_jcdb: warn_category

val wkey_implicit_function_declaration: warn_category

val wkey_no_proto: warn_category

val wkey_missing_spec: warn_category

val wkey_decimal_float: warn_category

val wkey_acsl_extension: warn_category

val wkey_cmdline: warn_category
(** Command-line related warning, e.g. for invalid options given by the user *)

(* ************************************************************************* *)
(** {2 Functors for late option registration}                                *)
(** Kernel_function-related options cannot be registered in this module:
    They depend on [Globals], which is linked later. We provide here functors
    to declare them after [Globals] *)
(* ************************************************************************* *)

module type Input_with_arg = sig
  include Parameter_sig.Input_with_arg
  val module_name: string
end

module Kernel_function_set(X:Input_with_arg): Parameter_sig.Kernel_function_set

(* ************************************************************************* *)
(** {2 Option groups} *)
(* ************************************************************************* *)

val inout_source: Cmdline.Group.t

val saveload: Cmdline.Group.t

val parsing: Cmdline.Group.t

val normalisation: Cmdline.Group.t

val analysis_options: Cmdline.Group.t

val seq: Cmdline.Group.t

val project: Cmdline.Group.t

val checks: Cmdline.Group.t

(* ************************************************************************* *)
(** {2 Installation Information} *)
(* ************************************************************************* *)

module PrintConfig: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
224
(** Behavior of option "-print-config" *)
225
226

module PrintVersion: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
227
(** Behavior of option "-print-version" *)
228
229

module PrintShare: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
230
(** Behavior of option "-print-share-path" *)
231
232

module PrintLib: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
233
(** Behavior of option "-print-lib-path" *)
234
235

module PrintPluginPath: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
236
(** Behavior of option "-print-plugin-path" *)
237

238
239
240
module AutocompleteHelp: Parameter_sig.String_set
(** Behavior of option "-autocomplete" *)

241
module PrintConfigJson: Parameter_sig.Bool
242
(** Behavior of option "-print-config-json"
243
    @since 22.0-Titanium *)
244

245
246
247
248
249
(* ************************************************************************* *)
(** {2 Output Messages} *)
(* ************************************************************************* *)

module GeneralVerbose: Parameter_sig.Int
Michele Alberti's avatar
Michele Alberti committed
250
(** Behavior of option "-verbose" *)
251
252

module GeneralDebug: Parameter_sig.Int
Michele Alberti's avatar
Michele Alberti committed
253
(** Behavior of option "-debug" *)
254
255

module Quiet: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
256
(** Behavior of option "-quiet" *)
257

258
259
260
module Permissive: Parameter_sig.Bool
(** Behavior of option "-permissive" *)

261
262
263
264
265
266
267
268
269
270
(** @plugin development guide *)
module Unicode: sig
  include Parameter_sig.Bool
  val without_unicode: ('a -> 'b) -> 'a -> 'b
  (** Execute the given function as if the option [-unicode] was not set. *)
end
(** Behavior of option "-unicode".
    @plugin development guide *)

module UseUnicode: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
271
272
(** Behavior of option "-unicode"
    @deprecated since Nitrogen-20111001 use module {!Unicode} instead. *)
273
274

module Time: Parameter_sig.String
Michele Alberti's avatar
Michele Alberti committed
275
(** Behavior of option "-time" *)
276
277
278
279
280
281

(* ************************************************************************* *)
(** {2 Input / Output Source Code} *)
(* ************************************************************************* *)

module PrintCode : Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
282
(** Behavior of option "-print" *)
283
284

module PrintMachdep : Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
285
286
(** Behavior of option "-print-machdep"
    @since Phosphorus-20170501-beta1 *)
287
288

module PrintLibc: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
289
290
(** Behavior of option "-print-libc"
    @since Phosphorus-20170501-beta1 *)
291
292

module PrintComments: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
293
(** Behavior of option "-keep-comments" *)
294
295

module PrintReturn : Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
296
297
(** Behavior of option "-print-return"
    @since Sulfur-20171101 *)
298
299
300
301
302
303
304
305
306
307
308
309
310

(** Behavior of option "-ocode".
    @plugin development guide *)
module CodeOutput : sig
  include Parameter_sig.String
  val output: (Format.formatter -> unit) -> unit
end

(** Behavior of option "-add-symbolic-path"
    @since Neon-20140301 *)
module SymbolicPath: Parameter_sig.String_set

module FloatNormal: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
311
(** Behavior of option "-float-normal" *)
312
313

module FloatRelative: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
314
(** Behavior of option "-float-relative" *)
315
316

module FloatHex: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
317
(** Behavior of option "-float-hex" *)
318
319

module BigIntsHex: Parameter_sig.Int
Michele Alberti's avatar
Michele Alberti committed
320
(** Behavior of option "-hexadecimal-big-integers" *)
321
322
323
324
325

(* ************************************************************************* *)
(** {2 Save/Load} *)
(* ************************************************************************* *)

326
module SaveState: Parameter_sig.Filepath
Michele Alberti's avatar
Michele Alberti committed
327
(** Behavior of option "-save" *)
328

329
module LoadState: Parameter_sig.Filepath
Michele Alberti's avatar
Michele Alberti committed
330
(** Behavior of option "-load" *)
331
332

module LoadModule: Parameter_sig.String_list
Michele Alberti's avatar
Michele Alberti committed
333
(** Behavior of option "-load-module" *)
334
335

module AutoLoadPlugins: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
336
(** Behavior of option "-autoload-plugins" *)
337
338
339
340
341

(** Kernel for journalization. *)
module Journal: sig

  module Enable: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
342
  (** Behavior of option "-journal-enable" *)
343
344

  module Name: Parameter_sig.String
Michele Alberti's avatar
Michele Alberti committed
345
  (** Behavior of option "-journal-name" *)
346
347
348
349

end

module Session_dir: Parameter_sig.String
Michele Alberti's avatar
Michele Alberti committed
350
(** Directory in which session files are searched.
351
352
353
    @since Neon-20140301 *)

module Config_dir: Parameter_sig.String
Michele Alberti's avatar
Michele Alberti committed
354
(** Directory in which config files are searched.
355
356
357
358
359
    @since Neon-20140301 *)

(* this stop special comment does not work as expected (and as explained in the
   OCamldoc manual, Section 15.2.2. It just skips all the rest of the file
   instead of skipping until the next stop comment...
Michele Alberti's avatar
Michele Alberti committed
360
361
   (**/**)
*)
362
363
364
365
366

module Set_project_as_default: Parameter_sig.Bool
(** Undocumented. *)

(* See (meta-)comment on the previous stop comment
Michele Alberti's avatar
Michele Alberti committed
367
368
   (**/**)
*)
369
370
371
372
373
374

(* ************************************************************************* *)
(** {2 Customizing Normalization and parsing} *)
(* ************************************************************************* *)

module UnrollingLevel: Parameter_sig.Int
Michele Alberti's avatar
Michele Alberti committed
375
(** Behavior of option "-ulevel" *)
376
377

module UnrollingForce: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
378
379
(** Behavior of option "-ulevel-force"
    @since Neon-20140301 *)
380
381
382
383
384
385

(** Behavior of option "-machdep".
    If function [set] is called, then {!File.prepare_from_c_files} must be
    called for well preparing the AST. *)
module Machdep: Parameter_sig.String

Virgile Prevosto's avatar
Virgile Prevosto committed
386
(** Behavior of invisible option -keep-logical-operators:
387
388
389
390
391
392
393
394
395
396
397
    Tries to avoid converting && and || into conditional statements.
    Note that this option is incompatible with many (most) plug-ins of the
    platform and thus should only be enabled with great care and for very
    specific analyses need.
*)
module LogicalOperators: Parameter_sig.Bool

(** Behavior of option "-enums" *)
module Enums: Parameter_sig.String

module CppCommand: Parameter_sig.String
Michele Alberti's avatar
Michele Alberti committed
398
(** Behavior of option "-cpp-command" *)
399
400

module CppExtraArgs: Parameter_sig.String_list
Michele Alberti's avatar
Michele Alberti committed
401
(** Behavior of option "-cpp-extra-args" *)
402

403
404
405
module CppExtraArgsPerFile: Parameter_sig.Filepath_map with type value = string
(** Behavior of option "-cpp-extra-args-per-file" *)

406
module CppGnuLike: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
407
(** Behavior of option "-cpp-frama-c-compliant" *)
408

409
410
411
module PrintCppCommands: Parameter_sig.Bool
(** Behavior of option "-print-cpp-commands" *)

412
module FramaCStdLib: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
413
(** Behavior of option "-frama-c-stdlib" *)
414
415

module ReadAnnot: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
416
(** Behavior of option "-read-annot" *)
417
418

module PreprocessAnnot: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
419
(** Behavior of option "-pp-annot" *)
420
421

module ContinueOnAnnotError: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
422
(** Behavior of option "-continue-annot-error" *)
423
424
425
[@@ deprecated "Use Kernel.wkey_annot_error instead"]

module SimplifyCfg: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
426
(** Behavior of option "-simplify-cfg" *)
427
428

module KeepSwitch: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
429
(** Behavior of option "-keep-switch" *)
430
431

module Keep_unused_specified_functions: Parameter_sig.Bool
432
433
434
435
(** Behavior of option "-keep-unused-specified-functions". *)

module Keep_unused_types: Parameter_sig.Bool
(** Behavior of option "-keep-unused-types". *)
436
437
438
439
440

module SimplifyTrivialLoops: Parameter_sig.Bool
(** Behavior of option "-simplify-trivial-loops". *)

module Constfold: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
441
(** Behavior of option "-constfold" *)
442
443

module InitializedPaddingLocals: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
444
(** Behavior of option "-initialized-padding-locals" *)
445
446

module AggressiveMerging: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
447
(** Behavior of option "-aggressive-merging" *)
448
449

module AsmContractsGenerate: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
450
(** Behavior of option "-asm-contracts" *)
451
452

module AsmContractsAutoValidate: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
453
(** Behavior of option "-asm-contracts-auto-validate." *)
454
455

module RemoveExn: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
456
(** Behavior of option "-remove-exn" *)
457
458

(** Analyzed files *)
459
module Files: Parameter_sig.Filepath_list
460
461
462
463
464
465
466
467
468
469
(** List of files to analyse *)

module Orig_name: Parameter_sig.Bool
(** Behavior of option "-orig-name" *)

val normalization_parameters: unit -> Typed_parameter.t list
(** All the normalization options that influence the AST (in particular,
    changing one will reset the AST entirely.contents

    @modify Chlorine-20180501 make it non-constant
Michele Alberti's avatar
Michele Alberti committed
470
*)
471
472

module WarnDecimalFloat: Parameter_sig.String
Michele Alberti's avatar
Michele Alberti committed
473
(** Behavior of option "-warn-decimal-float" *)
474
475
476
[@@ deprecated "Uses kernel.wkey_decimal_float instead."]

module ImplicitFunctionDeclaration: Parameter_sig.String
Michele Alberti's avatar
Michele Alberti committed
477
(** Behavior of option "-implicit-function-declaration" *)
478
479
480
[@@ deprecated "Uses kernel.wkey_implicit_function_declaration instead."]

module C11: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
481
(** Behavior of option "-c11" *)
482

483
module JsonCompilationDatabase: Parameter_sig.Filepath
Michele Alberti's avatar
Michele Alberti committed
484
(** Behavior of option "-json-compilation-database" *)
485
486
487
488
489
490

(* ************************************************************************* *)
(** {3 Customizing cabs2cil options} *)
(* ************************************************************************* *)

module AllowDuplication: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
491
(** Behavior of option "-allow-duplication". *)
492
493

module DoCollapseCallCast: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
494
(** Behavior of option "-collapse-call-cast".
495

Michele Alberti's avatar
Michele Alberti committed
496
497
498
    If false, the destination of a Call instruction should always have the
    same type as the function's return type.  Where needed, CIL will insert a
    temporary to make this happen.
499

Michele Alberti's avatar
Michele Alberti committed
500
501
502
503
    If true, the destination type may differ from the return type, so there
    is an implicit cast.  This is useful for analyses involving [malloc],
    because the instruction "T* x = malloc(...);" won't be broken into
    two instructions, so it's easy to find the allocation type.
504

Michele Alberti's avatar
Michele Alberti committed
505
506
    This is false by default.  Set to true to replicate the behavior
    of CIL 1.3.5 and earlier. *)
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539

(* ************************************************************************* *)
(** {2 Analysis Behavior of options} *)
(* ************************************************************************* *)

(** Behavior of option "-main".

    You should usually use {!Globals.entry_point} instead of
    {!MainFunction.get} since the first one handles the case where the entry
    point is invalid in the right way. *)
module MainFunction: sig

  include Parameter_sig.String

  (** {2 Internal functions}

      Not for casual users. *)

  val unsafe_set: t -> unit

end

(** Behavior of option "-lib-entry".

    You should usually use {!Globals.entry_point} instead of
    {!LibEntry.get} since the first one handles the case where the entry point
    is invalid in the right way. *)
module LibEntry: sig
  include Parameter_sig.Bool
  val unsafe_set: t -> unit (** Not for casual users. *)
end

module UnspecifiedAccess: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
540
(** Behavior of option "-unspecified-access" *)
541
542

module SafeArrays: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
543
544
(** Behavior of option "-safe-arrays".
    @plugin development guide *)
545
546

module SignedOverflow: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
547
(** Behavior of option "-warn-signed-overflow" *)
548
549

module UnsignedOverflow: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
550
(** Behavior of option "-warn-unsigned-overflow" *)
551
552

module LeftShiftNegative: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
553
(** Behavior of option "-warn-left-shift-negative" *)
554
555

module RightShiftNegative: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
556
(** Behavior of option "-warn-right-shift-negative" *)
557
558

module SignedDowncast: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
559
(** Behavior of option "-warn-signed-downcast" *)
560
561

module UnsignedDowncast: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
562
(** Behavior of option "-warn-unsigned-downcast" *)
563

564
565
566
module PointerDowncast: Parameter_sig.Bool
(** Behavior of option "-warn-pointer-downcast" *)

567
module SpecialFloat: Parameter_sig.String
Michele Alberti's avatar
Michele Alberti committed
568
(** Behavior of option "-warn-special-float" *)
569
570

module InvalidBool: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
571
(** Behavior of option "-warn-invalid-bool" *)
572

573
574
575
module InvalidPointer: Parameter_sig.Bool
(** Behavior of option "-warn-invalid-pointer" *)

576
module AbsoluteValidRange: Parameter_sig.String
Michele Alberti's avatar
Michele Alberti committed
577
(** Behavior of option "-absolute-valid-range" *)
578
579
580
581
582
583
584
585
586
587
588

(*
module FloatFlushToZero: Parameter_sig.Bool
  (** Behavior of option "-float-flush-to-zero" *)
*)

(* ************************************************************************* *)
(** {2 Checks} *)
(* ************************************************************************* *)

module Check: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
589
(** Behavior of option "-check" *)
590
591
592
593
594

module Copy: Parameter_sig.Bool
(** Behavior of option "-copy" *)

module TypeCheck: Parameter_sig.Bool
Michele Alberti's avatar
Michele Alberti committed
595
(** Behavior of option "-typecheck" *)
596
597
598
599
600
601
602


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