cil.mli 88.6 KB
Newer Older
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
(****************************************************************************)
(*                                                                          *)
(*  Copyright (C) 2001-2003                                                 *)
(*   George C. Necula    <necula@cs.berkeley.edu>                           *)
(*   Scott McPeak        <smcpeak@cs.berkeley.edu>                          *)
(*   Wes Weimer          <weimer@cs.berkeley.edu>                           *)
(*   Ben Liblit          <liblit@cs.berkeley.edu>                           *)
(*  All rights reserved.                                                    *)
(*                                                                          *)
(*  Redistribution and use in source and binary forms, with or without      *)
(*  modification, are permitted provided that the following conditions      *)
(*  are met:                                                                *)
(*                                                                          *)
(*  1. Redistributions of source code must retain the above copyright       *)
(*  notice, this list of conditions and the following disclaimer.           *)
(*                                                                          *)
(*  2. Redistributions in binary form must reproduce the above copyright    *)
(*  notice, this list of conditions and the following disclaimer in the     *)
(*  documentation and/or other materials provided with the distribution.    *)
(*                                                                          *)
(*  3. The names of the contributors may not be used to endorse or          *)
(*  promote products derived from this software without specific prior      *)
(*  written permission.                                                     *)
(*                                                                          *)
(*  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS     *)
(*  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT       *)
(*  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS       *)
(*  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE          *)
(*  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,     *)
(*  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,    *)
(*  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;        *)
(*  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER        *)
(*  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT      *)
(*  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN       *)
(*  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE         *)
(*  POSSIBILITY OF SUCH DAMAGE.                                             *)
(*                                                                          *)
(*  File modified by CEA (Commissariat à l'énergie atomique et aux          *)
(*                        énergies alternatives)                            *)
(*               and INRIA (Institut National de Recherche en Informatique  *)
(*                          et Automatique).                                *)
(****************************************************************************)

(** CIL main API.

    CIL original API documentation is available as
    an html version at http://manju.cs.berkeley.edu/cil.

    @plugin development guide *)

open Cil_types
open Cil_datatype

(* ************************************************************************* *)
(** {2 Builtins management} *)
(* ************************************************************************* *)

(** This module associates the name of a built-in function that might be used
    during elaboration with the corresponding varinfo.  This is done when
    parsing ${FRAMAC_SHARE}/libc/__fc_builtins.h, which is always performed
    before processing the actual list of files provided on the command line (see
    {!File.init_from_c_files}).  Actual list of such built-ins is managed in
    {!Cabs2cil}. *)
64
module Frama_c_builtins:
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
  State_builder.Hashtbl with type key = string and type data = Cil_types.varinfo

val is_builtin: Cil_types.varinfo -> bool
(** @return true if the given variable refers to a Frama-C builtin.
    @since Fluorine-20130401 *)

val is_unused_builtin: Cil_types.varinfo -> bool
(** @return true if the given variable refers to a Frama-C builtin that
    is not used in the current program. Plugins may (and in fact should)
    hide this builtin from their outputs *)

val is_special_builtin: string -> bool
(** @return [true] if the given name refers to a special built-in function.
    A special built-in function can have any number of arguments. It is up to
    the plug-ins to know what to do with it.
    @since Carbon-20101201 *)

(** register a new special built-in function *)
val add_special_builtin: string -> unit

(** register a new family of special built-in functions.
    @since Carbon-20101201
*)
val add_special_builtin_family: (string -> bool) -> unit

(** initialize the C built-ins. Should be called once per project, after the
    machine has been set. *)
val init_builtins: unit -> unit

(** Call this function to perform some initialization, and only after you have
    set [Cil.msvcMode]. [initLogicBuiltins] is the function to call to init
    logic builtins. The [Machdeps] argument is a description of the hardware
    platform and of the compiler used. *)
val initCIL: initLogicBuiltins:(unit -> unit) -> Cil_types.mach -> unit

(* ************************************************************************* *)
(** {2 Customization} *)
(* ************************************************************************* *)

type theMachine = private
Allan Blanchard's avatar
Allan Blanchard committed
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
  { mutable useLogicalOperators: bool;
    (** Whether to use the logical operands LAnd and LOr. By default, do not
        use them because they are unlike other expressions and do not
        evaluate both of their operands *)
    mutable theMachine: mach;
    mutable lowerConstants: bool; (** Do lower constants (default true) *)
    mutable insertImplicitCasts: bool;
    (** Do insert implicit casts (default true) *)
    mutable underscore_name: bool;
    (** Whether the compiler generates assembly labels by prepending "_" to
        the identifier. That is, will function foo() have the label "foo", or
        "_foo"? *)
    mutable stringLiteralType: typ;
    mutable upointKind: ikind
  (** An unsigned integer type that fits pointers. *);
    mutable upointType: typ;
    mutable wcharKind: ikind; (** An integer type that fits wchar_t. *)
    mutable wcharType: typ;
    mutable ptrdiffKind: ikind; (** An integer type that fits ptrdiff_t. *)
    mutable ptrdiffType: typ;
    mutable typeOfSizeOf: typ;
    (** An integer type that is the type of sizeof. *)
    mutable kindOfSizeOf: ikind;
    (** The integer kind of {!Cil.typeOfSizeOf}. *)
  }
130
131

val theMachine : theMachine
Allan Blanchard's avatar
Allan Blanchard committed
132
(** Current machine description *)
133
134
135
136

val selfMachine: State.t

val selfMachine_is_computed: ?project:Project.project -> unit -> bool
Allan Blanchard's avatar
Allan Blanchard committed
137
(** whether current project has set its machine description. *)
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

val msvcMode: unit -> bool
val gccMode: unit -> bool


(* ************************************************************************* *)
(** {2 Values for manipulating globals} *)
(* ************************************************************************* *)

(** Make an empty function from an existing global varinfo.
    @since Nitrogen-20111001 *)
val emptyFunctionFromVI: varinfo -> fundec

(** Make an empty function *)
val emptyFunction: string -> fundec

(** Update the formals of a [fundec] and make sure that the function type
    has the same information. Will copy the name as well into the type. *)
val setFormals: fundec -> varinfo list -> unit

(** Takes as input a function type (or a typename on it) and return its
    return type. *)
val getReturnType: typ -> typ

(** Change the return type of the function passed as 1st argument to be
    the type passed as 2nd argument. *)
val setReturnTypeVI: varinfo -> typ -> unit
val setReturnType: fundec -> typ -> unit

(** Set the types of arguments and results as given by the function type
 * passed as the second argument. Will not copy the names from the function
 * type to the formals *)
val setFunctionType: fundec -> typ -> unit

(** Set the type of the function and make formal arguments for them *)
val setFunctionTypeMakeFormals: fundec -> typ -> unit

(** Update the smaxid after you have populated with locals and formals
 * (unless you constructed those using {!Cil.makeLocalVar} or
 * {!Cil.makeTempVar}. *)
val setMaxId: fundec -> unit

val selfFormalsDecl: State.t
Allan Blanchard's avatar
Allan Blanchard committed
181
(** state of the table associating formals to each prototype. *)
182

183
val makeFormalsVarDecl: ?ghost:bool -> (string * typ * attributes) -> varinfo
Allan Blanchard's avatar
Allan Blanchard committed
184
185
186
187
(** creates a new varinfo for the parameter of a prototype.
    By default, this formal variable is not ghost.
    @modify 20.0-Calcium adds a parameter for ghost status
*)
188
189
190
191
192

(** Update the formals of a function declaration from its identifier and its
    type. For a function definition, use {!Cil.setFormals}.
    Do nothing if the type is not a function type or if the list of
    argument is empty.
Allan Blanchard's avatar
Allan Blanchard committed
193
*)
194
195
196
197
198
199
200
201
202
203
204
205
val setFormalsDecl: varinfo -> typ -> unit

(** remove a binding from the table.
    @since Oxygen-20120901 *)
val removeFormalsDecl: varinfo -> unit

(** replace formals of a function declaration with the given
    list of varinfo.
*)
val unsafeSetFormalsDecl: varinfo -> varinfo list -> unit

(** iterate the given function on declared prototypes.
206
    @since Oxygen-20120901
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
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
*)
val iterFormalsDecl: (varinfo -> varinfo list -> unit) -> unit

(** Get the formals of a function declaration registered with
    {!Cil.setFormalsDecl}.
    @raise Not_found if the function is not registered (this is in particular
    the case for prototypes with an empty list of arguments.
    See {!Cil.setFormalsDecl})
*)
val getFormalsDecl: varinfo -> varinfo list

(** A dummy file *)
val dummyFile: file

(** Iterate over all globals, including the global initializer *)
val iterGlobals: file -> (global -> unit) -> unit

(** Fold over all globals, including the global initializer *)
val foldGlobals: file -> ('a -> global -> 'a) -> 'a -> 'a

(** Map over all globals, including the global initializer and change things
    in place *)
val mapGlobals: file -> (global -> global) -> unit

(** Find a function or function prototype with the given name in the file.
  * If it does not exist, create a prototype with the given type, and return
  * the new varinfo.  This is useful when you need to call a libc function
  * whose prototype may or may not already exist in the file.
  *
  * Because the new prototype is added to the start of the file, you shouldn't
  * refer to any struct or union types in the function type.*)
val findOrCreateFunc: file -> string -> typ -> varinfo

(** creates an expression with a fresh id *)
val new_exp: loc:location -> exp_node -> exp

(** performs a deep copy of an expression (especially, avoid eid sharing).
    @since Nitrogen-20111001
*)
val copy_exp: exp -> exp

(** creates an expression with a dummy id.
    Use with caution, {i i.e.} not on expressions that may be put in the AST.
*)
val dummy_exp: exp_node -> exp

(** Return [true] on case and default labels, [false] otherwise. *)
val is_case_label: label -> bool


(** CIL keeps the types at the beginning of the file and the variables at the
 * end of the file. This function will take a global and add it to the
 * corresponding stack. Its operation is actually more complicated because if
 * the global declares a type that contains references to variables (e.g. in
 * sizeof in an array length) then it will also add declarations for the
 * variables to the types stack *)
val pushGlobal: global -> types: global list ref
Allan Blanchard's avatar
Allan Blanchard committed
264
  -> variables: global list ref -> unit
265
266
267
268
269
270
271
272
273
274
275
276
277

(** An empty statement. Used in pretty printing *)
val invalidStmt: stmt

(** A list of the built-in functions for the current compiler (GCC or
  * MSVC, depending on [!msvcMode]).  Maps the name to the
  * result and argument types, and whether it is vararg.
  * Initialized by {!Cil.initCIL}
  *
  * This map replaces [gccBuiltins] and [msvcBuiltins] in previous
  * versions of CIL.*)
module Builtin_functions :
  State_builder.Hashtbl with type key = string
Allan Blanchard's avatar
Allan Blanchard committed
278
                         and type data = typ * typ list * bool
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302

(** This is used as the location of the prototypes of builtin functions. *)
val builtinLoc: location

(** Returns a location that ranges over the two locations in arguments. *)
val range_loc: location -> location -> location

(* ************************************************************************* *)
(** {2 Values for manipulating initializers} *)
(* ************************************************************************* *)

(** Make a initializer for zero-ing a data type *)
val makeZeroInit: loc:location -> typ -> init

(** Fold over the list of initializers in a Compound (not also the nested
 * ones). [doinit] is called on every present initializer, even if it is of
 * compound type. The parameters of [doinit] are: the offset in the compound
 * (this is [Field(f,NoOffset)] or [Index(i,NoOffset)]), the initializer
 * value, expected type of the initializer value, accumulator. In the case of
 * arrays there might be missing zero-initializers at the end of the list.
 * These are scanned only if [implicit] is true. This is much like
 * [List.fold_left] except we also pass the type of the initializer.

 * This is a good way to use it to scan even nested initializers :
Allan Blanchard's avatar
Allan Blanchard committed
303
    {v
304
305
306
307
308
309
310
311
312
313
314
315
316
  let rec myInit (lv: lval) (i: init) (acc: 'a) : 'a =
    match i with
      | SingleInit e -> (* ... do something with [lv] and [e] and [acc] ... *)
      | CompoundInit (ct, initl) ->
         foldLeftCompound ~implicit:false
           ~doinit:(fun off' i' _typ acc' ->
                      myInit (addOffsetLval off' lv) i' acc')
           ~ct
           ~initl
           ~acc
v}
*)
val foldLeftCompound:
Allan Blanchard's avatar
Allan Blanchard committed
317
318
319
320
321
  implicit:bool ->
  doinit: (offset -> init -> typ -> 'a -> 'a) ->
  ct: typ ->
  initl: (offset * init) list ->
  acc: 'a -> 'a
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354

(* ************************************************************************* *)
(** {2 Values for manipulating types} *)
(* ************************************************************************* *)

(** void *)
val voidType: typ

(** is the given type "void"? *)
val isVoidType: typ -> bool

(** is the given type "void *"? *)
val isVoidPtrType: typ -> bool

(** int *)
val intType: typ

(** unsigned int *)
val uintType: typ

(** long *)
val longType: typ

(** long long *)
val longLongType: typ

(** unsigned long *)
val ulongType: typ

(** unsigned long long *)
val ulongLongType: typ

(** Any unsigned integer type of size 16 bits.
355
356
    It is equivalent to the ISO C uint16_t type but without using the
    corresponding header.
357
358
359
360
361
362
    Shall not be called if not such type exists in the current architecture.
    @since Nitrogen-20111001
*)
val uint16_t: unit -> typ

(** Any unsigned integer type of size 32 bits.
363
364
    It is equivalent to the ISO C uint32_t type but without using the
    corresponding header.
365
366
367
368
369
370
    Shall not be called if not such type exists in the current architecture.
    @since Nitrogen-20111001
*)
val uint32_t: unit -> typ

(** Any unsigned integer type of size 64 bits.
371
372
    It is equivalent to the ISO C uint64_t type but without using the
    corresponding header.
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
    Shall not be called if no such type exists in the current architecture.
    @since Nitrogen-20111001
*)
val uint64_t: unit -> typ

(** char *)
val charType: typ
val scharType: typ
val ucharType: typ

(** char * *)
val charPtrType: typ
val scharPtrType: typ
val ucharPtrType: typ

(** char const * *)
val charConstPtrType: typ

(** void * *)
val voidPtrType: typ

(** void const * *)
val voidConstPtrType: typ

(** int * *)
val intPtrType: typ

(** unsigned int * *)
val uintPtrType: typ

(** float *)
val floatType: typ

(** double *)
val doubleType: typ

(** long double *)
val longDoubleType: typ

(** @return true if and only if the given type is a signed integer type. *)
val isSignedInteger: typ -> bool

(** @return true if and only if the given type is an unsigned integer type.
    @since Oxygen-20120901 *)
val isUnsignedInteger: typ -> bool

(** This is a constant used as the name of an unnamed bitfield. These fields
    do not participate in initialization and their name is not printed. *)
val missingFieldName: string

(** Get the full name of a comp, including the 'struct' or 'union' prefix *)
val compFullName: compinfo -> string

(** Returns true if this is a complete type.
Allan Blanchard's avatar
Allan Blanchard committed
427
428
429
430
431
432
    This means that sizeof(t) makes sense.
    Incomplete types are not yet defined
    structures and empty arrays.
    @param allowZeroSizeArrays indicates whether arrays of
    size 0 (a gcc extension) are considered as complete. Default value
    depends on the current machdep.
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
*)
val isCompleteType: ?allowZeroSizeArrays:bool -> typ -> bool

(** [true] iff the given type is a [struct] whose last field is a flexible
    array member. When in gcc mode, a zero-sized array is identified with a
    FAM for this purpose.

    @since 18.0-Argon
*)
val has_flexible_array_member: typ -> bool

(** Unroll a type until it exposes a non
 * [TNamed]. Will collect all attributes appearing in [TNamed]!!! *)
val unrollType: typ -> typ

(** Unroll all the TNamed in a type (even under type constructors such as
 * [TPtr], [TFun] or [TArray]. Does not unroll the types of fields in [TComp]
 * types. Will collect all attributes *)
val unrollTypeDeep: typ -> typ

(** Separate out the storage-modifier name attributes *)
val separateStorageModifiers: attribute list -> attribute list * attribute list

(** returns the type of the result of an arithmetic operator applied to
    values of the corresponding input types.
    @since Nitrogen-20111001 (moved from Cabs2cil)
*)
val arithmeticConversion : Cil_types.typ -> Cil_types.typ -> Cil_types.typ

(** performs the usual integral promotions mentioned in C reference manual.
    @since Nitrogen-20111001 (moved from Cabs2cil)
*)
val integralPromotion : Cil_types.typ -> Cil_types.typ

(** True if the argument is a character type (i.e. plain, signed or unsigned)
    @since Chlorine-20180501 *)
val isAnyCharType: typ -> bool

(** True if the argument is a plain character type
    (but neither [signed char] nor [unsigned char]).
    @modify Chlorine-20180501 old behavior renamed as [isAnyCharType] *)
val isCharType: typ -> bool

(** True if the argument is a short type (i.e. signed or unsigned) *)
val isShortType: typ -> bool

(** True if the argument is a pointer to a character type
    (i.e. plain, signed or unsigned).
    @since Chlorine-20180501 *)
val isAnyCharPtrType: typ -> bool

(** True if the argument is a pointer to a plain character type
    (but neither [signed char] nor [unsigned char]).
    @modify Chlorine-20180501 old behavior renamed as [isAnyCharPtrType] *)
val isCharPtrType: typ -> bool

(** True if the argument is a pointer to a constant character type,
    e.g. a string literal.
    @since Chlorine-20180501 *)
val isCharConstPtrType: typ -> bool

(** True if the argument is an array of a character type
    (i.e. plain, signed or unsigned)
    @since Chlorine-20180501 *)
val isAnyCharArrayType: typ -> bool

(** True if the argument is an array of a character type
    (i.e. plain, signed or unsigned)
    @modify Chlorine-20180501 old behavior renamed as [isAnyCharArrayType] *)
val isCharArrayType: typ -> bool

(** True if the argument is an integral type (i.e. integer or enum) *)
val isIntegralType: typ -> bool

507
(** True if the argument is [_Bool]
508
    @since 19.0-Potassium
509
510
511
512
*)
val isBoolType: typ -> bool

(** True if the argument is [_Bool] or [boolean].
513
    @since 19.0-Potassium
Allan Blanchard's avatar
Allan Blanchard committed
514
*)
515
516
val isLogicPureBooleanType: logic_type -> bool

517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
(** True if the argument is an integral or pointer type. *)
val isIntegralOrPointerType: typ -> bool

(** True if the argument is an integral type (i.e. integer or enum), either
    C or mathematical one.
    @modify 18.0-Argon expands the logic type definition if necessary. *)
val isLogicIntegralType: logic_type -> bool

(** True if the argument is a boolean type, either integral C type or
    mathematical boolean one.
    @modify 18.0-Argon expands the logic type definition if necessary. *)
val isLogicBooleanType: logic_type -> bool

(** True if the argument is a floating point type. *)
val isFloatingType: typ -> bool

(** True if the argument is a floating point type.
    @modify 18.0-Argon expands the logic type definition if necessary. *)
val isLogicFloatType: logic_type -> bool

(** True if the argument is a C floating point type or logic 'real' type.
    @modify 18.0-Argon expands the logic type definition if necessary. *)
val isLogicRealOrFloatType: logic_type -> bool

(** True if the argument is the logic 'real' type.
    @modify 18.0-Argon expands the logic type definition if necessary. *)
val isLogicRealType: logic_type -> bool

(** True if the argument is an arithmetic type (i.e. integer, enum or
    floating point *)
val isArithmeticType: typ -> bool

549
550
(** True if the argument is a scalar type (i.e. integral, enum,
    floating point or pointer
551
    @since 22.0-Titanium
Virgile Prevosto's avatar
Virgile Prevosto committed
552
*)
553
554
555
val isScalarType: typ -> bool

(** alias of isScalarType.
556
    @deprecated 22.0-Titanium use isScalarType instead
Virgile Prevosto's avatar
Virgile Prevosto committed
557
*)
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
val isArithmeticOrPointerType: typ -> bool

(** True if the argument is a logic arithmetic type (i.e. integer, enum or
    floating point, either C or mathematical one.
    @modify 18.0-Argon expands the logic type definition if necessary. *)
val isLogicArithmeticType: logic_type -> bool

(** True if the argument is a function type *)
val isFunctionType: typ -> bool

(** True if the argument is the logic function type.
    Expands the logic type definition if necessary.
    @since 18.0-Argon *)
val isLogicFunctionType: logic_type -> bool

(** True if the argument is a pointer type. *)
val isPointerType: typ -> bool

(** True if the argument is a function pointer type.
    @since 18.0-Argon *)
val isFunPtrType: typ -> bool

(** True if the argument is the logic function pointer type.
    Expands the logic type definition if necessary.
    @since 18.0-Argon *)
val isLogicFunPtrType: logic_type -> bool

(** True if the argument is the type for reified C types.
    @modify 18.0-Argon expands the logic type definition if necessary. *)
val isTypeTagType: logic_type -> bool

(** True if the argument denotes the type of ... in a variadic function.
    @since Nitrogen-20111001 moved from cabs2cil *)
val isVariadicListType: typ -> bool

593
(** Obtain the argument list ([] if None).
Andre Maroneze's avatar
Andre Maroneze committed
594
    @since 20.0-Calcium Beware that it contains the ghost arguments. *)
595
596
597
val argsToList:
  (string * typ * attributes) list option -> (string * typ * attributes) list

Andre Maroneze's avatar
Andre Maroneze committed
598
(** @since 20.0-Calcium
Allan Blanchard's avatar
Allan Blanchard committed
599
    Obtain the argument lists (non-ghost, ghosts) ([], [] if None) *)
600
601
602
603
val argsToPairOfLists:
  (string * typ * attributes) list option ->
  (string * typ * attributes) list * (string * typ * attributes) list

604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
(** True if the argument is an array type *)
val isArrayType: typ -> bool

(** True if the argument is a struct of union type *)
val isStructOrUnionType: typ -> bool

(** Raised when {!Cil.lenOfArray} fails either because the length is [None]
  * or because it is a non-constant expression *)
exception LenOfArray

(** Call to compute the array length as present in the array type, to an
  * integer. Raises {!Cil.LenOfArray} if not able to compute the length, such
  * as when there is no length or the length is not a constant. *)
val lenOfArray: exp option -> int
val lenOfArray64: exp option -> Integer.t

(** Return a named fieldinfo in compinfo, or raise Not_found *)
val getCompField: compinfo -> string -> fieldinfo


(** A datatype to be used in conjunction with [existsType] *)
type existsAction =
    ExistsTrue                          (** We have found it *)
  | ExistsFalse                         (** Stop processing this branch *)
  | ExistsMaybe                         (** This node is not what we are
                                         * looking for but maybe its
                                         * successors are *)

(** Scans a type by applying the function on all elements.
    When the function returns ExistsTrue, the scan stops with
    true. When the function returns ExistsFalse then the current branch is not
    scanned anymore. Care is taken to
    apply the function only once on each composite type, thus avoiding
    circularity. When the function returns ExistsMaybe then the types that
    construct the current type are scanned (e.g. the base type for TPtr and
    TArray, the type of fields for a TComp, etc). *)
val existsType: (typ -> existsAction) -> typ -> bool


(** Given a function type split it into return type,
 * arguments, is_vararg and attributes. An error is raised if the type is not
 * a function type *)
val splitFunctionType:
Allan Blanchard's avatar
Allan Blanchard committed
647
  typ -> typ * (string * typ * attributes) list option * bool * attributes
648
649
650
651
652
653
654
655
656
657
658
(** Same as {!Cil.splitFunctionType} but takes a varinfo. Prints a nicer
 * error message if the varinfo is not for a function *)
val splitFunctionTypeVI:
  varinfo ->
  typ * (string * typ * attributes) list option * bool * attributes


(*********************************************************)
(**  LVALUES *)

(** Make a varinfo. Use this (rarely) to make a raw varinfo. Use other
Allan Blanchard's avatar
Allan Blanchard committed
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
    functions to make locals ({!Cil.makeLocalVar} or {!Cil.makeFormalVar} or
    {!Cil.makeTempVar}) and globals ({!Cil.makeGlobalVar}). Note that this
    function will assign a new identifier.
    The [temp] argument defaults to [false], and corresponds to the
    [vtemp] field in type {!Cil_types.varinfo}.
    The [source] argument defaults to [true], and corresponds to the field
    [vsource] .
    The [referenced] argument defaults to [false], and corresponds to the field
    [vreferenced] .
    The [ghost] argument defaults to [false], and corresponds to the field
    [vghost] .
    The [loc] argument defaults to [Location.unknown], and corresponds to the field
    [vdecl] .
    The first unnamed argument specifies whether the varinfo is for a global and
    the second is for formals.
    @modify 19.0-Potassium adds an optional ghost parameter
675
*)
676
val makeVarinfo:
677
  ?source:bool -> ?temp:bool -> ?referenced:bool -> ?ghost:bool -> ?loc:Location.t -> bool -> bool
678
  -> string -> typ -> varinfo
679
680
681
682
683
684

(** Make a formal variable for a function declaration. Insert it in both the
    sformals and the type of the function. You can optionally specify where to
    insert this one. If where = "^" then it is inserted first. If where = "$"
    then it is inserted last. Otherwise where must be the name of a formal
    after which to insert this. By default it is inserted at the end.
685
686
687
688
689
690
691
692
693
694

    The [ghost] parameter indicates if the variable should be inserted in the
    list of formals or ghost formals. By default, it takes the ghost status of
    the function where the formal is inserted. Note that:

    - specifying ghost to false if the function is ghost leads to an error
    - when [where] is specified, its status must be the same as the formal to
      insert (else, it cannot be found in the list of ghost or non ghost formals)

    @modify 19.0-Potassium adds the optional ghost parameter
695
*)
696
val makeFormalVar: fundec -> ?ghost:bool -> ?where:string -> ?loc:Location.t -> string -> typ -> varinfo
697
698
699
700
701
702
703
704
705
706

(** Make a local variable and add it to a function's slocals and to the given
    block (only if insert = true, which is the default).
    Make sure you know what you are doing if you set [insert=false].
    [temp] is passed to {!Cil.makeVarinfo}.
    The variable is attached to the toplevel block if [scope] is not specified.
    If the name passed as argument already exists within the function,
    a fresh name will be generated for the varinfo.

    @modify Chlorine-20180501 the name of the variable is guaranteed to be fresh.
Andre Maroneze's avatar
Andre Maroneze committed
707
    @modify 20.0-Calcium add ghost optional argument
708
709
*)
val makeLocalVar:
710
  fundec -> ?scope:block -> ?temp:bool -> ?referenced:bool -> ?insert:bool ->
711
  ?ghost:bool -> ?loc:Location.t -> string -> typ -> varinfo
712
713
714
715
716
717
718
719
720
721
722

(** if needed, rename the given varinfo so that its [vname] does not
    clash with the one of a local or formal variable of the given function.

    @since Chlorine-20180501
*)
val refresh_local_name: fundec -> varinfo -> unit

(** Make a temporary variable and add it to a function's slocals. The name of
    the temporary variable will be generated based on the given name hint so
    that to avoid conflicts with other locals.
723
724
    Optionally, you can give the variable a description of its contents and
    its location.
725
726
727
728
    Temporary variables are always considered as generated variables.
    If [insert] is true (the default), the variable will be inserted
    among other locals of the function. The value for [insert] should
    only be changed if you are completely sure this is not useful.
729

Andre Maroneze's avatar
Andre Maroneze committed
730
    @modify 20.0-Calcium add ghost optional argument
Allan Blanchard's avatar
Allan Blanchard committed
731
*)
732
733
val makeTempVar: fundec -> ?insert:bool -> ?ghost:bool -> ?name:string ->
  ?descr:string -> ?descrpure:bool -> ?loc:Location.t -> typ -> varinfo
734
735

(** Make a global variable. Your responsibility to make sure that the name
736
737
    is unique. [source] defaults to [true]. [temp] defaults to [false].

Andre Maroneze's avatar
Andre Maroneze committed
738
    @modify 20.0-Calcium add ghost optional arg
739
740
741
*)
val makeGlobalVar: ?source:bool -> ?temp:bool -> ?referenced:bool ->
  ?ghost:bool -> ?loc:Cil_datatype.Location.t -> string -> typ -> varinfo
742
743
744
745

(** Make a shallow copy of a [varinfo] and assign a new identifier.
    If the original varinfo has an associated logic var, it is copied too and
    associated to the copied varinfo
Allan Blanchard's avatar
Allan Blanchard committed
746
*)
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
val copyVarinfo: varinfo -> string -> varinfo

(** Changes the type of a varinfo and of its associated logic var if any.
    @since Neon-20140301 *)
val update_var_type: varinfo -> typ -> unit

(** Is an lvalue a bitfield? *)
val isBitfield: lval -> bool

(** Returns the last offset in the chain. *)
val lastOffset: offset -> offset

(** Add an offset at the end of an lvalue. Make sure the type of the lvalue
 * and the offset are compatible. *)
val addOffsetLval: offset -> lval -> lval

(** [addOffset o1 o2] adds [o1] to the end of [o2]. *)
val addOffset:     offset -> offset -> offset

(** Remove ONE offset from the end of an lvalue. Returns the lvalue with the
 * trimmed offset and the final offset. If the final offset is [NoOffset]
 * then the original [lval] did not have an offset. *)
val removeOffsetLval: lval -> lval * offset

(** Remove ONE offset from the end of an offset sequence. Returns the
 * trimmed offset and the final offset. If the final offset is [NoOffset]
 * then the original [lval] did not have an offset. *)
val removeOffset:   offset -> offset * offset

(** Compute the type of an lvalue *)
val typeOfLval: lval -> typ

(** Compute the type of an lhost (with no offset) *)
val typeOfLhost: lhost -> typ

(** Equivalent to [typeOfLval] for terms. *)
val typeOfTermLval: term_lval -> logic_type

(** Compute the type of an offset from a base type *)
val typeOffset: typ -> offset -> typ

(** Equivalent to [typeOffset] for terms. *)
val typeTermOffset: logic_type -> term_offset -> logic_type

(** Compute the type of an initializer *)
val typeOfInit: init -> typ

(** indicates whether the given lval is a modifiable lvalue in the sense
    of the C standard 6.3.2.1§1. *)
val is_modifiable_lval: lval -> bool

(* ************************************************************************* *)
(** {2 Values for manipulating expressions} *)
(* ************************************************************************* *)

(* Construct integer constants *)

(** 0 *)
val zero: loc:Location.t -> exp

(** 1 *)
val one: loc:Location.t -> exp

(** -1 *)
val mone: loc:Location.t -> exp

(** Construct an integer of a given kind without literal representation.
    Truncate the integer if [kind] is given, and the integer does not fit
    inside the type. The integer can have an optional literal representation
    [repr].
    @raise Not_representable if no ikind is provided and the integer is not
    representable. *)
val kinteger64: loc:location -> ?repr:string -> ?kind:ikind -> Integer.t -> exp

(** Construct an integer of a given kind. Converts the integer to int64 and
  * then uses kinteger64. This might truncate the value if you use a kind
  * that cannot represent the given integer. This can only happen for one of
  * the Char or Short kinds *)
val kinteger: loc:location -> ikind -> int -> exp

(** Construct an integer of kind IInt. You can use this always since the
    OCaml integers are 31 bits and are guaranteed to fit in an IInt *)
val integer: loc:location -> int -> exp

(** Constructs a floating point constant.
832
    @since Oxygen-20120901
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
*)
val kfloat: loc:location -> fkind -> float -> exp

(** True if the given expression is a (possibly cast'ed)
    character or an integer constant *)
val isInteger: exp -> Integer.t option

(** True if the expression is a compile-time constant *)
val isConstant: exp -> bool

(** True if the expression is a compile-time integer constant *)
val isIntegerConstant: exp -> bool

(** True if the given offset contains only field names or constant indices. *)
val isConstantOffset: offset -> bool

(** True if the given expression is a (possibly cast'ed) integer or character
    constant with value zero *)
val isZero: exp -> bool

(** True if the term is the constant 0 *)
val isLogicZero: term -> bool

(** True if the given term is [\null] or a constant null pointer*)
val isLogicNull: term -> bool

859
860
861
(** [no_op_coerce typ term] is [true] iff converting [term] to [typ] does
    not modify its value.

862
    @since 19.0-Potassium
863
864
865
*)
val no_op_coerce: logic_type -> term -> bool

866
867
868
869
870
871
872
873
(** gives the value of a wide char literal. *)
val reduce_multichar: Cil_types.typ -> int64 list -> int64

(** gives the value of a char literal. *)
val interpret_character_constant:
  int64 list -> Cil_types.constant * Cil_types.typ

(** Given the character c in a (CChr c), sign-extend it to 32 bits.
Allan Blanchard's avatar
Allan Blanchard committed
874
875
876
    (This is the official way of interpreting character constants, according to
    ISO C 6.4.4.4.10, which says that character constants are chars cast to ints)
    Returns CInt64(sign-extended c, IInt, None) *)
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
val charConstToInt: char -> Integer.t
val charConstToIntConstant: char -> constant

(** Do constant folding on an expression. If the first argument is [true] then
    will also compute compiler-dependent expressions such as sizeof.
    See also {!Cil.constFoldVisitor}, which will run constFold on all
    expressions in a given AST node. *)
val constFold: bool -> exp -> exp

(** Do constant folding on the given expression, just as [constFold] would. The
    resulting integer value, if the const-folding was complete, is returned.
    The [machdep] optional parameter, which is set to [true] by default,
    forces the simplification of architecture-dependent expressions. *)
val constFoldToInt: ?machdep:bool -> exp -> Integer.t option

(** Do constant folding on an term at toplevel only.
    This uses compiler-dependent informations and will
    remove all sizeof and alignof. *)
val constFoldTermNodeAtTop:  term_node -> term_node

(** Do constant folding on an term.
    If the first argument is true then
    will also compute compiler-dependent expressions such as [sizeof]
    and [alignof]. *)
val constFoldTerm: bool -> term -> term

903
904
905
906
(** Do constant folding on a {!Cil_types.offset}. If the second argument is true
    then will also compute compiler-dependent expressions such as [sizeof]. *)
val constFoldOffset: bool -> offset -> offset

907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
(** Do constant folding on a binary operation. The bulk of the work done by
    [constFold] is done here. If the second argument is true then
    will also compute compiler-dependent expressions such as [sizeof]. *)
val constFoldBinOp: loc:location -> bool -> binop -> exp -> exp -> typ -> exp

(** [true] if the two constant are equal.
    @since Nitrogen-20111001
*)
val compareConstant: constant -> constant -> bool

(** Increment an expression. Can be arithmetic or pointer type *)
val increm: exp -> int -> exp

(** Increment an expression. Can be arithmetic or pointer type *)
val increm64: exp -> Integer.t -> exp

(** Makes an lvalue out of a given variable *)
val var: varinfo -> lval

926
(** Creates an expr representing the variable.
927
    @since Nitrogen-20111001
Allan Blanchard's avatar
Allan Blanchard committed
928
*)
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
val evar: ?loc:location -> varinfo -> exp

(** Make an AddrOf. Given an lvalue of type T will give back an expression of
    type ptr(T). It optimizes somewhat expressions like "& v" and "& v[0]"  *)
val mkAddrOf: loc:location -> lval -> exp

(** Creates an expression corresponding to "&v".
    @since Oxygen-20120901 *)
val mkAddrOfVi: varinfo -> exp

(** Like mkAddrOf except if the type of lval is an array then it uses
    StartOf. This is the right operation for getting a pointer to the start
    of the storage denoted by lval. *)
val mkAddrOrStartOf: loc:location -> lval -> exp

(** Make a Mem, while optimizing AddrOf. The type of the addr must be
    TPtr(t) and the type of the resulting lval is t. Note that in CIL the
    implicit conversion between an array and the pointer to the first
    element does not apply. You must do the conversion yourself using
    StartOf *)
val mkMem: addr:exp -> off:offset -> lval

(** makes a binary operation and performs const folding.  Inserts
    casts between arithmetic types as needed, or between pointer
    types, but do not attempt to cast pointer to int or
    vice-versa. Use appropriate binop (PlusPI & friends) for that.
    @modify Chlorine-20180501 no systematic cast to uintptr_t for ptr comparisons.
*)
val mkBinOp: loc:location -> binop -> exp -> exp -> exp

(** same as {!mkBinOp}, but performs a systematic cast (unless one of the
    arguments is [0]) of pointers into [uintptr_t] during comparisons,
    making such operation defined even if the pointers do not share
    the same base. This was the behavior of {!mkBinOp} prior to the
    introduction of this function.
    @since Chlorine-20180501
Allan Blanchard's avatar
Allan Blanchard committed
965
*)
966
967
968
969
970
971
972
973
val mkBinOp_safe_ptr_cmp: loc:location -> binop -> exp -> exp -> exp

(** Equivalent to [mkMem] for terms. *)
val mkTermMem: addr:term -> off:term_offset -> term_lval

(** Make an expression that is a string constant (of pointer type) *)
val mkString: loc:location -> string -> exp

974
(** [true] if both types are not equivalent.
975
976
977
978
979
980
981
982
983
984
985
986
    if [force] is [true], returns [true] whenever both types are not equal
    (modulo typedefs). If [force] is [false] (the default), other equivalences
    are considered, in particular between an enum and its representative
    integer type.
    @modify Fluorine-20130401 added [force] argument
*)
val need_cast: ?force:bool -> typ -> typ -> bool

(** Construct a cast when having the old type of the expression. If the new
    type is the same as the old type, then no cast is added, unless [force]
    is [true] (default is [false])
    @modify Fluorine-20130401 add [force] argument
Allan Blanchard's avatar
Allan Blanchard committed
987
*)
988
989
990
991
992
993
994
995
996
val mkCastT: ?force:bool -> e:exp -> oldt:typ -> newt:typ -> exp

(** Like {!Cil.mkCastT} but uses typeOf to get [oldt] *)
val mkCast: ?force:bool -> e:exp -> newt:typ -> exp

(** Equivalent to [stripCasts] for terms. *)
val stripTermCasts: term -> term

(** Removes casts from this expression, but ignores casts within
Allan Blanchard's avatar
Allan Blanchard committed
997
998
    other expression constructs.  So we delete the (A) and (B) casts from
    "(A)(B)(x + (C)y)", but leave the (C) cast. *)
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
val stripCasts: exp -> exp

(** Removes info wrappers and return underlying expression *)
val stripInfo: exp -> exp

(** Removes casts and info wrappers and return underlying expression *)
val stripCastsAndInfo: exp -> exp

(** Removes casts and info wrappers,except last info wrapper, and return
    underlying expression *)
val stripCastsButLastInfo: exp -> exp

(** Extracts term information in an expression information *)
val exp_info_of_term: term -> exp_info

(** Constructs a term from a term node and an expression information *)
val term_of_exp_info: location -> term_node -> exp_info -> term

(** Map some function on underlying expression if Info or else on expression *)
val map_under_info: (exp -> exp) -> exp -> exp

(** Apply some function on underlying expression if Info or else on expression *)
val app_under_info: (exp -> unit) -> exp -> unit

val typeOf: exp -> typ
(** Compute the type of an expression. *)

val typeOf_pointed : typ -> typ
(** Returns the type pointed by the given type. Asserts it is a pointer type. *)

val typeOf_array_elem : typ -> typ
(** Returns the type of the array elements of the given type.
    Asserts it is an array type. *)

val is_fully_arithmetic: typ -> bool
Allan Blanchard's avatar
Allan Blanchard committed
1034
(** Returns [true] whenever the type contains only arithmetic types *)
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056

(** Convert a string representing a C integer literal to an expression.
    Handles the prefixes 0x and 0 and the suffixes L, U, UL, LL, ULL.
*)
val parseInt: string -> Integer.t
val parseIntExp: loc:location -> string -> exp
val parseIntLogic: loc:location -> string -> term

(** Convert a string representing a C integer literal to an expression.
    Handles the prefixes 0x and 0 and the suffixes L, U, UL, LL, ULL *)

val appears_in_expr: varinfo -> exp -> bool
(** @return true if the given variable appears in the expression. *)

(**********************************************)
(** {3 Values for manipulating statements} *)
(**********************************************)

(** Construct a statement, given its kind. Initialize the [sid] field to -1
    if [valid_sid] is false (the default),
    or to a valid sid if [valid_sid] is true,
    and [labels], [succs] and [preds] to the empty list *)
1057
1058
val mkStmt: ?ghost:bool -> ?valid_sid:bool -> ?sattr:attributes -> stmtkind ->
  stmt
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079

(* make the [new_stmtkind] changing the CFG relatively to [ref_stmt] *)
val mkStmtCfg: before:bool -> new_stmtkind:stmtkind -> ref_stmt:stmt -> stmt

(** Construct a block with no attributes, given a list of statements *)
val mkBlock: stmt list -> block

(** Construct a non-scoping block, i.e. a block that is not used to determine
    the end of scope of local variables. Hence, the blocals of such a block
    must always be empty.

    @since Phosphorus-20170501-beta1
*)
val mkBlockNonScoping: stmt list -> block

(** Construct a block with no attributes, given a list of statements and
    wrap it into the Cfg. *)
val mkStmtCfgBlock: stmt list -> stmt

(** Construct a statement consisting of just one instruction
    See {!Cil.mkStmt} for the signification of the optional args.
Allan Blanchard's avatar
Allan Blanchard committed
1080
*)
1081
1082
val mkStmtOneInstr: ?ghost:bool -> ?valid_sid:bool -> ?sattr:attributes ->
  instr -> stmt
1083
1084
1085
1086
1087
1088
1089
1090

(** Try to compress statements so as to get maximal basic blocks.
 * use this instead of List.@ because you get fewer basic blocks *)
(*val compactStmts: stmt list -> stmt list*)

(** Returns an empty statement (of kind [Instr]). See [mkStmt] for [ghost] and
    [valid_sid] arguments.
    @modify Neon-20130301 adds the [valid_sid] optional argument. *)
1091
1092
val mkEmptyStmt: ?ghost:bool -> ?valid_sid:bool -> ?sattr:attributes ->
  ?loc:location -> unit -> stmt
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123

(** A instr to serve as a placeholder *)
val dummyInstr: instr

(** A statement consisting of just [dummyInstr].
    @plugin development guide *)
val dummyStmt: stmt

(** Create an instruction equivalent to a pure expression. The new instruction
    corresponds to the initialization of a new fresh variable, i.e.
    [int tmp = exp]. The scope of this fresh variable
    is determined by the block given in argument, that is the instruction
    must be placed directly (modulo non-scoping blocks) inside this block.
*)
val mkPureExprInstr:
  fundec:fundec -> scope:block -> ?loc:location -> exp -> instr

(** Create an instruction as above, enclosed in a block
    of a single ([Instr]) statement, which will be the scope of the fresh
    variable holding the value of the expression.

    See {!Cil.mkStmt} for information about [ghost] and [valid_sid], and
    {!Cil.mkPureExprInstr} for information about [loc].

    @modify Chlorine-20180501 lift optional arg valid_sid from [mkStmt] instead
    of relying on ill-fated default.
*)
val mkPureExpr:
  ?ghost:bool -> ?valid_sid:bool -> fundec:fundec ->
  ?loc:location -> exp -> stmt

1124
1125
1126
1127
(** Make a loop. Can contain Break or Continue.
    The kind of loop (While, For, DoWhile) is given by [sattr];
    it is a While loop if unspecified. *)
val mkLoop: ?sattr:attributes -> guard:exp -> body:stmt list -> stmt list
1128
1129
1130
1131
1132
1133

(** Make a for loop for(i=start; i<past; i += incr) \{ ... \}. The body
    can contain Break but not Continue. Can be used with i a pointer
    or an integer. Start and done must have the same type but incr
    must be an integer *)
val mkForIncr:  iter:varinfo -> first:exp -> stopat:exp -> incr:exp
Allan Blanchard's avatar
Allan Blanchard committed
1134
  -> body:stmt list -> stmt list
1135
1136
1137
1138

(** Make a for loop for(start; guard; next) \{ ... \}. The body can
    contain Break but not Continue !!! *)
val mkFor: start:stmt list -> guard:exp -> next: stmt list ->
Allan Blanchard's avatar
Allan Blanchard committed
1139
  body: stmt list -> stmt list
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170

(** creates a block with empty attributes from an unspecified sequence. *)
val block_from_unspecified_sequence:
  (stmt * lval list * lval list * lval list * stmt ref list) list -> block

(** [treat_constructor_as_func action v f args kind loc] calls [action] with
    the parameters corresponding to the call to [f], of kind [kind],
    initializing [v] with arguments [args].
    @since Phosphorus-20170501-beta1
*)
val treat_constructor_as_func:
  (lval option -> exp -> exp list -> location -> 'a) ->
  varinfo -> varinfo -> exp list -> constructor_kind -> location -> 'a

(** [find_def_stmt b v] returns the [Local_init] instruction within [b] that
    initializes [v]. [v] must have its [vdefined] field set to true, and be
    among [b.blocals].
    @raise Fatal error if [v] is not a local variable of [b] with an
    initializer.
    @since Phosphorus-20170501-beta1
*)
val find_def_stmt: block -> varinfo -> stmt

(** returns [true] iff the given non-scoping block contains local init
    statements (thus of locals belonging to an outer block), either directly or
    within a non-scoping block or undefined sequence.labels

    @since Phosphorus-20170501-beta1
*)
val has_extern_local_init: block -> bool

1171
1172
(** returns [true] iff the given block is a ghost else block.

Andre Maroneze's avatar
Andre Maroneze committed
1173
    @since 21.0-Scandium
1174
1175
1176
*)
val is_ghost_else: block -> bool

1177
1178
1179
1180
1181
1182
1183
(* ************************************************************************* *)
(** {2 Values for manipulating attributes} *)
(* ************************************************************************* *)

(** Various classes of attributes *)
type attributeClass =
    AttrName of bool
Allan Blanchard's avatar
Allan Blanchard committed
1184
1185
1186
  (** Attribute of a name. If argument is true and we are on MSVC then
      the attribute is printed using __declspec as part of the storage
      specifier  *)
1187
  | AttrFunType of bool
Allan Blanchard's avatar
Allan Blanchard committed
1188
1189
  (** Attribute of a function type. If argument is true and we are on
      MSVC then the attribute is printed just before the function name *)
1190
1191
1192
  | AttrType  (** Attribute of a type *)

val registerAttribute: string -> attributeClass -> unit
Allan Blanchard's avatar
Allan Blanchard committed
1193
(** Add a new attribute with a specified class *)
1194
1195

val removeAttribute: string -> unit
Allan Blanchard's avatar
Allan Blanchard committed
1196
(** Remove an attribute previously registered. *)
1197
1198

val attributeClass: string -> attributeClass
Allan Blanchard's avatar
Allan Blanchard committed
1199
(** Return the class of an attributes. *)
1200
1201
1202
1203

(** Partition the attributes into classes:name attributes, function type,
    and type attributes *)
val partitionAttributes:  default:attributeClass ->
Allan Blanchard's avatar
Allan Blanchard committed
1204
1205
1206
  attributes -> attribute list * (* AttrName *)
                attribute list * (* AttrFunType *)
                attribute list   (* AttrType *)
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223

(** Add an attribute. Maintains the attributes in sorted order of the second
    argument *)
val addAttribute: attribute -> attributes -> attributes

(** Add a list of attributes. Maintains the attributes in sorted order. The
    second argument must be sorted, but not necessarily the first *)
val addAttributes: attribute list -> attributes -> attributes

(** Remove all attributes with the given name. Maintains the attributes in
    sorted order.  *)
val dropAttribute: string -> attributes -> attributes

(** Remove all attributes with names appearing in the string list.
 *  Maintains the attributes in sorted order *)
val dropAttributes: string list -> attributes -> attributes

1224
(** A block marked with this attribute is known to be a ghost else.
1225

1226
    @since 21.0-Scandium
1227
*)
1228
val frama_c_ghost_else: string
1229

1230
(** A varinfo marked with this attribute is known to be a ghost formal.
1231

1232
    @since 20.0-Calcium
1233
*)
1234
val frama_c_ghost_formal: string
1235
1236
1237
1238
1239
1240

(** a formal marked with this attribute is known to be a pointer to an
    object being initialized by the current function, which can thus assign
    any sub-object regardless of const status.

    @since 18.0-Argon
Allan Blanchard's avatar
Allan Blanchard committed
1241
*)
1242
1243
val frama_c_init_obj: string

1244
1245
(** a field struct marked with this attribute is known to be mutable, i.e.
    it can be modified even on a const object.
1246

1247
    @since 18.0-Argon
1248
*)
1249
val frama_c_mutable: string
1250

1251
1252
1253
1254
1255
(** A block marked with this attribute is known to be inlined, i.e.
    it replaces a call to an inline function.
*)
val frama_c_inlined: string

1256
1257
1258
1259
1260
(** [true] if the given lval is allowed to be assigned to thanks to
    a [frama_c_init_obj] or a [frama_c_mutable] attribute.
*)
val is_mutable_or_initialized: lval -> bool

1261
1262
(** [true] if the given varinfo is a ghost formal variable.

Andre Maroneze's avatar
Andre Maroneze committed
1263
    @since 20.0-Calcium
1264
1265
1266
1267
1268
*)
val isGhostFormalVarinfo: varinfo -> bool

(** [true] if the given formal declaration corresponds to a ghost formal variable.

Andre Maroneze's avatar
Andre Maroneze committed
1269
    @since 20.0-Calcium
1270
1271
1272
*)
val isGhostFormalVarDecl: (string * typ * attributes) -> bool

1273
1274
1275
1276
1277
1278
1279
1280
1281
(** Remove attributes whose name appears in the first argument that are
    present anywhere in the fully expanded version of the type.
    @since Oxygen-20120901
    @deprecated Chlorine-20180501 use {!Cil.typeRemoveAttributesDeep} instead,
    which does not traverse pointers and function types, or
    {!Cil.typeDeepDropAllAttributes}, which will give a pristine version of the
    type, without any attributes.
*)
val typeDeepDropAttributes: string list -> typ -> typ
Allan Blanchard's avatar
Allan Blanchard committed
1282
[@@ ocaml.deprecated "Use Cil.typeRemoveAttributesDeep"]
1283

1284
(** Remove any attribute appearing somewhere in the fully expanded
1285
    version of the type.
1286
    @since Oxygen-20120901
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
*)
val typeDeepDropAllAttributes: typ -> typ

(** Retains attributes with the given name *)
val filterAttributes: string -> attributes -> attributes

(** True if the named attribute appears in the attribute list. The list of
    attributes must be sorted.  *)
val hasAttribute: string -> attributes -> bool

(** returns the complete name for an attribute annotation. *)
val mkAttrAnnot: string -> string

(** Returns the name of an attribute. *)
val attributeName: attribute -> string

(** Returns the list of parameters associated to an attribute. The list is empty if there
    is no such attribute or it has no parameters at all. *)
val findAttribute: string -> attribute list -> attrparam list

(** Returns all the attributes contained in a type. This requires a traversal
    of the type structure, in case of composite, enumeration and named types *)
val typeAttrs: typ -> attribute list

(** Returns the attributes of a type. *)
val typeAttr: typ -> attribute list

(** Sets the attributes of the type to the given list. Previous attributes
    are discarded. *)
val setTypeAttrs: typ -> attributes -> typ

(** Add some attributes to a type *)
val typeAddAttributes: attribute list -> typ -> typ

(** Remove all attributes with the given names from a type. Note that this
    does not remove attributes from typedef and tag definitions, just from
    their uses (unfolding the type definition when needed).
    It only removes attributes of topmost type, i.e. does not
    recurse under pointers, arrays, ...
*)
val typeRemoveAttributes: string list -> typ -> typ

1329
(** same as above, but remove any existing attribute from the type.
1330

Allan Blanchard's avatar
Allan Blanchard committed
1331
    @since Magnesium-20151001
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
*)
val typeRemoveAllAttributes: typ -> typ

(** Same as [typeRemoveAttributes], but recursively removes the given
    attributes from inner types as well. Mainly useful to check whether
    two types are equal modulo some attributes. See also
    [typeDeepDropAllAttributes], which will strip every single attribute
    from a type.
*)
val typeRemoveAttributesDeep: string list -> typ -> typ

val typeHasAttribute: string -> typ -> bool
(** Does the type have the given attribute. Does
    not recurse through pointer types, nor inside function prototypes.
    @since Sodium-20150201 *)

val typeHasQualifier: string -> typ -> bool
(** Does the type have the given qualifier. Handles the case of arrays, for
    which the qualifiers are actually carried by the type of the elements.
    It is always correct to call this function instead of {!typeHasAttribute}.
    For l-values, both functions return the same results, as l-values cannot
    have array type.
    @since Sodium-20150201 *)

val typeHasAttributeDeep: string -> typ -> bool
(** Does the type or one of its subtypes have the given attribute. Does
    not recurse through pointer types, nor inside function prototypes.
    @since Oxygen-20120901
    @deprecated Chlorine-20180501 see {!Cil.typeHasAttributeMemoryBlock}
Allan Blanchard's avatar
Allan Blanchard committed
1361
*)
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
[@@ deprecated "Use Cil.typeHasAttributeMemoryBlock instead"]

val typeHasAttributeMemoryBlock: string -> typ -> bool
(** [typeHasAttributeMemoryBlock attr t] is
    [true] iff at least one component of an object of type [t] has attribute
    [attr]. In other words, it searches for [attr] under aggregates, but not
    under pointers.

    @since Chlorine-20180501 replaces typeHasAttributeDeep (name too ambiguous)
*)

(** Remove all attributes relative to const, volatile and restrict attributes
    @since Nitrogen-20111001
Allan Blanchard's avatar
Allan Blanchard committed
1375
*)
1376
1377
1378
val type_remove_qualifier_attributes: typ -> typ

(**
Allan Blanchard's avatar
Allan Blanchard committed
1379
1380
   remove also qualifiers under Ptr and Arrays
   @since Sodium-20150201
1381
1382
1383
1384
1385
1386
*)
val type_remove_qualifier_attributes_deep: typ -> typ

(** Remove all attributes relative to const, volatile and restrict attributes
    when building a C cast
    @since Oxygen-20120901
Allan Blanchard's avatar
Allan Blanchard committed
1387
*)
1388
1389
1390
1391
1392
val type_remove_attributes_for_c_cast: typ -> typ

(** Remove all attributes relative to const, volatile and restrict attributes
    when building a logic cast
    @since Oxygen-20120901
Allan Blanchard's avatar
Allan Blanchard committed
1393
*)
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
val type_remove_attributes_for_logic_type: typ -> typ

(** retains attributes corresponding to type qualifiers (6.7.3) *)
val filter_qualifier_attributes: attributes -> attributes

(** given some attributes on an array type, split them into those that belong
    to the type of the elements of the array (currently, qualifiers such as
    const and volatile), and those that must remain on the array, in that
    order
    @since Oxygen-20120901 *)
val splitArrayAttributes: attributes -> attributes * attributes

val bitfield_attribute_name: string
(** Name of the attribute that is automatically inserted (with an [AINT size]
    argument when querying the type of a field that is a bitfield *)

(** Convert an expression into an attrparam, if possible. Otherwise raise
    NotAnAttrParam with the offending subexpression *)
val expToAttrParam: exp -> attrparam

1414
1415

(** Return the attributes of the global annotation, if any.
Andre Maroneze's avatar
Andre Maroneze committed
1416
    @since 20.0-Calcium
1417
*)
1418
val global_annotation_attributes: global_annotation -> attributes
1419
1420

(** Return the attributes of the global, if any.
Andre Maroneze's avatar
Andre Maroneze committed
1421
    @since 20.0-Calcium
1422
*)
1423
val global_attributes: global -> attributes
1424

1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
exception NotAnAttrParam of exp

(* ************************************************************************* *)
(** {2 Const Attribute} *)
(* ************************************************************************* *)

val isConstType : typ -> bool
(** Check for ["const"] qualifier from the type of an l-value (do not follow pointer)
    @return true iff a part of the related l-value has ["const"] qualifier
    @since Chlorine-20180501 *)

(* ************************************************************************* *)
(** {2 Volatile Attribute} *)
(* ************************************************************************* *)

val isVolatileType : typ -> bool
(** Check for ["volatile"] qualifier from the type of an l-value (do not follow pointer)
    @return true iff a part of the related l-value has ["volatile"] qualifier
    @since Sulfur-20171101 *)

val isVolatileLogicType : logic_type -> bool
(** Check for ["volatile"] qualifier from a logic type
    @since Sulfur-20171101 *)

val isVolatileLval : lval -> bool
(** Check if the l-value has a volatile part
    @since Sulfur-20171101 *)

val isVolatileTermLval : term_lval -> bool
(** Check if the l-value has a volatile part
    @since Sulfur-20171101 *)

1457
1458
1459
1460
1461
1462
1463
(* ************************************************************************* *)
(** {2 Ghost Attribute} *)
(* ************************************************************************* *)

val isGhostType : typ -> bool
(** Check for ["ghost"] qualifier from the type of an l-value (do not follow pointer)
    @return true iff a part of the related l-value has ["ghost"] qualifier
Andre Maroneze's avatar
Andre Maroneze committed
1464
    @since 21.0-Scandium *)
1465

1466
1467
1468
1469
val isWFGhostType : typ -> bool
(** Check if the received type is well-formed according to \ghost semantics, that is
    once the type is not ghost anymore, \ghost cannot appear again.
    @return true iff the type is well formed
Andre Maroneze's avatar
Andre Maroneze committed
1470
    @since 21.0-Scandium *)
1471

1472
1473
1474
1475
1476
1477
1478
1479
(* ************************************************************************* *)
(** {2 The visitor} *)
(* ************************************************************************* *)

(** Different visiting actions. 'a will be instantiated with [exp], [instr],
    etc.
    @plugin development guide *)
type 'a visitAction =
1480
  | SkipChildren (** Do not visit the children. Return the node as it is.
Allan Blanchard's avatar
Allan Blanchard committed
1481
                     @plugin development guide *)
1482
  | DoChildren (** Continue with the children of this node. Rebuild the node on
Allan Blanchard's avatar
Allan Blanchard committed
1483
1484
                   return if any of the children changes (use == test).
                   @plugin development guide *)
1485
1486
1487
1488
1489
  | DoChildrenPost of ('a -> 'a)
  (** visit the children, and apply the given function to the result.
      @plugin development guide *)
  | JustCopy (** visit the children, but only to make the necessary copies
                 (only useful for copy visitor).
Allan Blanchard's avatar
Allan Blanchard committed
1490
                 @plugin development guide *)
1491
1492
  | JustCopyPost of ('a -> 'a)
  (** same as JustCopy + applies the given function to the result.
1493
1494
      @plugin development guide*)
  | ChangeTo of 'a  (** Replace the expression with the given one.
Allan Blanchard's avatar
Allan Blanchard committed
1495
                        @plugin development guide *)
1496
1497
1498
1499
1500
  | ChangeToPost of 'a * ('a -> 'a)
  (** applies the expression to the function and gives back the result.
      Useful to insert some actions in an inheritance chain.
      @plugin development guide *)
  | ChangeDoChildrenPost of 'a * ('a -> 'a)
Allan Blanchard's avatar
Allan Blanchard committed
1501
1502
1503
1504
  (** First consider that the entire exp is replaced by the first parameter. Then
      continue with the children. On return rebuild the node if any of the
      children has changed and then apply the function on the node.
      @plugin development guide *)
1505
1506
1507
1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
1518
1519
1520
1521

val mk_behavior :
  ?name:string ->
  ?assumes:identified_predicate list ->
  ?requires:identified_predicate list ->
  ?post_cond:(termination_kind * identified_predicate) list ->
  ?assigns:Cil_types.assigns ->
  ?allocation:Cil_types.allocation ->
  ?extended:acsl_extension list ->
  unit ->
  Cil_types.behavior
(** @since Carbon-20101201
    returns a dummy behavior with the default name [Cil.default_behavior_name].
    invariant: [b_assumes] must always be
    empty for behavior named [Cil.default_behavior_name] *)

val default_behavior_name: string
Allan Blanchard's avatar
Allan Blanchard committed
1522
(** @since Carbon-20101201  *)
1523
1524
1525

val is_default_behavior: behavior -> bool
val find_default_behavior: funspec -> funbehavior option
Allan Blanchard's avatar
Allan Blanchard committed
1526
(** @since Carbon-20101201  *)
1527
1528

val find_default_requires: behavior list -> identified_predicate list
Allan Blanchard's avatar
Allan Blanchard committed
1529
(** @since Carbon-20101201  *)
1530
1531
1532
1533
1534
1535
1536
1537

(* ************************************************************************* *)
(** {2 Visitor mechanism} *)
(* ************************************************************************* *)

(** {3 Visitor class} *)

(** A visitor interface for traversing CIL trees. Create instantiations of
Allan Blanchard's avatar
Allan Blanchard committed
1538
1539
1540
1541
1542
1543
1544
1545
1546
    this type by specializing the class {!nopCilVisitor}. Each of the
    specialized visiting functions can also call the [queueInstr] to specify
    that some instructions should be inserted before the current statement.
    Use syntax like [self#queueInstr] to call a method
    associated with the current object.

    {b Important Note for Frama-C Users:} Unless you really know what you are
    doing, you should probably inherit from the
    {!Visitor.generic_frama_c_visitor} instead of {!genericCilVisitor} or
1547
    {!nopCilVisitor}
1548

1549
1550
    @plugin development guide *)
class type cilVisitor = object
1551
  method behavior: Visitor_behavior.t
1552
1553
1554
1555
  (** the kind of behavior expected for the behavior.
      @plugin development guide *)

  method project: Project.t option
Allan Blanchard's avatar
Allan Blanchard committed
1556
1557
  (** Project the visitor operates on. Non-nil for copy visitor.
      @since Oxygen-20120901 *)
1558
1559

  method plain_copy_visitor: cilVisitor
Allan Blanchard's avatar
Allan Blanchard committed
1560
  (** a visitor who only does copies of the nodes according to [behavior] *)
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
1572
1573
1574
1575
1576
1577
1578
1579
1580
1581
1582
1583
1584
1585
1586
1587
1588
1589
1590
1591
1592
1593
1594

  method vfile: file -> file visitAction
  (** visit a whole file.
      @plugin development guide *)

  method vvdec: varinfo -> varinfo visitAction
  (** Invoked for each variable declaration. The children to be traversed
      are those corresponding to the type and attributes of the variable.
      Note that variable declarations are [GVar], [GVarDecl], [GFun] and
      [GFunDecl] globals, the formals of functions prototypes, and the
      formals and locals of function definitions. This means that the list
      of formals of a function may be traversed multiple times if there exists
      both a declaration and a definition, or multiple declarations.
      @plugin development guide *)

  method vvrbl: varinfo -> varinfo visitAction
  (** Invoked on each variable use. Here only the [SkipChildren] and
      [ChangeTo] actions make sense since there are no subtrees. Note that
      the type and attributes of the variable are not traversed for a
      variable use.
      @plugin development guide *)

  method vexpr: exp -> exp visitAction
  (** Invoked on each expression occurrence. The subtrees are the
      subexpressions, the types (for a [Cast] or [SizeOf] expression) or the
      variable use.
      @plugin development guide *)

  method vlval: lval -> lval visitAction
  (** Invoked on each lvalue occurrence *)

  method voffs: offset -> offset visitAction
  (** Invoked on each offset occurrence that is *not* as part of an
      initializer list specification, i.e. in an lval or recursively inside an
1595
      offset.
1596
1597
1598
1599
1600
1601
1602
1603
1604
1605
1606
1607
1608
1609
1610
1611
      @plugin development guide *)

  method vinitoffs: offset -> offset visitAction
  (** Invoked on each offset appearing in the list of a
      CompoundInit initializer.  *)

  method vinst: instr -> instr list visitAction
  (** Invoked on each instruction occurrence. The [ChangeTo] action can
      replace this instruction with a list of instructions *)

  method vstmt: stmt -> stmt visitAction
  (** Control-flow statement. The default [DoChildren] action does not create a
      new statement when the components change. Instead it updates the contents
      of the original statement. This is done to preserve the sharing with
      [Goto] and [Case] statements that point to the original statement. If you
      use the [ChangeTo] action then you should take care of preserving that
1612
      sharing yourself.
1613
1614
1615
1616
      @plugin development guide *)

  method vblock: block -> block visitAction
  (** Block. *)
1617
1618

  method vfunc: fundec -> fundec visitAction
1619
1620
1621
1622
1623
1624
1625
1626
1627
1628
  (** Function definition. Replaced in place. *)

  method vglob: global -> global list visitAction
  (** Global (vars, types, etc.)
      @plugin development guide *)

  method vinit: varinfo -> offset -> init -> init visitAction
  (** Initializers. Pass the global where this occurs, and the offset *)

  method vlocal_init: varinfo -> local_init -> local_init visitAction
Allan Blanchard's avatar
Allan Blanchard committed
1629
  (** local initializer. pass the variable under initialization. *)
1630
1631
1632
1633
1634
1635
1636

  method vtype: typ -> typ visitAction
  (** Use of some type. For typedef, struct, union and enum, the visit is
      done once at the global defining the type. Thus, children of
      [TComp], [TEnum] and [TNamed] are not visited again. *)

  method vcompinfo: compinfo -> compinfo visitAction
Allan Blanchard's avatar
Allan Blanchard committed
1637
  (** declaration of a struct/union *)
1638
1639

  method venuminfo: enuminfo -> enuminfo visitAction
Allan Blanchard's avatar
Allan Blanchard committed
1640
  (** declaration of an enumeration *)
1641
1642

  method vfieldinfo: fieldinfo -> fieldinfo visitAction
Allan Blanchard's avatar
Allan Blanchard committed
1643
  (** visit the declaration of a field of a structure or union *)
1644
1645

  method venumitem: enumitem -> enumitem visitAction
Allan Blanchard's avatar
Allan Blanchard committed
1646
  (** visit the declaration of an enumeration item *)
1647
1648
1649
1650
1651
1652
1653
1654
1655
1656
1657
1658
1659
1660
1661
1662
1663
1664
1665
1666
1667
1668
1669
1670
1671

  method vattr: attribute -> attribute list visitAction
  (** Attribute. Each attribute can be replaced by a list *)

  method vattrparam: attrparam -> attrparam visitAction
  (** Attribute parameters. *)

  method queueInstr: instr list -> unit
  (** Add here instructions while visiting to queue them to precede the
      current statement being processed. Use this method only
      when you are visiting an expression that is inside a function body, or a
      statement, because otherwise there will no place for the visitor to place
      your instructions. *)

  (** Gets the queue of instructions and resets the queue. This is done
      automatically for you when you visit statements. *)
  method unqueueInstr: unit -> instr list

  method current_stmt: stmt option
  (** link to the current statement being visited.

      {b NB:} for copy visitor, the stmt is the original one (use
      [get_stmt] to obtain the corresponding copy) *)

  method current_kinstr: kinstr
Allan Blanchard's avatar
Allan Blanchard committed
1672
1673
1674
1675
  (** [Kstmt stmt] when visiting statement stmt, [Kglobal] when called outside
      of a statement.
      @since Carbon-20101201
      @plugin development guide *)
1676
1677
1678
1679
1680

  method push_stmt : stmt -> unit
  method pop_stmt : stmt -> unit

  method current_func: fundec option
Allan Blanchard's avatar
Allan Blanchard committed
1681
  (** link to the current function being visited.
1682

Allan Blanchard's avatar
Allan Blanchard committed
1683
      {b NB:} for copy visitors, the fundec is the original one. *)
1684
1685
1686
1687
1688
1689
1690
1691
1692
1693
1694
1695
1696
1697
1698
1699
1700
1701
1702
1703
1704
1705
1706
1707
1708
1709
1710
1711
1712
1713
1714
1715
1716
1717
1718
1719
1720
1721
1722
1723
1724
1725
1726
1727
1728
1729
1730
1731
1732
1733
1734
1735
1736
1737
1738
1739
1740
1741
1742
1743
1744
1745
1746
1747
1748
1749
1750
1751
1752
1753
1754
1755
1756
1757
1758
1759
1760
1761
1762
1763
  method set_current_func: fundec -> unit
  method reset_current_func: unit -> unit

  method vlogic_type: logic_type -> logic_type visitAction
  method vmodel_info: model_info -> model_info visitAction
  method videntified_term: identified_term -> identified_term visitAction
  method vterm: term -> term visitAction
  method vterm_node: term_node -> term_node visitAction
  method vterm_lval: term_lval -> term_lval visitAction
  method vterm_lhost: term_lhost -> term_lhost visitAction
  method vterm_offset: term_offset -> term_offset visitAction
  method vlogic_label: logic_label -> logic_label visitAction
  method vlogic_info_decl: logic_info -> logic_info visitAction
  (** @plugin development guide *)

  method vlogic_info_use: logic_info -> logic_info visitAction
  (** @plugin development guide *)

  method vlogic_type_info_decl: logic_type_info -> logic_type_info visitAction
  (** @plugin development guide *)

  method vlogic_type_info_use: logic_type_info -> logic_type_info visitAction
  (** @plugin development guide *)

  method vlogic_type_def: logic_type_def -> logic_type_def visitAction
  method vlogic_ctor_info_decl: logic_ctor_info -> logic_ctor_info visitAction
  (** @plugin development guide *)

  method vlogic_ctor_info_use: logic_ctor_info -> logic_ctor_info visitAction
  (** @plugin development guide *)

  method vlogic_var_decl: logic_var -> logic_var visitAction
  (** @plugin development guide *)

  method vlogic_var_use: logic_var -> logic_var visitAction
  (** @plugin development guide *)

  method vquantifiers: quantifiers -> quantifiers visitAction

  method videntified_predicate:
    identified_predicate -> identified_predicate visitAction

  method vpredicate_node: predicate_node -> predicate_node visitAction
  method vpredicate: predicate -> predicate visitAction
  method vbehavior: funbehavior -> funbehavior visitAction
  method vspec: funspec -> funspec visitAction
  method vassigns: assigns -> assigns visitAction

  method vfrees:
    identified_term list -> identified_term list visitAction
  (**	@since Oxygen-20120901 *)

  method vallocates:
    identified_term list -> identified_term list visitAction
  (**	@since Oxygen-20120901 *)

  method vallocation: allocation -> allocation visitAction
  (**	@since Oxygen-20120901 *)

  method vloop_pragma: loop_pragma -> loop_pragma visitAction
  method vslice_pragma: slice_pragma -> slice_pragma visitAction
  method vimpact_pragma: impact_pragma -> impact_pragma visitAction

  method vdeps: deps -> deps visitAction
  method vfrom: from -> from visitAction
  method vcode_annot: code_annotation -> code_annotation visitAction
  method vannotation: global_annotation -> global_annotation visitAction

  method fill_global_tables: unit
  (** fill the global environment tables at the end of a full copy in a
      new project.
      @plugin development guide *)

  method get_filling_actions: (unit -> unit) Queue.t
  (** get the queue of actions to be performed at the end of a full copy.
      @plugin development guide *)

end

(** Indicates how an extended behavior clause is supposed to be visited.
1764
    The default behavior is [DoChildren], which ends up visiting
1765
1766
1767
1768
1769
1770
    each identified predicate in the list and leave the id as is.

    @plugin development guide

    @since Sodium-20150201
    @modify Silicon-20161101
Andre Maroneze's avatar
Andre Maroneze committed
1771
    @deprecated 21.0-Scandium
1772
1773
1774
1775
1776
*)
val register_behavior_extension:
  string ->
  (cilVisitor -> acsl_extension_kind -> (acsl_extension_kind) visitAction)
  -> unit
1777
[@@ deprecated "Use Acsl_extension.register_behavior instead (arg: ~visitor)"]
1778
1779
1780

(**/**)
class internal_genericCilVisitor:
1781
  fundec option ref -> Visitor_behavior.t -> (unit->unit) Queue.t -> cilVisitor
1782
1783
1784
1785
(**/**)

(** generic visitor, parameterized by its copying behavior.
    Traverses the CIL tree without modifying anything *)
1786
class genericCilVisitor: Visitor_behavior.t -> cilVisitor
1787
1788
1789
1790
1791
1792
1793
1794
1795
1796
1797
1798
1799
1800
1801
1802
1803
1804
1805
1806
1807
1808
1809
1810
1811
1812
1813
1814
1815
1816
1817
1818
1819
1820
1821
1822
1823
1824
1825
1826
1827
1828
1829
1830
1831
1832
1833
1834
1835
1836

(** Default in place visitor doing nothing and operating on current project. *)
class nopCilVisitor: cilVisitor

(** {3 Generic visit functions} *)
(** [doVisit vis deepCopyVisitor copy action children node]
    visits a [node]
    (or its copy according to the result of [copy]) and if needed
    its [children]. {b Do not use it if you don't understand Cil visitor
    mechanism}
    @param vis the visitor performing the needed transformations. The open
    type allows for extensions to Cil to be visited by the same mechanisms.
    @param deepCopyVisitor a generator for a visitor of the same type
    of the current one that performs a deep copy of the AST.
    Needed when the visitAction is [SkipChildren] or [ChangeTo] and [vis]
    is a copy visitor (we need to finish the copy anyway)
    @param copy function that may return a copy of the actual node.
    @param action the visiting function for the current node
    @param children what to do on the children of the current node
    @param node the current node
*)
val doVisit:
  'visitor -> 'visitor ->
  ('a -> 'a) ->
  ('a -> 'a visitAction) ->
  ('visitor -> 'a -> 'a) -> 'a -> 'a

(** same as above, but can return a list of nodes *)
val doVisitList:
  'visitor -> 'visitor ->
  ('a -> 'a) ->
  ('a -> 'a list visitAction) ->
  ('visitor -> 'a -> 'a) -> 'a -> 'a list

(* other cil constructs *)

(** {3 Visitor's entry points} *)

(** Visit a file. This will re-cons all globals TWICE (so that it is
 * tail-recursive). Use {!Cil.visitCilFileSameGlobals} if your visitor will
 * not change the list of globals.
    @plugin development guide *)
val visitCilFileCopy: cilVisitor -> file -> file

(** Same thing, but the result is ignored. The given visitor must thus be
    an inplace visitor. Nothing is done if the visitor is a copy visitor.
    @plugin development guide *)
val visitCilFile: cilVisitor -> file -> unit

(** A visitor for the whole file that does not *physically* change the
Allan Blanchard's avatar
Allan Blanchard committed
1837
1838
1839
1840
    globals (but maybe changes things inside the globals through
    side-effects). Use this function instead of {!Cil.visitCilFile}
    whenever appropriate because it is more efficient for long files.
    @plugin development guide *)
1841
1842
1843
1844
1845
1846
1847
1848
1849
1850
1851
1852
1853
1854
1855
1856
1857
1858
1859
1860
1861
1862
1863
1864
1865
1866
1867
1868
1869
1870
1871
1872
1873
1874
1875
1876
1877
1878
1879
val visitCilFileSameGlobals: cilVisitor -> file -> unit

(** Visit a global *)
val visitCilGlobal: cilVisitor -> global -> global list

(** Visit a function definition *)
val visitCilFunction: cilVisitor -> fundec -> fundec

(* Visit an expression *)
val visitCilExpr: cilVisitor -> exp -> exp

val visitCilEnumInfo: cilVisitor -> enuminfo -> enuminfo

(** Visit an lvalue *)
val visitCilLval: cilVisitor -> lval -> lval

(** Visit an lvalue or recursive offset *)
val visitCilOffset: cilVisitor -> offset -> offset

(** Visit an initializer offset *)
val visitCilInitOffset: cilVisitor -> offset -> offset

(** Visit a local initializer (with the local being initialized). *)
val visitCilLocal_init: cilVisitor -> varinfo -> local_init -> local_init

(** Visit an instruction *)
val visitCilInstr: cilVisitor -> instr -> instr list

(** Visit a statement *)
val visitCilStmt: cilVisitor -> stmt -> stmt

(** Visit a block *)
val visitCilBlock: cilVisitor -> block -> block

(** Mark the given block as candidate to be flattened into its parent block,
    after returning from its visit. This is not systematic, as the environment
    might prevent it (e.g. if the preceding statement is a statement contract
    or a slicing/pragma annotation, or if there are labels involved). Use
    that whenever you're creating a block in order to hold multiple statements
1880
1881
1882
    as a result of visiting a single statement. If the block contains local
    variables, it will not be marked as transient, since removing it will
    change the scope of those variables.
1883
1884

    @raise Fatal error if the given block attempts to declare local variables
1885
    and contain definitions of local variables that are not part of the block.
1886
1887

    @since Phosphorus-20170501-beta1
1888
    @modify 19.0-Potassium: do not raise fatal as soon as the block has locals
1889
1890
1891
1892
1893
1894
1895
1896
1897
1898
1899
1900
1901
1902
1903
1904
1905
1906
1907
1908
1909
1910
1911
1912
1913
1914
1915
1916
1917
1918
1919
1920
1921
1922
1923
1924
1925
1926
1927
1928
1929
1930
1931
1932
1933
1934
1935
1936
1937
1938
1939
1940
1941
1942
*)
val transient_block: block -> block

(** tells whether the block has been marked as transient

    @since Phosphorus-20170501-beta1.
*)
val is_transient_block: block -> bool

(** [flatten_transient_sub_blocks b] flattens all direct sub-blocks of [b]
    that have been marked as cleanable, whenever possible

    @since Phosphorus-20170501-beta1
*)
val flatten_transient_sub_blocks: block -> block

(**/**)

(** Internal usage only. *)

(** Indicates that the potentially transient block given as argument
    must in fact be preserved after the visit. The resulting block will
    be marked as non-scoping.

    @since Phosphorus-20170501-beta1.
*)
val block_of_transient: block -> block

(**/**)

(** Visit a type *)
val visitCilType: cilVisitor -> typ -> typ

(** Visit a variable declaration *)
val visitCilVarDecl: cilVisitor -> varinfo -> varinfo

(** Visit an initializer, pass also the global to which this belongs and the
 * offset. *)
val visitCilInit: cilVisitor -> varinfo -> offset -> init -> init

(** Visit a list of attributes *)
val visitCilAttributes: cilVisitor -> attribute list -> attribute list

val visitCilAnnotation: cilVisitor -> global_annotation -> global_annotation

val visitCilCodeAnnotation: cilVisitor -> code_annotation -> code_annotation