1
(**************************************************************************)
3
(* Copyright (C) 2001-2003, *)
4
(* George C. Necula <necula@cs.berkeley.edu> *)
5
(* Scott McPeak <smcpeak@cs.berkeley.edu> *)
6
(* Wes Weimer <weimer@cs.berkeley.edu> *)
7
(* Ben Liblit <liblit@cs.berkeley.edu> *)
8
(* All rights reserved. *)
10
(* Redistribution and use in source and binary forms, with or without *)
11
(* modification, are permitted provided that the following conditions *)
14
(* 1. Redistributions of source code must retain the above copyright *)
15
(* notice, this list of conditions and the following disclaimer. *)
17
(* 2. Redistributions in binary form must reproduce the above copyright *)
18
(* notice, this list of conditions and the following disclaimer in the *)
19
(* documentation and/or other materials provided with the distribution. *)
21
(* 3. The names of the contributors may not be used to endorse or *)
22
(* promote products derived from this software without specific prior *)
23
(* written permission. *)
25
(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *)
26
(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *)
27
(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *)
28
(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *)
29
(* COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *)
30
(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *)
31
(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; *)
32
(* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER *)
33
(* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT *)
34
(* LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN *)
35
(* ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE *)
36
(* POSSIBILITY OF SUCH DAMAGE. *)
38
(* File modified by CEA (Commissariat � l'�nergie Atomique). *)
39
(**************************************************************************)
43
* CIL: An intermediate language for analyzing C programs.
49
(** CIL original API documentation is available as
50
* an html version at http://manju.cs.berkeley.edu/cil.
51
@plugin development guide *)
54
(** Call this function to perform some initialization. Call if after you have
55
* set [Cil.msvcMode]. *)
56
val initCIL: unit -> unit
59
(** This are the CIL version numbers. A CIL version is a number of the form
60
* M.m.r (major, minor and release) *)
61
val cilVersion: string
62
val cilVersionMajor: int
63
val cilVersionMinor: int
64
val cilVersionRevision: int
66
(** This module defines the abstract syntax of CIL. It also provides utility
67
* functions for traversing the CIL data structures, and pretty-printing
68
* them. The parser for both the GCC and MSVC front-ends can be invoked as
69
* [Frontc.parse: string -> unit ->] {!Cil_types.file}. This function must be given
70
* the name of a preprocessed C file and will return the top-level data
71
* structure that describes a whole source file. By default the parsing and
72
* elaboration into CIL is done as for GCC source. If you want to use MSVC
73
* source you must set the [Cil.msvcMode] to [true] and must also invoke the
74
* function [Frontc.setMSVCMode: unit -> unit]. *)
78
type theMachine = private
79
{ (** Whether the pretty printer should print output for the MS VC
80
compiler. Default is GCC *)
81
mutable msvcMode: bool;
82
(** Whether to use the logical operands LAnd and LOr. By default, do not
83
use them because they are unlike other expressions and do not
84
evaluate both of their operands *)
85
mutable useLogicalOperators: bool;
86
mutable theMachine: mach;
87
mutable lowerConstants: bool; (** Do lower constants (default true) *)
88
mutable insertImplicitCasts: bool; (** Do insert implicit casts
90
(** Whether the machine is little endian. *)
91
mutable little_endian: bool;
92
(** Whether "char" is unsigned. *)
93
mutable char_is_unsigned: bool;
94
(** Whether the compiler generates assembly labels by prepending "_" to
95
the identifier. That is, will function foo() have the label "foo", or
97
mutable underscore_name: bool;
98
(** Wether enum are signed or not. *)
99
mutable enum_are_signed: bool;
100
mutable stringLiteralType: typ;
101
(** An unsigned integer type that fits pointers. Depends on
103
mutable upointType: typ;
104
mutable wcharKind: ikind; (** An integer type that fits wchar_t. *)
105
mutable wcharType: typ;
106
mutable ptrdiffKind: ikind; (** An integer type that fits ptrdiff_t. *)
107
mutable ptrdiffType: typ;
108
mutable typeOfSizeOf: typ; (** An integer type that is the type of
110
mutable kindOfSizeOf: ikind (** The integer kind of
111
{!Cil.typeOfSizeOf}. *)
114
val theMachine : theMachine
115
(** Current machine description *)
117
val selfMachine: Project.Computation.t
119
val set_msvcMode: bool -> unit
120
(** Must be called before {!Cil.initCIL}. *)
122
(** Styles of printing line directives *)
123
type lineDirectiveStyle =
124
| LineComment (** Before every element, print the line
125
* number in comments. This is ignored by
126
* processing tools (thus errors are reproted
127
* in the CIL output), but useful for
128
* visual inspection *)
129
| LineCommentSparse (** Like LineComment but only print a line
130
* directive for a new source line *)
131
| LinePreprocessorInput (** Use #line directives *)
132
| LinePreprocessorOutput (** Use # nnn directives (in gcc mode) *)
135
{ (** How to print line directives *)
136
mutable lineDirectiveStyle: lineDirectiveStyle option;
137
(** Whether we print something that will only be used as input to our own
138
parser. In that case we are a bit more liberal in what we print *)
139
mutable print_CIL_Input: bool;
140
(** Whether to print the CIL as they are, without trying to be smart and
141
print nicer code. Normally this is false, in which case the pretty
142
printer will turn the while(1) loops of CIL into nicer loops, will not
143
print empty "else" blocks, etc. These is one case howewer in which if
144
you turn this on you will get code that does not compile: if you use
145
varargs the __builtin_va_arg function will be printed in its internal
147
mutable printCilAsIs: bool;
148
(** The length used when wrapping output lines. Setting this variable to
149
a large integer will prevent wrapping and make #line directives more
151
mutable lineLength: int;
152
(** Emit warnings when truncating integer constants (default true) *)
153
mutable warnTruncate: bool }
155
val miscState: miscState
157
(** To be able to add/remove features easily, each feature should be package
158
* as an interface with the following interface. These features should be *)
159
type featureDescr = {
160
fd_enabled: bool ref;
161
(** The enable flag. Set to default value *)
164
(** This is used to construct an option "--doxxx" and "--dontxxx" that
165
* enable and disable the feature *)
167
fd_description: string;
168
(** A longer name that can be used to document the new options *)
170
fd_extraopt: (string * Arg.spec * string) list;
171
(** Additional command line options *)
173
fd_doit: (file -> unit);
174
(** This performs the transformation *)
177
(** Whether to perform a CIL consistency checking after this stage, if
178
* checking is enabled (--check is passed to cilly). Set this to true if
179
* your feature makes any changes for the program. *)
182
(** Comparison function for tsets.
183
** Compares first by filename, then line, then byte *)
184
val compareLoc: location -> location -> int
186
(** {b Values for manipulating globals} *)
188
(** Make an empty function *)
189
val emptyFunction: string -> fundec
191
(** Update the formals of a [fundec] and make sure that the function type
192
has the same information. Will copy the name as well into the type. *)
193
val setFormals: fundec -> varinfo list -> unit
195
(** Takes as input a function type (or a typename on it) and return its
197
val getReturnType: typ -> typ
199
(** Change the return type of the function passed as 1st argument to be
200
the type passed as 2nd argument. *)
201
val setReturnTypeVI: varinfo -> typ -> unit
202
val setReturnType: fundec -> typ -> unit
204
(** Set the types of arguments and results as given by the function type
205
* passed as the second argument. Will not copy the names from the function
206
* type to the formals *)
207
val setFunctionType: fundec -> typ -> unit
209
(** Set the type of the function and make formal arguments for them *)
210
val setFunctionTypeMakeFormals: fundec -> typ -> unit
212
(** Update the smaxid after you have populated with locals and formals
213
* (unless you constructed those using {!Cil.makeLocalVar} or
214
* {!Cil.makeTempVar}. *)
215
val setMaxId: fundec -> unit
217
val selfFormalsDecl: Project.Computation.t
218
(** state of the table associating formals to each prototype. *)
220
val makeFormalsVarDecl: (string * typ * attributes) -> varinfo
221
(** creates a new varinfo for the parameter of a prototype. *)
223
(** Update the formals of a function declaration from its identifier and its
224
type. For a function definition, use {!Cil.setFormals}.
225
Do nothing if the type is not a function type or if the list of
228
val setFormalsDecl: varinfo -> typ -> unit
230
(** replace to formals of a function declaration with the given
233
val unsafeSetFormalsDecl: varinfo -> varinfo list -> unit
235
(** Get the formals of a function declaration registered with
236
{!Cil.setFormalsDecl}.
237
@raise Not_found if the function is not registered (this is in particular
238
the case for prototypes with an empty list of arguments.
239
See {!Cil.setFormalsDecl})
241
val getFormalsDecl: varinfo -> varinfo list
246
(** Get the global initializer and create one if it does not already exist.
247
* When it creates a global initializer it attempts to place a call to it in
248
* the main function named by the optional argument (default "main") *)
249
val getGlobInit: ?main_name:string -> file -> fundec
251
(** Iterate over all globals, including the global initializer *)
252
val iterGlobals: file -> (global -> unit) -> unit
254
(** Fold over all globals, including the global initializer *)
255
val foldGlobals: file -> ('a -> global -> 'a) -> 'a -> 'a
257
(** Map over all globals, including the global initializer and change things
259
val mapGlobals: file -> (global -> global) -> unit
261
(** Find a function or function prototype with the given name in the file.
262
* If it does not exist, create a prototype with the given type, and return
263
* the new varinfo. This is useful when you need to call a libc function
264
* whose prototype may or may not already exist in the file.
266
* Because the new prototype is added to the start of the file, you shouldn't
267
* refer to any struct or union types in the function type.*)
268
val findOrCreateFunc: file -> string -> typ -> varinfo
271
val next: unit -> int
275
(** Return [true] on case and default labels, [false] otherwise. *)
276
val is_case_label: label -> bool
278
(** Prepare a function for CFG information computation by
279
* {!Cil.computeCFGInfo}. This function converts all [Break], [Switch],
280
* [Default] and [Continue] {!Cil_types.stmtkind}s and {!Cil_types.label}s into [If]s
281
* and [Goto]s, giving the function body a very CFG-like character. This
282
* function modifies its argument in place. *)
283
val prepareCFG: ?keepSwitch:bool -> fundec -> unit
285
(** Compute the CFG information for all statements in a fundec and return a
286
* list of the statements. The input fundec cannot have [Break], [Switch],
287
* [Default], or [Continue] {!Cil_types.stmtkind}s or {!Cil_types.label}s. Use
288
* {!Cil.prepareCFG} to transform them away. The second argument should
289
* be [true] if you wish a global statement number, [false] if you wish a
290
* local (per-function) statement numbering. The list of statements is set
291
* in the sallstmts field of a fundec.
293
* NOTE: unless you want the simpler control-flow graph provided by
294
* prepareCFG, or you need the function's smaxstmtid and sallstmt fields
295
* filled in, we recommend you use [Cfg.computeFileCFG] instead of this
296
* function to compute control-flow information.
297
* [Cfg.computeFileCFG] is newer and will handle switch, break, and
298
* continue correctly.*)
299
val computeCFGInfo: fundec -> bool -> unit
302
(** Create a deep copy of a function. There should be no sharing between the
303
* copy and the original function *)
304
val copyFunction: fundec -> string -> fundec
307
(** CIL keeps the types at the beginning of the file and the variables at the
308
* end of the file. This function will take a global and add it to the
309
* corresponding stack. Its operation is actually more complicated because if
310
* the global declares a type that contains references to variables (e.g. in
311
* sizeof in an array length) then it will also add declarations for the
312
* variables to the types stack *)
313
val pushGlobal: global -> types: global list ref
314
-> variables: global list ref -> unit
316
(** An empty statement. Used in pretty printing *)
317
val invalidStmt: stmt
319
(** A list of the built-in functions for the current compiler (GCC or
320
* MSVC, depending on [!msvcMode]). Maps the name to the
321
* result and argument types, and whether it is vararg.
322
* Initialized by {!Cil.initCIL}
324
* This map replaces [gccBuiltins] and [msvcBuiltins] in previous
326
module BuiltinFunctions :
327
Computation.HASHTBL_OUTPUT with type key = string
328
and type data = typ * typ list * bool
330
(** This is used as the location of the prototypes of builtin functions. *)
331
val builtinLoc: location
333
(** Returns a location that ranges over the two locations in arguments. *)
334
val range_loc: location -> location -> location
336
(** {b Values for manipulating initializers} *)
338
(** Make a initializer for zero-ing a data type *)
339
val makeZeroInit: typ -> init
341
(** Fold over the list of initializers in a Compound (not also the nested
342
* ones). [doinit] is called on every present initializer, even if it is of
343
* compound type. The parameters of [doinit] are: the offset in the compound
344
* (this is [Field(f,NoOffset)] or [Index(i,NoOffset)]), the initializer
345
* value, expected type of the initializer value, accumulator. In the case of
346
* arrays there might be missing zero-initializers at the end of the list.
347
* These are scanned only if [implicit] is true. This is much like
348
* [List.fold_left] except we also pass the type of the initializer.
350
* This is a good way to use it to scan even nested initializers :
352
let rec myInit (lv: lval) (i: init) (acc: 'a) : 'a =
354
SingleInit e -> ... do something with lv and e and acc ...
355
| CompoundInit (ct, initl) ->
356
foldLeftCompound ~implicit:false
357
~doinit:(fun off' i' t' acc ->
358
myInit (addOffsetLval lv off') i' acc)
364
val foldLeftCompound:
366
doinit: (offset -> init -> typ -> 'a -> 'a) ->
368
initl: (offset * init) list ->
371
(** {2 Values for manipulating types} *)
376
(** is the given type "void"? *)
377
val isVoidType: typ -> bool
379
(** is the given type "void *"? *)
380
val isVoidPtrType: typ -> bool
401
val charConstPtrType: typ
409
(** unsigned int * *)
415
(** Returns true if and only if the given integer type is signed. *)
416
val isSigned: ikind -> bool
418
(** Returns true if and only if the given type is a signed integer type. *)
419
val isSignedInteger: typ -> bool
422
(** Creates a a (potentially recursive) composite type. The arguments are:
423
* (1) a boolean indicating whether it is a struct or a union, (2) the name
424
* (always non-empty), (3) a function that when given a representation of the
425
* structure type constructs the type of the fields recursive type (the first
426
* argument is only useful when some fields need to refer to the type of the
427
* structure itself), and (4) a list of attributes to be associated with the
428
* composite type. The resulting compinfo has the field "cdefined" only if
429
* the list of fields is non-empty. *)
430
val mkCompInfo: bool -> (* whether it is a struct or a union *)
431
string -> (* name of the composite type; cannot be empty *)
433
(string * typ * int option * attributes * location) list) ->
434
(* a function that when given a forward
435
representation of the structure type constructs the type of
436
the fields. The function can ignore this argument if not
437
constructing a recursive type. *)
438
attributes -> compinfo
440
(** Makes a shallow copy of a {!Cil_types.compinfo} changing the name and the key.*)
441
val copyCompInfo: compinfo -> string -> compinfo
443
(** This is a constant used as the name of an unnamed bitfield. These fields
444
do not participate in initialization and their name is not printed. *)
445
val missingFieldName: string
447
(** Get the full name of a comp *)
448
val compFullName: compinfo -> string
450
(** Returns true if this is a complete type.
451
This means that sizeof(t) makes sense.
452
Incomplete types are not yet defined
453
structures and empty arrays. *)
454
val isCompleteType: typ -> bool
456
(** Unroll a type until it exposes a non
457
* [TNamed]. Will collect all attributes appearing in [TNamed]!!! *)
458
val unrollType: typ -> typ
460
(** Unroll all the TNamed in a type (even under type constructors such as
461
* [TPtr], [TFun] or [TArray]. Does not unroll the types of fields in [TComp]
462
* types. Will collect all attributes *)
463
val unrollTypeDeep: typ -> typ
465
(** Separate out the storage-modifier name attributes *)
466
val separateStorageModifiers: attribute list -> attribute list * attribute list
468
(** True if the argument is a character type (i.e. plain, signed or unsigned) *)
469
val isCharType: typ -> bool
471
(** True if the argument is a pointer to a character type
472
(i.e. plain, signed or unsigned) *)
473
val isCharPtrType: typ -> bool
475
(** True if the argument is an array of a character type
476
(i.e. plain, signed or unsigned) *)
477
val isCharArrayType: typ -> bool
479
(** True if the argument is a logic integral type (i.e. integer or enum) *)
480
val isIntegralType: typ -> bool
482
(** True if the argument is an integral type (i.e. integer or enum), either
483
C or mathematical one *)
484
val isLogicIntegralType: logic_type -> bool
486
(** True if the argument is a floating point type *)
487
val isFloatingType: typ -> bool
489
(** True if the argument is a floating point type *)
490
val isLogicFloatType: logic_type -> bool
492
(** True if the argument is a C floating point type or logic 'real' type *)
493
val isLogicRealOrFloatType: logic_type -> bool
495
(** True if the argument is an arithmetic type (i.e. integer, enum or
497
val isArithmeticType: typ -> bool
499
(** True if the argument is a logic arithmetic type (i.e. integer, enum or
500
floating point, either C or mathematical one *)
501
val isLogicArithmeticType: logic_type -> bool
503
(** True if the argument is a pointer type *)
504
val isPointerType: typ -> bool
506
(** True if the argument is the type for reified C types *)
507
val isTypeTagType: logic_type -> bool
509
(** True if the argument is a function type.
510
@plugin development guide *)
511
val isFunctionType: typ -> bool
513
(** Obtain the argument list ([] if None) *)
515
(string * typ * attributes) list option -> (string * typ * attributes) list
517
(** True if the argument is an array type *)
518
val isArrayType: typ -> bool
520
(** True if the argument is a struct of union type *)
521
val isStructOrUnionType: typ -> bool
523
(** Raised when {!Cil.lenOfArray} fails either because the length is [None]
524
* or because it is a non-constant expression *)
527
(** Call to compute the array length as present in the array type, to an
528
* integer. Raises {!Cil.LenOfArray} if not able to compute the length, such
529
* as when there is no length or the length is not a constant. *)
530
val lenOfArray: exp option -> int
531
val lenOfArray64: exp option -> Int64.t
533
(** Return a named fieldinfo in compinfo, or raise Not_found *)
534
val getCompField: compinfo -> string -> fieldinfo
537
(** A datatype to be used in conjunction with [existsType] *)
539
ExistsTrue (** We have found it *)
540
| ExistsFalse (** Stop processing this branch *)
541
| ExistsMaybe (** This node is not what we are
542
* looking for but maybe its
545
(** Scans a type by applying the function on all elements.
546
When the function returns ExistsTrue, the scan stops with
547
true. When the function returns ExistsFalse then the current branch is not
548
scanned anymore. Care is taken to
549
apply the function only once on each composite type, thus avoiding
550
circularity. When the function returns ExistsMaybe then the types that
551
construct the current type are scanned (e.g. the base type for TPtr and
552
TArray, the type of fields for a TComp, etc). *)
553
val existsType: (typ -> existsAction) -> typ -> bool
556
(** Given a function type split it into return type,
557
* arguments, is_vararg and attributes. An error is raised if the type is not
559
val splitFunctionType:
560
typ -> typ * (string * typ * attributes) list option * bool * attributes
561
(** Same as {!Cil.splitFunctionType} but takes a varinfo. Prints a nicer
562
* error message if the varinfo is not for a function *)
563
val splitFunctionTypeVI:
565
typ * (string * typ * attributes) list option * bool * attributes
568
(** {b Type signatures} *)
570
(** Type signatures. Two types are identical iff they have identical
571
* signatures. These contain the same information as types but canonicalized.
572
* For example, two function types that are identical except for the name of
573
* the formal arguments are given the same signature. Also, [TNamed]
574
* constructors are unrolled. You shoud use [Cilutil.equals] to compare type
575
* signatures because they might still contain circular structures (through
576
* attributes, and sizeof) *)
578
(** Compute a type signature *)
579
val typeSig: typ -> typsig
581
(** Like {!Cil.typeSig} but customize the incorporation of attributes.
582
Use ~ignoreSign:true to convert all signed integer types to unsigned,
583
so that signed and unsigned will compare the same. *)
584
val typeSigWithAttrs: ?ignoreSign:bool -> (attributes -> attributes) -> typ -> typsig
586
(** Replace the attributes of a signature (only at top level) *)
587
val setTypeSigAttrs: attributes -> typsig -> typsig
589
(** Get the top-level attributes of a signature *)
590
val typeSigAttrs: typsig -> attributes
592
(*********************************************************)
595
(** Make a varinfo. Use this (rarely) to make a raw varinfo. Use other
596
* functions to make locals ({!Cil.makeLocalVar} or {!Cil.makeFormalVar} or
597
* {!Cil.makeTempVar}) and globals ({!Cil.makeGlobalVar}). Note that this
598
* function will assign a new identifier. The [logic] argument defaults to [false]
599
* and should be used to create a varinfo such that [varinfo.vlogic=true].
600
* The first argument specifies whether the varinfo is for a global and
601
the second is for formals. *)
602
val makeVarinfo: ?logic:bool -> bool -> bool -> string -> typ -> varinfo
604
(** Make a formal variable for a function declaration. Insert it in both the
605
sformals and the type of the function. You can optionally specify where to
606
insert this one. If where = "^" then it is inserted first. If where = "$"
607
then it is inserted last. Otherwise where must be the name of a formal
608
after which to insert this. By default it is inserted at the end. *)
609
val makeFormalVar: fundec -> ?where:string -> string -> typ -> varinfo
611
(** Make a local variable and add it to a function's slocals (only if insert =
612
true, which is the default). Make sure you know what you are doing if you
614
val makeLocalVar: fundec -> ?insert:bool -> string -> typ -> varinfo
616
(** Make a pseudo-variable to use as placeholder in term to expression
617
conversions. Its logic field is set. *)
618
val makePseudoVar: typ -> varinfo
620
(** Make a temporary variable and add it to a function's slocals. The name of
621
the temporary variable will be generated based on the given name hint so
622
that to avoid conflicts with other locals.
623
Optionally, you can give the variable a description of its contents. *)
624
val makeTempVar: fundec -> ?name:string -> ?descr:string ->
625
?descrpure:bool -> typ -> varinfo
627
(** Make a global variable. Your responsibility to make sure that the name
628
is unique. [logic] defaults to [false]. *)
629
val makeGlobalVar: ?logic:bool -> string -> typ -> varinfo
631
(** Make a shallow copy of a [varinfo] and assign a new identifier.
632
If the original varinfo has an associated logic var, it is copied too and
633
associated to the copied varinfo
635
val copyVarinfo: varinfo -> string -> varinfo
637
val set_vid: varinfo -> unit
638
(** Set the vid of the given varinfo with a fresh id. *)
640
val new_raw_id: unit -> int
641
(** Generate a new ID. This will be different than any variable ID
642
that is generated by {!Cil.makeLocalVar} and friends.
643
Must not be used for setting vid: use {!set_vid} instead. *)
645
val varinfo_from_vid: int -> varinfo
646
(** @return the varinfo corresponding to the given id.
647
@raise Not_found if the given id does not match any varinfo. *)
649
val varinfos_self: Project.Computation.t
650
(** State of the varinfos table. *)
652
(** Returns the last offset in the chain. *)
653
val lastOffset: offset -> offset
655
(** Equivalent to [lastOffset] for terms. *)
656
val lastTermOffset: term_offset -> term_offset
658
(** Equivalent to [lastOffset] for tsets. *)
659
val lastTsetsOffset: tsets_offset -> tsets_offset
661
(** Add an offset at the end of an lvalue. Make sure the type of the lvalue
662
* and the offset are compatible. *)
663
val addOffsetLval: offset -> lval -> lval
665
(** Equivalent to [addOffsetLval] for terms. *)
666
val addTermOffsetLval: term_offset -> term_lval -> term_lval
668
(** Equivalent to [addOffsetLval] for tsets. *)
669
val addTsetsOffsetLval: tsets_offset -> tsets_lval -> tsets_lval
671
(** [addOffset o1 o2] adds [o1] to the end of [o2]. *)
672
val addOffset: offset -> offset -> offset
674
(** Equivalent to [addOffset] for terms. *)
675
val addTermOffset: term_offset -> term_offset -> term_offset
677
(** Remove ONE offset from the end of an lvalue. Returns the lvalue with the
678
* trimmed offset and the final offset. If the final offset is [NoOffset]
679
* then the original [lval] did not have an offset. *)
680
val removeOffsetLval: lval -> lval * offset
682
(** Remove ONE offset from the end of an offset sequence. Returns the
683
* trimmed offset and the final offset. If the final offset is [NoOffset]
684
* then the original [lval] did not have an offset. *)
685
val removeOffset: offset -> offset * offset
687
(** Compute the type of an lvalue *)
688
val typeOfLval: lval -> typ
690
(** Equivalent to [typeOfLval] for terms.
691
{b Do not use it for the [TResult] lval}
693
val typeOfTermLval: term_lval -> logic_type
695
(** Equivalent to [typeOfLval] for tsets.
696
{b Do not use it for the [TSResult] lval}
698
val typeOfTsetsLval: tsets_lval -> logic_type
700
(** type of a tsets_elem *)
701
val typeOfTsetsElem: tsets_elem -> logic_type
703
(** Compute the type of an offset from a base type *)
704
val typeOffset: typ -> offset -> typ
706
(** Equivalent to [typeOffset] for terms. *)
707
val typeTermOffset: logic_type -> term_offset -> logic_type
709
(** Equivalent to [typeOffset] for tsets. *)
710
val typeTsetsOffset: logic_type -> tsets_offset -> logic_type
713
(*******************************************************)
714
(** {b Values for manipulating expressions} *)
717
(* Construct integer constants *)
729
(** Construct an integer of a given kind, using OCaml's int64 type. If needed
730
* it will truncate the integer to be within the representable range for the
732
val kinteger64: ikind -> int64 -> exp
734
(** Construct an integer of a given kind. Converts the integer to int64 and
735
* then uses kinteger64. This might truncate the value if you use a kind
736
* that cannot represent the given integer. This can only happen for one of
737
* the Char or Short kinds *)
738
val kinteger: ikind -> int -> exp
740
(** Construct an integer of kind IInt. You can use this always since the
741
OCaml integers are 31 bits and are guaranteed to fit in an IInt *)
742
val integer: int -> exp
745
(** True if the given expression is a (possibly cast'ed)
746
character or an integer constant *)
747
val isInteger: exp -> int64 option
749
(** Convert a 64-bit int to an OCaml int, or raise an exception if that
751
val i64_to_int: int64 -> int
753
(** True if the expression is a compile-time constant *)
754
val isConstant: exp -> bool
756
(** True if the given offset contains only field nanmes or constant indices. *)
757
val isConstantOffset: offset -> bool
759
(** True if the given expression is a (possibly cast'ed) integer or character
760
constant with value zero *)
761
val isZero: exp -> bool
763
(** True if the term is the constant 0 *)
764
val isLogicZero: term -> bool
766
(** True if the given term is [\null] or a constant null pointer*)
767
val isLogicNull: term -> bool
769
val get_status : code_annotation -> annot_status
771
(** gives the value of a wide char literal. *)
772
val reduce_multichar: Cil_types.typ -> int64 list -> int64
774
(** gives the value of a char literal. *)
775
val interpret_character_constant:
776
int64 list -> Cil_types.constant * Cil_types.typ
778
(** Given the character c in a (CChr c), sign-extend it to 32 bits.
779
(This is the official way of interpreting character constants, according to
780
ISO C 6.4.4.4.10, which says that character constants are chars cast to ints)
781
Returns CInt64(sign-extened c, IInt, None) *)
782
val charConstToInt: char -> constant
784
(** Do constant folding on an expression. If the first argument is true then
785
will also compute compiler-dependent expressions such as sizeof.
786
See also {!Cil.constFoldVisitor}, which will run constFold on all
787
expressions in a given AST node.*)
788
val constFold: bool -> exp -> exp
790
(** Do constant folding on a binary operation. The bulk of the work done by
791
[constFold] is done here. If the first argument is true then
792
will also compute compiler-dependent expressions such as sizeof *)
793
val constFoldBinOp: bool -> binop -> exp -> exp -> typ -> exp
795
(** Increment an expression. Can be arithmetic or pointer type *)
796
val increm: exp -> int -> exp
798
(** Increment an expression. Can be arithmetic or pointer type *)
799
val increm64: exp -> int64 -> exp
801
(** Makes an lvalue out of a given variable *)
802
val var: varinfo -> lval
804
(** Make an AddrOf. Given an lvalue of type T will give back an expression of
805
type ptr(T). It optimizes somewhat expressions like "& v" and "& v[0]" *)
806
val mkAddrOf: lval -> exp
809
(** Like mkAddrOf except if the type of lval is an array then it uses
810
StartOf. This is the right operation for getting a pointer to the start
811
of the storage denoted by lval. *)
812
val mkAddrOrStartOf: lval -> exp
814
(** Make a Mem, while optimizing AddrOf. The type of the addr must be
815
TPtr(t) and the type of the resulting lval is t. Note that in CIL the
816
implicit conversion between an array and the pointer to the first
817
element does not apply. You must do the conversion yourself using
819
val mkMem: addr:exp -> off:offset -> lval
821
(** Equivalent to [mkMem] for terms. *)
822
val mkTermMem: addr:term -> off:term_offset -> term_lval
824
(** Make an expression that is a string constant (of pointer type) *)
825
val mkString: string -> exp
827
(** Construct a cast when having the old type of the expression. If the new
828
* type is the same as the old type, then no cast is added. *)
829
val mkCastT: e:exp -> oldt:typ -> newt:typ -> exp
831
(** Like {!Cil.mkCastT} but uses typeOf to get [oldt] *)
832
val mkCast: e:exp -> newt:typ -> exp
834
(** Equivalent to [stripCasts] for terms. *)
835
val stripTermCasts: term -> term
837
(** Equivalent to [stripCasts] for tsets. *)
838
val stripTsetsCasts: tsets_elem -> tsets_elem
840
(** Removes casts from this expression, but ignores casts within
841
other expression constructs. So we delete the (A) and (B) casts from
842
"(A)(B)(x + (C)y)", but leave the (C) cast. *)
843
val stripCasts: exp -> exp
845
(** Removes info wrappers and return underlying expression *)
846
val stripInfo: exp -> exp
848
(** Removes casts and info wrappers and return underlying expression *)
849
val stripCastsAndInfo: exp -> exp
851
(** Removes casts and info wrappers,except last info wrapper, and return
852
underlying expression *)
853
val stripCastsButLastInfo: exp -> exp
855
(** Extracts term information in an expression information *)
856
val exp_info_of_term: term -> exp_info
858
(** Constructs a term from a term node and an expression information *)
859
val term_of_exp_info: term_node -> exp_info -> term
861
(** Map some function on underlying expression if Info or else on expression *)
862
val map_under_info: (exp -> exp) -> exp -> exp
864
(** Apply some function on underlying expression if Info or else on expression *)
865
val app_under_info: (exp -> unit) -> exp -> unit
867
(** Compute the type of an expression.
868
@plugin development guide *)
869
val typeOf: exp -> typ
871
val typeOf_pointed : typ -> typ
872
(** Returns the type pointed by the given type. Asserts it is a pointer
875
val is_fully_arithmetic: typ -> bool
876
(** Returns [true] whenever the type contains only arithmetic types *)
878
(** Convert a string representing a C integer literal to an expression.
879
* Handles the prefixes 0x and 0 and the suffixes L, U, UL, LL, ULL *)
880
val parseInt: string -> exp
883
(**********************************************)
884
(** {b Values for manipulating statements} *)
886
(** Construct a statement, given its kind. Initialize the [sid] field to -1
887
if [valid_sid] is false, or to a valid sid if [valid_sid] is true,
888
and [labels], [succs] and [preds] to the empty list *)
889
val mkStmt: ?valid_sid:bool -> stmtkind -> stmt
891
(* make the [new_stmtkind] changing the CFG relatively to [ref_stmt] *)
892
val mkStmtCfg: before:bool -> new_stmtkind:stmtkind -> ref_stmt:stmt -> stmt
894
(** Construct a block with no attributes, given a list of statements *)
895
val mkBlock: stmt list -> block
897
(** Construct a block with no attributes, given a list of statements and
898
wrap it into the Cfg. *)
899
val mkStmtCfgBlock: stmt list -> stmt
901
(** Construct a statement consisting of just one instruction *)
902
val mkStmtOneInstr: instr -> stmt
904
(** Try to compress statements so as to get maximal basic blocks.
905
* use this instead of List.@ because you get fewer basic blocks *)
906
(*val compactStmts: stmt list -> stmt list*)
908
(** Returns an empty statement (of kind [Instr]) *)
909
val mkEmptyStmt: ?loc:location -> unit -> stmt
911
(** A instr to serve as a placeholder *)
912
val dummyInstr: instr
914
(** A statement consisting of just [dummyInstr] *)
917
(** Make a while loop. Can contain Break or Continue *)
918
val mkWhile: guard:exp -> body:stmt list -> stmt list
920
(** Make a for loop for(i=start; i<past; i += incr) \{ ... \}. The body
921
can contain Break but not Continue. Can be used with i a pointer
922
or an integer. Start and done must have the same type but incr
923
must be an integer *)
924
val mkForIncr: iter:varinfo -> first:exp -> stopat:exp -> incr:exp
925
-> body:stmt list -> stmt list
927
(** Make a for loop for(start; guard; next) \{ ... \}. The body can
928
contain Break but not Continue !!! *)
929
val mkFor: start:stmt list -> guard:exp -> next: stmt list ->
930
body: stmt list -> stmt list
932
(** creates a block with empty attributes from an unspecified sequence. *)
933
val block_from_unspecified_sequence:
934
(stmt * lval list * lval list) list -> block
936
(**************************************************)
937
(** {b Values for manipulating attributes} *)
939
(** Various classes of attributes *)
940
type attributeClass =
942
(** Attribute of a name. If argument is true and we are on MSVC then
943
the attribute is printed using __declspec as part of the storage
945
| AttrFunType of bool
946
(** Attribute of a function type. If argument is true and we are on
947
MSVC then the attribute is printed just before the function name *)
948
| AttrType (** Attribute of a type *)
950
val registerAttribute: string -> attributeClass -> unit
951
(** Add a new attribute with a specified class *)
953
val removeAttribute: string -> unit
954
(** Remove an attribute previously registered. *)
956
val attributeClass: string -> attributeClass
957
(** Return the class of an attributes. *)
959
(** Partition the attributes into classes:name attributes, function type,
960
and type attributes *)
961
val partitionAttributes: default:attributeClass ->
962
attributes -> attribute list * (* AttrName *)
963
attribute list * (* AttrFunType *)
964
attribute list (* AttrType *)
966
(** Add an attribute. Maintains the attributes in sorted order of the second
968
val addAttribute: attribute -> attributes -> attributes
970
(** Add a list of attributes. Maintains the attributes in sorted order. The
971
second argument must be sorted, but not necessarily the first *)
972
val addAttributes: attribute list -> attributes -> attributes
974
(** Remove all attributes with the given name. Maintains the attributes in
976
val dropAttribute: string -> attributes -> attributes
978
(** Remove all attributes with names appearing in the string list.
979
* Maintains the attributes in sorted order *)
980
val dropAttributes: string list -> attributes -> attributes
982
(** Retains attributes with the given name *)
983
val filterAttributes: string -> attributes -> attributes
985
(** True if the named attribute appears in the attribute list. The list of
986
attributes must be sorted. *)
987
val hasAttribute: string -> attributes -> bool
989
(** returns the complete name for an attribute annotation. *)
990
val mkAttrAnnot: string -> string
992
(** Returns the name of an attribute. *)
993
val attributeName: attribute -> string
995
(** Returns the list of parameters associated to an attribute. The list is empty if there
996
is no such attribute or it has no parameters at all. *)
997
val findAttribute: string -> attribute list -> attrparam list
999
(** Returns all the attributes contained in a type. This requires a traversal
1000
of the type structure, in case of composite, enumeration and named types *)
1001
val typeAttrs: typ -> attribute list
1003
(** Returns the attributes of a type. *)
1004
val typeAttr: typ -> attribute list
1006
val setTypeAttrs: typ -> attributes -> typ (* Resets the attributes *)
1009
(** Add some attributes to a type *)
1010
val typeAddAttributes: attribute list -> typ -> typ
1012
(** Remove all attributes with the given names from a type. Note that this
1013
does not remove attributes from typedef and tag definitions, just from
1015
val typeRemoveAttributes: string list -> typ -> typ
1017
(** Convert an expression into an attrparam, if possible. Otherwise raise
1018
NotAnAttrParam with the offending subexpression *)
1019
val expToAttrParam: exp -> attrparam
1021
(** @return the list of field names leading to the wanted attributes *)
1022
val exists_attribute_deep: (attribute -> bool) -> typ -> string list option
1024
exception NotAnAttrParam of exp
1027
****************** VISITOR
1029
(** {b The visitor} *)
1031
(** Different visiting actions. 'a will be instantiated with [exp], [instr],
1033
@plugin development guide *)
1034
type 'a visitAction =
1035
SkipChildren (** Do not visit the children. Return
1036
the node as it is. *)
1037
| DoChildren (** Continue with the children of this
1038
node. Rebuild the node on return
1039
if any of the children changes
1041
| ChangeTo of 'a (** Replace the expression with the
1043
| ChangeToPost of 'a * ('a -> 'a)
1044
(** applies the expression to the function
1045
and gives back the result. Useful to insert some actions in
1046
an inheritance chain
1048
| ChangeDoChildrenPost of 'a * ('a -> 'a) (** First consider that the entire
1049
exp is replaced by the first
1050
parameter. Then continue with
1051
the children. On return rebuild
1052
the node if any of the children
1053
has changed and then apply the
1054
function on the node *)
1057
type visitor_behavior
1058
(** How the visitor should behave in front of mutable fields: in
1059
place modification or copy of the structure. This type is abstract.
1060
Use one of the two values below in your classes.
1061
@plugin development guide *)
1063
val inplace_visit: unit -> visitor_behavior
1064
(** In-place modification. Behavior of the original cil visitor.
1065
@plugin development guide *)
1067
val copy_visit: unit -> visitor_behavior
1068
(** Makes fresh copies of the mutable structures.
1069
- preserves sharing for varinfo.
1070
- makes fresh copy of varinfo only for declarations. Variables that are
1071
only used in the visited AST are thus still shared with the original
1072
AST. This allows for instance to copy a function with its
1073
formals and local variables, and to keep the references to other
1074
globals in the function's body.
1075
@plugin development guide *)
1077
(** true iff the behavior is a copy behavior. *)
1078
val is_copy_behavior: visitor_behavior -> bool
1080
val reset_behavior_varinfo: visitor_behavior -> unit
1081
(** resets the internal tables used by the given visitor_behavior.
1082
If you use fresh instances of visitor for each round of transformation,
1083
this should not be needed. In place modifications do not need that at all.
1085
val reset_behavior_compinfo: visitor_behavior -> unit
1086
val reset_behavior_enuminfo: visitor_behavior -> unit
1087
val reset_behavior_enumitem: visitor_behavior -> unit
1088
val reset_behavior_typeinfo: visitor_behavior -> unit
1089
val reset_behavior_stmt: visitor_behavior -> unit
1090
val reset_behavior_logic_info: visitor_behavior -> unit
1091
val reset_behavior_fieldinfo: visitor_behavior -> unit
1093
val get_varinfo: visitor_behavior -> varinfo -> varinfo
1094
(** retrieve the representative of a given varinfo in the current
1095
state of the visitor
1097
val get_compinfo: visitor_behavior -> compinfo -> compinfo
1098
val get_enuminfo: visitor_behavior -> enuminfo -> enuminfo
1099
val get_enumitem: visitor_behavior -> enumitem -> enumitem
1100
val get_typeinfo: visitor_behavior -> typeinfo -> typeinfo
1101
val get_stmt: visitor_behavior -> stmt -> stmt
1102
val get_logic_info: visitor_behavior -> logic_info -> logic_info
1103
val get_fieldinfo: visitor_behavior -> fieldinfo -> fieldinfo
1104
val get_logic_var: visitor_behavior -> logic_var -> logic_var
1106
val get_original_varinfo: visitor_behavior -> varinfo -> varinfo
1107
(** retrieve the original representative of a given copy of a varinfo
1108
in the current state of the visitor.
1110
val get_original_compinfo: visitor_behavior -> compinfo -> compinfo
1111
val get_original_enuminfo: visitor_behavior -> enuminfo -> enuminfo
1112
val get_original_enumitem: visitor_behavior -> enumitem -> enumitem
1113
val get_original_typeinfo: visitor_behavior -> typeinfo -> typeinfo
1114
val get_original_stmt: visitor_behavior -> stmt -> stmt
1115
val get_original_logic_info: visitor_behavior -> logic_info -> logic_info
1116
val get_original_fieldinfo: visitor_behavior -> fieldinfo -> fieldinfo
1117
val get_original_logic_var: visitor_behavior -> logic_var -> logic_var
1119
val set_varinfo: visitor_behavior -> varinfo -> varinfo -> unit
1120
(** change the representative of a given varinfo in the current
1121
state of the visitor. Use with care (i.e. makes sure that the old one
1122
is not referenced anywhere in the AST, or sharing will be lost.
1124
val set_compinfo: visitor_behavior -> compinfo -> compinfo -> unit
1125
val set_enuminfo: visitor_behavior -> enuminfo -> enuminfo -> unit
1126
val set_enumitem: visitor_behavior -> enumitem -> enumitem -> unit
1127
val set_typeinfo: visitor_behavior -> typeinfo -> typeinfo -> unit
1128
val set_stmt: visitor_behavior -> stmt -> stmt -> unit
1129
val set_logic_info: visitor_behavior -> logic_info -> logic_info -> unit
1130
val set_fieldinfo: visitor_behavior -> fieldinfo -> fieldinfo -> unit
1131
val set_logic_var: visitor_behavior -> logic_var -> logic_var -> unit
1133
val set_orig_varinfo: visitor_behavior -> varinfo -> varinfo -> unit
1134
(** change the reference of a given new varinfo in the current
1135
state of the visitor. Use with care
1137
val set_orig_compinfo: visitor_behavior -> compinfo -> compinfo -> unit
1138
val set_orig_enuminfo: visitor_behavior -> enuminfo -> enuminfo -> unit
1139
val set_orig_enumitem: visitor_behavior -> enumitem -> enumitem -> unit
1140
val set_orig_typeinfo: visitor_behavior -> typeinfo -> typeinfo -> unit
1141
val set_orig_stmt: visitor_behavior -> stmt -> stmt -> unit
1142
val set_orig_logic_info: visitor_behavior -> logic_info -> logic_info -> unit
1143
val set_orig_fieldinfo: visitor_behavior -> fieldinfo -> fieldinfo -> unit
1144
val set_orig_logic_var: visitor_behavior -> logic_var -> logic_var -> unit
1146
(** A visitor interface for traversing CIL trees. Create instantiations of
1147
* this type by specializing the class {!nopCilVisitor}. Each of the
1148
* specialized visiting functions can also call the [queueInstr] to specify
1149
* that some instructions should be inserted before the current instruction
1150
* or statement. Use syntax like [self#queueInstr] to call a method
1151
* associated with the current object.
1153
* {b Important Note for Frama-C Users:} Unless you really know what you are
1154
* doing, you should probably inherit from the
1155
* {!Visitor.generic_frama_c_visitor} instead of {!genericCilVisitor} or
1157
@plugin development guide *)
1158
class type cilVisitor = object
1159
method behavior: visitor_behavior
1160
(** the kind of behavior expected for the behavior *)
1162
method vfile: file -> file visitAction
1163
(** visit a whole file.
1164
@plugin development guide *)
1166
method vvdec: varinfo -> varinfo visitAction
1167
(** Invoked for each variable declaration. The subtrees to be traversed
1168
* are those corresponding to the type and attributes of the variable.
1169
* Note that variable declarations are all the [GVar], [GVarDecl], [GFun],
1170
* all the [varinfo] in formals of function types, and the formals and
1171
* locals for function definitions. This means that the list of formals
1172
* in a function definition will be traversed twice, once as part of the
1173
* function type and second as part of the formals in a function
1175
@plugin development guide *)
1177
method vvrbl: varinfo -> varinfo visitAction
1178
(** Invoked on each variable use. Here only the [SkipChildren] and
1179
* [ChangeTo] actions make sense since there are no subtrees. Note that
1180
* the type and attributes of the variable are not traversed for a
1182
@plugin development guide *)
1184
method vexpr: exp -> exp visitAction
1185
(** Invoked on each expression occurrence. The subtrees are the
1186
* subexpressions, the types (for a [Cast] or [SizeOf] expression) or the
1188
@plugin development guide *)
1190
method vlval: lval -> lval visitAction
1191
(** Invoked on each lvalue occurrence *)
1193
method voffs: offset -> offset visitAction
1194
(** Invoked on each offset occurrence that is *not* as part
1195
* of an initializer list specification, i.e. in an lval or
1196
* recursively inside an offset.
1197
@plugin development guide *)
1199
method vinitoffs: offset -> offset visitAction
1200
(** Invoked on each offset appearing in the list of a
1201
* CompoundInit initializer. *)
1203
method vinst: instr -> instr list visitAction
1204
(** Invoked on each instruction occurrence. The [ChangeTo] action can
1205
* replace this instruction with a list of instructions *)
1207
method vstmt: stmt -> stmt visitAction
1208
(** Control-flow statement. The default [DoChildren] action does not
1209
* create a new statement when the components change. Instead it updates
1210
* the contents of the original statement. This is done to preserve the
1211
* sharing with [Goto] and [Case] statements that point to the original
1212
* statement. If you use the [ChangeTo] action then you should take care
1213
* of preserving that sharing yourself.
1214
@plugin development guide *)
1216
method vblock: block -> block visitAction (** Block. *)
1217
method vfunc: fundec -> fundec visitAction (** Function definition.
1218
Replaced in place. *)
1219
method vglob: global -> global list visitAction
1220
(** Global (vars, types, etc.)
1221
@plugin development guide *)
1223
method vinit: varinfo -> offset -> init -> init visitAction
1224
(** Initializers for globals,
1225
* pass the global where this
1226
* occurs, and the offset *)
1227
method vtype: typ -> typ visitAction
1228
(** Use of some type. For typedef, struct, union and enum, the visit is
1229
done once at the global defining the type. Thus, children of
1230
[TComp], [TEnum] and [TNamed] are not visited again.
1233
method vcompinfo: compinfo -> compinfo visitAction
1234
(** declaration of a struct/union *)
1236
method venuminfo: enuminfo -> enuminfo visitAction
1237
(** declaration of an enumeration *)
1239
method vfieldinfo: fieldinfo -> fieldinfo visitAction
1240
(** visit the declaration of a field of a structure or union *)
1242
method venumitem: enumitem -> enumitem visitAction
1243
(** visit the declaration of an enumeration item *)
1245
method vattr: attribute -> attribute list visitAction
1246
(** Attribute. Each attribute can be replaced by a list *)
1247
method vattrparam: attrparam -> attrparam visitAction
1248
(** Attribute parameters. *)
1250
(** Add here instructions while visiting to queue them to preceede the
1251
* current statement or instruction being processed. Use this method only
1252
* when you are visiting an expression that is inside a function body, or
1253
* a statement, because otherwise there will no place for the visitor to
1254
* place your instructions. *)
1255
method queueInstr: instr list -> unit
1257
(** Gets the queue of instructions and resets the queue. This is done
1258
* automatically for you when you visit statments. *)
1259
method unqueueInstr: unit -> instr list
1261
method current_stmt: stmt option
1262
(** link to the current statement being visited.
1264
{b NB:} for copy visitor, the stmt is the original one (use
1265
[get_stmt] to obtain the corresponding copy)
1268
method push_stmt : stmt -> unit
1269
method pop_stmt : stmt -> unit
1271
method current_func: fundec option
1272
(** link to the current function being visited.
1274
{b NB:} for copy visitors, the fundec is the original one.
1276
method set_current_func: fundec -> unit
1277
method reset_current_func: unit -> unit
1279
method vlogic_type: logic_type -> logic_type visitAction
1281
method vtsets_elem: tsets_elem -> tsets_elem visitAction
1283
method vtsets_lval: tsets_lval -> tsets_lval visitAction
1285
method vtsets_lhost: tsets_lhost -> tsets_lhost visitAction
1287
method vtsets_offset: tsets_offset -> tsets_offset visitAction
1289
method vtsets: tsets -> tsets visitAction
1291
method vterm: term -> term visitAction
1293
method vterm_node: term_node -> term_node visitAction
1295
method vterm_lval: term_lval -> term_lval visitAction
1297
method vterm_lhost: term_lhost -> term_lhost visitAction
1299
method vterm_offset: term_offset -> term_offset visitAction
1301
method vlogic_info_decl: logic_info -> logic_info visitAction
1303
method vlogic_info_use: logic_info -> logic_info visitAction
1305
method vlogic_var_decl: logic_var -> logic_var visitAction
1307
method vlogic_var_use: logic_var -> logic_var visitAction
1309
method vquantifiers: quantifiers -> quantifiers visitAction
1311
method vpredicate: predicate -> predicate visitAction
1313
method vpredicate_named: predicate named -> predicate named visitAction
1316
method vpredicate_info_decl: predicate_info -> predicate_info visitAction
1320
method vpredicate_info_use: predicate_info -> predicate_info visitAction
1323
method vbehavior: funbehavior -> funbehavior visitAction
1325
method vspec: funspec -> funspec visitAction
1328
identified_tsets assigns -> identified_tsets assigns visitAction
1330
method vloop_pragma: term loop_pragma -> term loop_pragma visitAction
1332
method vslice_pragma: term slice_pragma -> term slice_pragma visitAction
1333
method vimpact_pragma: term impact_pragma -> term impact_pragma visitAction
1336
identified_tsets zone -> identified_tsets zone visitAction
1338
method vcode_annot: code_annotation -> code_annotation visitAction
1340
method vannotation: global_annotation -> global_annotation visitAction
1342
(** fill the global environment tables at the end of a full copy in a
1344
@plugin development guide *)
1345
method fill_global_tables: unit
1347
(** get the queue of actions to be performed at the end of a full copy.
1348
@plugin development guide *)
1349
method get_filling_actions: (unit -> unit) Queue.t
1351
(** Used at the beginning of the visit of a whole file to update
1352
global logic tables with copied informations when needed.
1354
method set_logic_tables: unit -> unit
1358
(** generic visitor, parameterized by its copying behavior.
1359
Traverses the CIL tree without modifying anything *)
1360
class genericCilVisitor: ?prj:(Project.t) -> visitor_behavior -> cilVisitor
1362
(** Default in place visitor doing nothing and operating on current project. *)
1363
class nopCilVisitor: cilVisitor
1365
(** [doVisit vis deepCopyVisitor copy action children node] visits a [node]
1366
(or its copy according to the result of [copy]) and if needed
1367
its [children]. {b Do not use it if you don't understand Cil visitor
1369
@param vis the visitor performing the needed transformations. The open
1370
type allows for extensions to Cil to be visited by the same mechanisms.
1371
@param deepCopyVisitor a generator for a visitor of the same type
1372
of the current one that performs a deep copy of the AST.
1373
Needed when the visitAction is [SkipChildren] or [ChangeTo] and [vis]
1374
is a copy visitor (we need to finish the copy anyway)
1375
@param copy function that may return a copy of the actual node.
1376
@param action the visiting function for the current node
1377
@param children what to do on the children of the current node
1378
@param node the current node
1383
('a -> 'a visitAction) ->
1384
('visit -> 'a -> 'a) -> 'a -> 'a
1386
(** same as above, but can return a list of nodes *)
1390
('a -> 'a list visitAction) ->
1391
('visit -> 'a -> 'a) -> 'a -> 'a list
1393
(* other cil constructs *)
1395
(** Visit a file. This will will re-cons all globals TWICE (so that it is
1396
* tail-recursive). Use {!Cil.visitCilFileSameGlobals} if your visitor will
1397
* not change the list of globals.
1398
@plugin development guide *)
1399
val visitCilFileCopy: cilVisitor -> file -> file
1401
(** Same thing, but the result is ignored. The given visitor must thus be
1402
an inplace visitor. Nothing is done if the visitor is a copy visitor.
1403
@plugin development guide *)
1404
val visitCilFile: cilVisitor -> file -> unit
1406
(** A visitor for the whole file that does not change the globals (but maybe
1407
* changes things inside the globals). Use this function instead of
1408
* {!Cil.visitCilFile} whenever appropriate because it is more efficient for
1410
@plugin development guide *)
1411
val visitCilFileSameGlobals: cilVisitor -> file -> unit
1413
(** Visit a global *)
1414
val visitCilGlobal: cilVisitor -> global -> global list
1416
(** Visit a function definition *)
1417
val visitCilFunction: cilVisitor -> fundec -> fundec
1419
(* Visit an expression *)
1420
val visitCilExpr: cilVisitor -> exp -> exp
1422
(** Visit an lvalue *)
1423
val visitCilLval: cilVisitor -> lval -> lval
1425
(** Visit an lvalue or recursive offset *)
1426
val visitCilOffset: cilVisitor -> offset -> offset
1428
(** Visit an initializer offset *)
1429
val visitCilInitOffset: cilVisitor -> offset -> offset
1431
(** Visit an instruction *)
1432
val visitCilInstr: cilVisitor -> instr -> instr list
1434
(** Visit a statement *)
1435
val visitCilStmt: cilVisitor -> stmt -> stmt
1437
(** Visit a block *)
1438
val visitCilBlock: cilVisitor -> block -> block
1441
val visitCilType: cilVisitor -> typ -> typ
1443
(** Visit a variable declaration *)
1444
val visitCilVarDecl: cilVisitor -> varinfo -> varinfo
1446
(** Visit an initializer, pass also the global to which this belongs and the
1448
val visitCilInit: cilVisitor -> varinfo -> offset -> init -> init
1450
(** Visit a list of attributes *)
1451
val visitCilAttributes: cilVisitor -> attribute list -> attribute list
1453
val visitCilAnnotation: cilVisitor -> global_annotation -> global_annotation
1455
val visitCilCodeAnnotation: cilVisitor -> code_annotation -> code_annotation
1457
val visitCilAssigns:
1458
cilVisitor -> identified_tsets assigns -> identified_tsets assigns
1460
val visitCilFunspec: cilVisitor -> funspec -> funspec
1462
val visitCilBehavior: cilVisitor -> funbehavior -> funbehavior
1463
val visitCilBehaviors: cilVisitor -> funbehavior list -> funbehavior list
1465
val visitCilLogicType: cilVisitor -> logic_type -> logic_type
1467
val visitCilPredicate: cilVisitor -> predicate -> predicate
1469
val visitCilPredicateNamed: cilVisitor -> predicate named -> predicate named
1471
val visitCilTsets: cilVisitor -> tsets -> tsets
1473
val visitCilTsetsElem: cilVisitor -> tsets_elem -> tsets_elem
1475
val visitCilTsetsOffset: cilVisitor -> tsets_offset -> tsets_offset
1477
val visitCilTerm: cilVisitor -> term -> term
1479
val visitCilTermOffset: cilVisitor -> term_offset -> term_offset
1482
val visitCilPredicateInfo: cilVisitor -> predicate_info -> predicate_info
1485
val visitCilLogicInfo: cilVisitor -> logic_info -> logic_info
1487
(* And some generic visitors. The above are built with these *)
1490
(** {b Utility functions} *)
1492
val is_skip: stmtkind -> bool
1494
(** A visitor that does constant folding. Pass as argument whether you want
1495
* machine specific simplifications to be done, or not. *)
1496
val constFoldVisitor: bool -> cilVisitor
1498
(** Return the string 's' if we're printing output for gcc, suppres
1499
* it if we're printing for CIL to parse back in. the purpose is to
1500
* hide things from gcc that it complains about, but still be able
1501
* to do lossless transformations when CIL is the consumer *)
1502
val forgcc: string -> string
1504
(** {b Debugging support} *)
1506
(** A reference to the current location. If you are careful to set this to
1507
* the current location then you can use some built-in logging functions that
1508
* will print the location. *)
1509
module CurrentLoc: Computation.REF_OUTPUT with type data = location
1511
(** A reference to the current global being visited *)
1512
val currentGlobal: global ref
1515
(** CIL has a fairly easy to use mechanism for printing error messages. This
1516
* mechanism is built on top of the pretty-printer mechanism (see
1517
* {!Pretty.doc}) and the error-message modules (see {!Errormsg.error}).
1519
Here is a typical example for printing a log message: {v
1520
ignore (Errormsg.log "Expression %a is not positive (at %s:%i)\n"
1521
d_exp e loc.file loc.line)
1524
and here is an example of how you print a fatal error message that stop the
1526
Errormsg.s (Errormsg.bug "Why am I here?")
1529
Notice that you can use C format strings with some extension. The most
1530
useful extension is "%a" that means to consumer the next two argument from
1531
the argument list and to apply the first to [unit] and then to the second
1532
and to print the resulting {!Pretty.doc}. For each major type in CIL there is
1533
a corresponding function that pretty-prints an element of that type:
1537
(** Pretty-print a location *)
1538
val d_loc: Format.formatter -> location -> unit
1540
(** Pretty-print the [(Cil.CurrentLoc.get ())] *)
1541
val d_thisloc: Format.formatter -> unit
1543
(** Pretty-print an integer of a given kind *)
1544
val d_ikind: Format.formatter -> ikind -> unit
1546
(** Pretty-print a floating-point kind *)
1547
val d_fkind: Format.formatter -> fkind -> unit
1549
(** Pretty-print storage-class information *)
1550
val d_storage: Format.formatter -> storage -> unit
1552
(** Pretty-print a constant *)
1553
val d_const: Format.formatter -> constant -> unit
1555
(** returns a dummy specification *)
1556
val empty_funspec : unit -> funspec
1558
(** returns true if the given spec is empty. *)
1559
val is_empty_funspec: funspec -> bool
1561
val derefStarLevel: int
1564
val addrOfLevel: int
1565
val additiveLevel: int
1566
val comparativeLevel: int
1567
val bitwiseLevel: int
1569
(** Parentheses level. An expression "a op b" is printed parenthesized if its
1570
* parentheses level is >= that that of its context. Identifiers have the
1571
* lowest level and weakly binding operators (e.g. |) have the largest level.
1572
* The correctness criterion is that a smaller level MUST correspond to a
1573
* stronger precedence!
1575
val getParenthLevel: exp -> int
1577
val getParenthLevelLogic:term_node -> int
1579
(** A printer interface for CIL trees. Create instantiations of
1580
* this type by specializing the class {!defaultCilPrinterClass}. *)
1581
(** A printer interface for CIL trees. Create instantiations of
1582
* this type by specializing the class {!Cil.defaultCilPrinter}. *)
1583
class type cilPrinter = object
1585
(** Local logical annotation (function specifications and code annotations
1586
are printed only if [logic_printer_enabled] is set to true
1588
val mutable logic_printer_enabled : bool
1590
(** more info is displayed when on verbose mode. *)
1591
val mutable verbose: bool
1593
method current_function: varinfo option
1594
(** Returns the [varinfo] corresponding to the function being printed *)
1596
method current_stmt: stmt option
1597
(** Returns the stmt being printed *)
1599
method may_be_skipped: stmt -> bool
1600
(** This is called to check that a given statement may be
1601
compacted with another one.
1602
For example this is called whenever a [while(1)] followed by a conditional
1603
[if (cond) break;] may be compacted into [while(cond)]. *)
1606
method setPrintInstrTerminator : string -> unit
1607
method getPrintInstrTerminator : unit -> string
1609
method pVarName: Format.formatter -> string -> unit
1610
(** Invoked each time an identifier name is to be printed. Allows for
1611
various manipulation of the name, such as unmangling. *)
1613
method pVDecl: Format.formatter -> varinfo -> unit
1614
(** Invoked for each variable declaration. Note that variable
1615
* declarations are all the [GVar], [GVarDecl], [GFun], all the [varinfo]
1616
* in formals of function types, and the formals and locals for function
1619
method pVar: Format.formatter -> varinfo -> unit
1620
(** Invoked on each variable use. *)
1622
method pLval: Format.formatter -> lval -> unit
1623
(** Invoked on each lvalue occurence *)
1625
method pOffset: Format.formatter -> offset -> unit
1626
(** Invoked on each offset occurence. The second argument is the base. *)
1628
method pInstr: Format.formatter -> instr -> unit
1629
(** Invoked on each instruction occurrence. *)
1631
method pStmt: Format.formatter -> stmt -> unit
1632
(** Control-flow statement. *)
1634
method pStmtNext : stmt -> Format.formatter -> stmt -> unit
1636
method pBlock: ?toplevel:bool -> Format.formatter -> block -> unit
1637
(** Print a block. *)
1639
method pGlobal: Format.formatter -> global -> unit
1640
(** Global (vars, types, etc.). This can be slow. *)
1642
method pFieldDecl: Format.formatter -> fieldinfo -> unit
1643
(** A field declaration *)
1645
method pType: (Format.formatter -> unit) option -> Format.formatter -> typ -> unit
1646
(* Use of some type in some declaration. The first argument is used to print
1647
* the declared element, or is None if we are just printing a type with no
1648
* name being declared. Note that for structure/union and enumeration types
1649
* the definition of the composite type is not visited. Use [vglob] to
1652
method pAttr: Format.formatter -> attribute -> bool
1653
(** Attribute. Also return an indication whether this attribute must be
1654
* printed inside the __attribute__ list or not. *)
1656
method pAttrParam: Format.formatter -> attrparam -> unit
1657
(** Attribute paramter *)
1659
method pAttrs: Format.formatter -> attributes -> unit
1660
(** Attribute lists *)
1662
method pLabel: Format.formatter -> label -> unit
1665
method pLineDirective: ?forcefile:bool -> Format.formatter -> location -> unit
1666
(** Print a line-number. This is assumed to come always on an empty line.
1667
* If the forcefile argument is present and is true then the file name
1668
* will be printed always. Otherwise the file name is printed only if it
1669
* is different from the last time time this function is called. The last
1670
* file name is stored in a private field inside the cilPrinter object. *)
1672
method pAnnotatedStmt : stmt -> Format.formatter -> stmt -> unit
1673
(** Print an annotated statement. The code to be printed is given in the
1674
* last {!Cil_types.stmt} argument. The initial {!Cil_types.stmt} argument
1675
* records the statement which follows the one being printed;
1676
* {!defaultCilPrinterClass} uses this information to prettify
1677
* statement printing in certain special cases. *)
1679
method pStmtKind : stmt -> Format.formatter -> stmtkind -> unit
1680
(** Print a statement kind. The code to be printed is given in the
1681
* {!Cil_types.stmtkind} argument. The initial {!Cil_types.stmt} argument
1682
* records the statement which follows the one being printed;
1683
* {!defaultCilPrinterClass} uses this information to prettify
1684
* statement printing in certain special cases.
1685
* The boolean flag indicated whether the statement has labels
1686
* (which have already been printed)
1689
method pExp: Format.formatter -> exp -> unit
1690
(** Print expressions *)
1692
method pInit: Format.formatter -> init -> unit
1693
(** Print initializers. This can be slow. *)
1695
(** Pretty-printing of annotations. *)
1697
method pLogic_type: Format.formatter -> logic_type -> unit
1699
method pTsets_elem: Format.formatter -> tsets_elem -> unit
1701
method pTsets_lval: Format.formatter -> tsets_lval -> unit
1703
method pTsets_lhost: Format.formatter -> tsets_lhost -> unit
1705
method pTsets_offset: Format.formatter -> tsets_offset -> unit
1707
method pTsets: Format.formatter -> tsets -> unit
1709
method pTerm: Format.formatter -> term -> unit
1711
method pTerm_node: Format.formatter -> term -> unit
1713
method pTerm_lval: Format.formatter -> term_lval -> unit
1715
method pTerm_offset: Format.formatter -> term_offset -> unit
1717
method pLogic_info_use: Format.formatter -> logic_info -> unit
1719
method pLogic_var: Format.formatter -> logic_var -> unit
1721
method pQuantifiers: Format.formatter -> quantifiers -> unit
1723
method pPredicate: Format.formatter -> predicate -> unit
1725
method pPredicate_named: Format.formatter -> predicate named -> unit
1728
method pPredicate_info_use: Format.formatter -> predicate_info -> unit
1731
method pBehavior: Format.formatter -> funbehavior -> unit
1733
method pSpec: Format.formatter -> funspec -> unit
1735
method pZone: Format.formatter -> identified_tsets zone -> unit
1737
(** pAssigns is parameterized by its introducing keyword
1738
(i.e. loop_assigns or assigns)
1741
string -> Format.formatter -> identified_tsets assigns -> unit
1743
method pStatus : Format.formatter -> Cil_types.annot_status -> unit
1745
method pCode_annot: Format.formatter -> code_annotation -> unit
1747
method pAnnotation: Format.formatter -> global_annotation -> unit
1750
class defaultCilPrinterClass: cilPrinter
1751
val defaultCilPrinter: cilPrinter
1753
class type descriptiveCilPrinter = object
1756
method startTemps: unit -> unit
1757
method stopTemps: unit -> unit
1758
method pTemps: Format.formatter -> unit
1761
class descriptiveCilPrinterClass : descriptiveCilPrinter
1762
(** Like defaultCilPrinterClass, but instead of temporary variable
1763
names it prints the description that was provided when the temp was
1764
created. This is usually better for messages that are printed for end
1765
users, although you may want the temporary names for debugging. *)
1766
val descriptiveCilPrinter: descriptiveCilPrinter
1769
(* Top-level printing functions *)
1770
(** Print a type given a pretty printer *)
1771
val printType: cilPrinter -> Format.formatter -> typ -> unit
1773
(** Print an expression given a pretty printer *)
1774
val printExp: cilPrinter -> Format.formatter -> exp -> unit
1776
(** Print an lvalue given a pretty printer *)
1777
val printLval: cilPrinter -> Format.formatter -> lval -> unit
1779
(** Print a global given a pretty printer *)
1780
val printGlobal: cilPrinter -> Format.formatter -> global -> unit
1782
(** Print an attribute given a pretty printer *)
1783
val printAttr: cilPrinter -> Format.formatter -> attribute -> unit
1785
(** Print a set of attributes given a pretty printer *)
1786
val printAttrs: cilPrinter -> Format.formatter -> attributes -> unit
1788
(** Print an instruction given a pretty printer *)
1789
val printInstr: cilPrinter -> Format.formatter -> instr -> unit
1791
(** Print a statement given a pretty printer. This can take very long
1792
* (or even overflow the stack) for huge statements. *)
1793
val printStmt: cilPrinter -> Format.formatter -> stmt -> unit
1795
(** Print a block given a pretty printer. This can take very long
1796
* (or even overflow the stack) for huge block. *)
1797
val printBlock: cilPrinter -> Format.formatter -> block -> unit
1799
(** Print an initializer given a pretty printer. This can take very long
1800
* (or even overflow the stack) for huge initializers. *)
1801
val printInit: cilPrinter -> Format.formatter -> init -> unit
1803
val printTerm_lval: cilPrinter -> Format.formatter -> term_lval -> unit
1804
val printLogic_var: cilPrinter -> Format.formatter -> logic_var -> unit
1805
val printLogic_type: cilPrinter -> Format.formatter -> logic_type -> unit
1806
val printTerm: cilPrinter -> Format.formatter -> term -> unit
1807
val printTerm_offset: cilPrinter -> Format.formatter -> term_offset -> unit
1808
val printPredicate_named:
1809
cilPrinter -> Format.formatter -> predicate named -> unit
1810
val printCode_annotation:
1811
cilPrinter -> Format.formatter -> code_annotation -> unit
1812
val printFunspec: cilPrinter -> Format.formatter -> funspec -> unit
1813
val printAnnotation: cilPrinter -> Format.formatter -> global_annotation -> unit
1815
(** Pretty-print a type using {!Cil.defaultCilPrinter} *)
1816
val d_type: Format.formatter -> typ -> unit
1818
(** Pretty-print an expression using {!Cil.defaultCilPrinter} *)
1819
val d_exp: Format.formatter -> exp -> unit
1821
(** Pretty-print an lvalue using {!Cil.defaultCilPrinter} *)
1822
val d_lval: Format.formatter -> lval -> unit
1824
(** Pretty-print an offset using {!Cil.defaultCilPrinter}, given the pretty
1825
* printing for the base. *)
1826
val d_offset: Format.formatter -> offset -> unit
1828
(** Pretty-print an initializer using {!Cil.defaultCilPrinter}. This can be
1829
* extremely slow (or even overflow the stack) for huge initializers. *)
1830
val d_init: Format.formatter -> init -> unit
1832
(** Pretty-print a binary operator *)
1833
val d_binop: Format.formatter -> binop -> unit
1835
(** Pretty-print a unary operator *)
1836
val d_unop: Format.formatter -> unop -> unit
1838
(** Pretty-print an attribute using {!Cil.defaultCilPrinter} *)
1839
val d_attr: Format.formatter -> attribute -> unit
1841
(** Pretty-print an argument of an attribute using {!Cil.defaultCilPrinter} *)
1842
val d_attrparam: Format.formatter -> attrparam -> unit
1844
(** Pretty-print a list of attributes using {!Cil.defaultCilPrinter} *)
1845
val d_attrlist: Format.formatter -> attributes -> unit
1847
(** Pretty-print an instruction using {!Cil.defaultCilPrinter} *)
1848
val d_instr: Format.formatter -> instr -> unit
1850
(** Pretty-print a label using {!Cil.defaultCilPrinter} *)
1851
val d_label: Format.formatter -> label -> unit
1853
(** Pretty-print a statement using {!Cil.defaultCilPrinter}. This can be
1854
* extremely slow (or even overflow the stack) for huge statements. *)
1855
val d_stmt: Format.formatter -> stmt -> unit
1857
(** Pretty-print a block using {!Cil.defaultCilPrinter}. This can be
1858
* extremely slow (or even overflow the stack) for huge blocks. *)
1859
val d_block: Format.formatter -> block -> unit
1861
(** Pretty-print the internal representation of a global using
1862
* {!Cil.defaultCilPrinter}. This can be extremely slow (or even overflow the
1863
* stack) for huge globals (such as arrays with lots of initializers). *)
1864
val d_global: Format.formatter -> global -> unit
1866
val d_term_lval: Format.formatter -> term_lval -> unit
1867
val d_logic_var: Format.formatter -> logic_var -> unit
1868
val d_logic_type: Format.formatter -> logic_type -> unit
1869
val d_term: Format.formatter -> term -> unit
1870
val d_term_offset: Format.formatter -> term_offset -> unit
1871
val d_tsets_lval: Format.formatter -> tsets_lval -> unit
1872
val d_tsets: Format.formatter -> tsets -> unit
1873
val d_tsets_elem: Format.formatter -> tsets_elem -> unit
1874
val d_tsets_lhost: Format.formatter -> tsets_lhost -> unit
1875
val d_tsets_offset: Format.formatter -> tsets_offset -> unit
1877
val d_status: Format.formatter -> annot_status -> unit
1878
val d_predicate_named: Format.formatter -> predicate named -> unit
1879
val d_code_annotation: Format.formatter -> code_annotation -> unit
1880
val d_funspec: Format.formatter -> funspec -> unit
1881
val d_annotation: Format.formatter -> global_annotation -> unit
1883
(** Versions of the above pretty printers, that don't print #line directives *)
1884
val dn_exp : Format.formatter -> exp -> unit
1885
val dn_lval : Format.formatter -> lval -> unit
1886
(* dn_offset is missing because it has a different interface *)
1887
val dn_init : Format.formatter -> init -> unit
1888
val dn_type : Format.formatter -> typ -> unit
1889
val dn_global : Format.formatter -> global -> unit
1890
val dn_attrlist : Format.formatter -> attributes -> unit
1891
val dn_attr : Format.formatter -> attribute -> unit
1892
val dn_attrparam : Format.formatter -> attrparam -> unit
1893
val dn_stmt : Format.formatter -> stmt -> unit
1894
val dn_instr : Format.formatter -> instr -> unit
1897
(** Pretty-print an entire file. Here you give the channel where the printout
1898
* should be sent. *)
1899
val dumpFile: cilPrinter -> out_channel -> string -> file -> unit
1900
val d_file: cilPrinter -> Format.formatter -> file -> unit
1903
(** the following error message producing functions also print a location in
1904
* the code. use {!Errormsg.bug} and {!Errormsg.unimp} if you do not want
1907
(** Like {!Errormsg.bug} except that [(Cil.CurrentLoc.get ())] is also printed *)
1908
val bug: ('a, Format.formatter, unit, 'b) format4 -> 'a
1910
(** Raises [Errormsg.Error] after printing *)
1911
val fatal_unimp: ('a, Format.formatter, unit, 'b) format4 -> 'a
1912
val fatal_error: ('a, Format.formatter, unit, 'b) format4 -> 'a
1914
(** Like {!Errormsg.unimp} except that [(Cil.CurrentLoc.get ())]is also printed *)
1915
val unimp: ('a, Format.formatter, unit, unit) format4 -> 'a
1917
(** Like {!Errormsg.error} except that this full location is given
1918
[(file, line, byte_start_on_line, byte_stop_on_line)] *)
1919
val error_loc: string*int*int*int -> ('a, Format.formatter, unit, unit) format4 -> 'a
1921
(** Like {!Errormsg.error} except that [(Cil.CurrentLoc.get ())] is also printed *)
1922
val error: ('a, Format.formatter, unit, unit) format4 -> 'a
1924
(** Like {!Cil.error} except that it explicitly takes a location argument,
1925
* instead of using the [(Cil.CurrentLoc.get ())] *)
1926
val errorLoc: location -> ('a, Format.formatter, unit, unit) format4 -> 'a
1928
(** Like {!Errormsg.warn} except that [(Cil.CurrentLoc.get ())] is also printed *)
1929
val warn: ('a, Format.formatter, unit, unit) format4 -> 'a
1931
(** Like {!Errormsg.warnOpt} except that [(Cil.CurrentLoc.get ())] is also printed.
1932
* This warning is printed only of {!Errormsg.warnFlag} is set. *)
1933
val warnOpt: ('a, Format.formatter, unit, unit) format4 -> 'a
1935
(** Like {!Errormsg.warn} except that [(Cil.CurrentLoc.get ())] and context
1937
val warnContext: ('a, Format.formatter, unit, unit) format4 -> 'a
1939
(** Like {!Errormsg.warn} except that [(Cil.CurrentLoc.get ())] and context is also
1940
* printed. This warning is printed only of {!Errormsg.warnFlag} is set. *)
1941
val warnContextOpt: ('a, Format.formatter, unit, unit) format4 -> 'a
1943
(** Like {!Cil.warn} except that it explicitly takes a location argument,
1944
* instead of using the [(Cil.CurrentLoc.get ())] *)
1945
val warnLoc: location -> ('a, Format.formatter, unit, unit) format4 -> 'a
1947
val log: ('a, Format.formatter, unit, unit) format4 -> 'a
1949
val logLoc: location -> ('a, Format.formatter, unit, unit) format4 -> 'a
1952
sep:((Format.formatter -> 'a list -> unit) -> 'a list -> unit,
1953
Format.formatter, unit,
1954
(Format.formatter -> 'b -> unit) -> 'b -> unit) format4 ->
1955
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
1957
val fprintf_to_string : ('a, Format.formatter, unit, string) format4 -> 'a
1958
(** Sometimes you do not want to see the syntactic sugar that the above
1959
* pretty-printing functions add. In that case you can use the following
1960
* pretty-printing functions. But note that the output of these functions is
1963
(** Sometimes you do not want to see the syntactic sugar that the above
1964
* pretty-printing functions add. In that case you can use the following
1965
* pretty-printing functions. But note that the output of these functions is
1968
(** Pretty-print the internal representation of an expression *)
1969
val d_plainexp: Format.formatter -> exp -> unit
1971
(** Pretty-print the internal representation of an integer *)
1972
val d_plaininit: Format.formatter -> init -> unit
1974
(** Pretty-print the internal representation of an lvalue *)
1975
val d_plainlval: Format.formatter -> lval -> unit
1977
(** Pretty-print the internal representation of an lvalue offset
1978
val d_plainoffset: Format.formatter -> offset -> Pretty.doc *)
1980
(** Pretty-print the internal representation of a type *)
1981
val d_plaintype: Format.formatter -> typ -> unit
1983
(** Pretty-print an expression while printing descriptions rather than names
1985
val dd_exp: Format.formatter -> exp -> unit
1987
(** Pretty-print an lvalue on the left side of an assignment.
1988
If there is an offset or memory dereference, temporaries will
1989
be replaced by descriptions as in dd_exp. If the lval is a temp var,
1990
that var will not be replaced by a description; use "dd_exp () (Lval lv)"
1991
if that's what you want. *)
1992
val dd_lval: Format.formatter -> lval -> unit
1994
(** {b ALPHA conversion} has been moved to the Alpha module. *)
1997
(** Assign unique names to local variables. This might be necessary after you
1998
* transformed the code and added or renamed some new variables. Names are
1999
* not used by CIL internally, but once you print the file out the compiler
2000
* downstream might be confused. You might
2001
* have added a new global that happens to have the same name as a local in
2002
* some function. Rename the local to ensure that there would never be
2003
* confusioin. Or, viceversa, you might have added a local with a name that
2004
* conflicts with a global *)
2005
val uniqueVarNames: file -> unit
2007
(** {b Optimization Passes} *)
2009
(** A peephole optimizer that processes two adjacent statements and possibly
2010
replaces them both. If some replacement happens, then the new statements
2011
are themselves subject to optimization. Each statement is the list
2012
is optimized independently. *)
2013
val peepHole2: (stmt * stmt -> stmt list option) -> stmt list -> stmt list
2015
(** Similar to [peepHole2] except that the optimization window consists of
2016
one statement, not two *)
2017
val peepHole1: (instr -> instr list option) -> stmt list -> unit
2019
(** {b Machine dependency} *)
2022
(** Raised when one of the bitsSizeOf functions cannot compute the size of a
2023
* type. This can happen because the type contains array-length expressions
2024
* that we don't know how to compute or because it is a type whose size is
2025
* not defined (e.g. TFun or an undefined compinfo). The string is an
2026
* explanation of the error *)
2027
exception SizeOfError of string * typ
2029
(** The size of a type, in bits. Trailing padding is added for structs and
2030
* arrays. Raises {!Cil.SizeOfError} when it cannot compute the size. This
2031
* function is architecture dependent, so you should only call this after you
2032
* call {!Cil.initCIL}. Remember that on GCC sizeof(void) is 1! *)
2033
val bitsSizeOf: typ -> int
2035
val truncateInteger64: ikind -> int64 -> int64 * bool
2037
(** The size of a type, in bytes. Returns a constant expression or a "sizeof"
2038
* expression if it cannot compute the size. This function is architecture
2039
* dependent, so you should only call this after you call {!Cil.initCIL}. *)
2040
val sizeOf: typ -> exp
2042
(** The size of a type, in bytes. Raises {!Cil.SizeOfError} when it cannot
2043
compute the size. *)
2044
val sizeOf_int: typ -> int
2046
(** The minimum alignment (in bytes) for a type. This function is
2047
* architecture dependent, so you should only call this after you call
2048
* {!Cil.initCIL}. *)
2049
val alignOf_int: typ -> int
2051
(** Give a type of a base and an offset, returns the number of bits from the
2052
* base address and the width (also expressed in bits) for the subobject
2053
* denoted by the offset. Raises {!Cil.SizeOfError} when it cannot compute
2054
* the size. This function is architecture dependent, so you should only call
2055
* this after you call {!Cil.initCIL}. *)
2056
val bitsOffset: typ -> offset -> int * int
2058
(** Generate an {!Cil_types.exp} to be used in case of errors. *)
2059
val dExp:string -> exp
2061
(** Generate an {!Cil_types.instr} to be used in case of errors. *)
2062
val dInstr: string -> location -> instr
2064
(** Generate a {!Cil_types.global} to be used in case of errors. *)
2065
val dGlobal: string -> location -> global
2067
(** Like map but try not to make a copy of the list *)
2068
val mapNoCopy: ('a -> 'a) -> 'a list -> 'a list
2070
(** Like map but each call can return a list. Try not to make a copy of the
2072
val mapNoCopyList: ('a -> 'a list) -> 'a list -> 'a list
2074
(** sm: return true if the first is a prefix of the second string *)
2075
val startsWith: string -> string -> bool
2078
(** {b An Interpreter for constructing CIL constructs} *)
2080
(** The type of argument for the interpreter *)
2083
| Feo of exp option (** For array lengths *)
2087
| FE of exp list (** For arguments in a function call *)
2088
| Ff of (string * typ * attributes) (** For a formal argument *)
2089
| FF of (string * typ * attributes) list (** For formal argument lists *)
2090
| Fva of bool (** For the ellipsis in a function type *)
2093
| Flo of lval option
2108
| FP of attrparam list
2112
val d_formatarg : Format.formatter -> formatArg -> unit
2114
val stmt_of_instr_list : ?loc:location -> instr list -> stmtkind
2116
val pretty_loc : Format.formatter -> kinstr -> unit
2117
val pretty_loc_simply : Format.formatter -> kinstr -> unit
2120
(** Convert a C variable into the corresponding logic variable.
2121
The returned logic variable is unique for a given C variable.
2123
val cvar_to_lvar : varinfo -> logic_var
2125
(** Create a fresh logical variable giving its name and type. *)
2126
val make_logic_var : string -> logic_type -> logic_var
2128
(** Make a temporary variable to use in annotations *)
2129
val make_temp_logic_var: logic_type -> logic_var
2131
(** The constant logic term zero.
2132
@plugin development guide *)
2133
val lzero : ?loc:location -> unit -> term
2135
(** The given constant logic term *)
2136
val lconstant : ?loc:location -> Int64.t -> term
2138
(** Bind all free variables with an universal quantifier *)
2139
val close_predicate : predicate named -> predicate named
2141
(** extract [varinfo] elements from an [exp] *)
2142
val extract_varinfos_from_exp : exp -> Cilutil.VarinfoSet.t
2144
(** extract [varinfo] elements from an [lval] *)
2145
val extract_varinfos_from_lval : lval -> Cilutil.VarinfoSet.t
2147
(** extract [logic_var] elements from a [term] *)
2148
val extract_free_logicvars_from_term : term -> Cilutil.LogicVarSet.t
2150
(** extract [logic_var] elements from a [predicate] *)
2151
val extract_free_logicvars_from_predicate :
2152
predicate named -> Cilutil.LogicVarSet.t
2154
(** creates a visitor that will replace in place uses of var in the first
2155
list by their counterpart in the second list.
2156
@raise Invalid_argument if the lists have different lengths.
2158
val create_alpha_renaming: varinfo list -> varinfo list -> cilVisitor
2160
val print_utf8 : bool ref
2164
compile-command: "make -C ../.."
added
removed
cil/src/cil.mli
