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
(**************************************************************************)
41
(** The Abstract Syntax of CIL.
42
@plugin development guide *)
44
(**************************** WARNING ***************************************)
45
(* Remember to reflect any change here into the visitor and pretty-printer *)
46
(* in cil.ml. In particular, if a type becomes mutable, it is necessary to *)
47
(* adapt the Cil.behavior type and the copy_behavior accordingly. *)
48
(* A first test to see if something has been broken by a change is to launch*)
49
(* ptests.byte -add-options '-files-debug "-check -copy"' *)
50
(* In addition, it is a good idea to add some invariant checks in the *)
51
(* check_file class in frama-c/src/file.ml (before lauching the tests) *)
52
(****************************************************************************)
54
(** The top-level representation of a CIL source file (and the result of the
55
* parsing and elaboration). Its main contents is the list of global
56
* declarations and definitions. You can iterate over the globals in a
57
* {!Cil_types.file} using the following iterators: {!Cil.mapGlobals},
58
* {!Cil.iterGlobals} and {!Cil.foldGlobals}. You can also use the
59
* {!Cil.dummyFile} when you need a {!Cil_types.file} as a placeholder. For each
60
* global item CIL stores the source location where it appears (using the
61
* type {!Cil_types.location}) *)
63
{ mutable fileName: string; (** The complete file name *)
64
mutable globals: global list; (** List of globals as they will appear
65
in the printed file *)
66
mutable globinit: fundec option;
67
(** An optional global initializer function. This is a function where
68
* you can put stuff that must be executed before the program is
69
* started. This function, is conceptually at the end of the file,
70
* although it is not part of the globals list. Use {!Cil.getGlobInit}
71
* to create/get one. *)
72
mutable globinitcalled: bool;
73
(** Whether the global initialization function is called in main. This
74
should always be false if there is no global initializer. When
75
you create a global initialization CIL will try to insert code in
78
(** Top-level representation of a C source file.
79
@plugin development guide *)
81
(** The main type for representing global declarations and definitions. A list
82
of these form a CIL file. The order of globals in the file is generally
84
@plugin development guide *)
86
| GType of typeinfo * location
87
(** A typedef. All uses of type names (through the [TNamed] constructor)
88
must be preceeded in the file by a definition of the name. The string
89
is the defined name and always not-empty. *)
91
| GCompTag of compinfo * location
92
(** Defines a struct/union tag with some fields. There must be one of
93
these for each struct/union tag that you use (through the [TComp]
94
constructor) since this is the only context in which the fields are
95
printed. Consequently nested structure tag definitions must be
96
broken into individual definitions with the innermost structure
99
| GCompTagDecl of compinfo * location
100
(** Declares a struct/union tag. Use as a forward declaration. This is
101
* printed without the fields. *)
103
| GEnumTag of enuminfo * location
104
(** Declares an enumeration tag with some fields. There must be one of
105
these for each enumeration tag that you use (through the [TEnum]
106
constructor) since this is the only context in which the items are
109
| GEnumTagDecl of enuminfo * location
110
(** Declares an enumeration tag. Use as a forward declaration. This is
111
* printed without the items. *)
113
| GVarDecl of funspec * varinfo * location
114
(** A variable declaration (not a definition). If the variable has a
115
function type then this is a prototype. There can be several
116
declarations and at most one definition for a given variable. If both
117
forms appear then they must share the same varinfo structure. A
118
prototype shares the varinfo with the fundec of the definition. Either
119
has storage Extern or there must be a definition in this file *)
121
| GVar of varinfo * initinfo * location
122
(** A variable definition. Can have an initializer. The initializer is
123
* updateable so that you can change it without requiring to recreate
124
* the list of globals. There can be at most one definition for a
125
* variable in an entire program. Cannot have storage Extern or function
129
| GFun of fundec * location
130
(** A function definition. *)
132
| GAsm of string * location (** Global asm statement. These ones
133
can contain only a template *)
134
| GPragma of attribute * location (** Pragmas at top level. Use the same
135
syntax as attributes *)
136
| GText of string (** Some text (printed verbatim) at
137
top level. E.g., this way you can
138
put comments in the output. *)
139
| GAnnot of global_annotation * location
140
(** a global annotation. Can be
141
- an axiom or a lemma
142
- a predicate declaration or definition
143
- a global type invariant
145
- a logic function declaration or definition.
148
(** {b Types}. A C type is represented in CIL using the type {!Cil_types.typ}.
149
* Among types we differentiate the integral types (with different kinds
150
* denoting the sign and precision), floating point types, enumeration types,
151
* array and pointer types, and function types. Every type is associated with
152
* a list of attributes, which are always kept in sorted order. Use
153
* {!Cil.addAttribute} and {!Cil.addAttributes} to construct list of
154
* attributes. If you want to inspect a type, you should use
155
* {!Cil.unrollType} or {!Cil.unrollTypeDeep} to see through the uses of
157
(** CIL is configured at build-time with the sizes and alignments of the
158
* underlying compiler (GCC or MSVC). CIL contains functions that can compute
159
* the size of a type (in bits) {!Cil.bitsSizeOf}, the alignment of a type
160
* (in bytes) {!Cil.alignOf_int}, and can convert an offset into a start and
161
* width (both in bits) using the function {!Cil.bitsOffset}. At the moment
162
* these functions do not take into account the [packed] attributes and
166
TVoid of attributes (** Void type. Also predefined as {!Cil.voidType} *)
167
| TInt of ikind * attributes
168
(** An integer type. The kind specifies the sign and width. Several
169
* useful variants are predefined as {!Cil.intType}, {!Cil.uintType},
170
* {!Cil.longType}, {!Cil.charType}. *)
172
| TFloat of fkind * attributes
173
(** A floating-point type. The kind specifies the precision. You can
174
* also use the predefined constant {!Cil.doubleType}. *)
176
| TPtr of typ * attributes
177
(** Pointer type. Several useful variants are predefined as
178
* {!Cil.charPtrType}, {!Cil.charConstPtrType} (pointer to a
179
* constant character), {!Cil.voidPtrType},
180
* {!Cil.intPtrType} *)
182
| TArray of typ * exp option * attributes
183
(** Array type. It indicates the base type and the array length. *)
185
| TFun of typ * (string * typ * attributes) list option * bool * attributes
186
(** Function type. Indicates the type of the result, the name, type
187
* and name attributes of the formal arguments ([None] if no
188
* arguments were specified, as in a function whose definition or
189
* prototype we have not seen; [Some \[\]] means void). Use
190
* {!Cil.argsToList} to obtain a list of arguments. The boolean
191
* indicates if it is a variable-argument function. If this is the
192
* type of a varinfo for which we have a function declaration then
193
* the information for the formals must match that in the
194
* function's sformals. Use {!Cil.setFormals}, or
195
* {!Cil.setFunctionType}, or {!Cil.makeFormalVar} for this
198
| TNamed of typeinfo * attributes
199
(** The use of a named type. All uses of the same type name must
200
* share the typeinfo. Each such type name must be preceeded
201
* in the file by a [GType] global. This is printed as just the
202
* type name. The actual referred type is not printed here and is
203
* carried only to simplify processing. To see through a sequence
204
* of named type references, use {!Cil.unrollType}. The attributes
205
* are in addition to those given when the type name was defined. *)
207
| TComp of compinfo * attributes
208
(** A reference to a struct or a union type. All references to the
209
same struct or union must share the same compinfo among them and
210
with a [GCompTag] global that preceeds all uses (except maybe
211
those that are pointers to the composite type). The attributes
212
given are those pertaining to this use of the type and are in
213
addition to the attributes that were given at the definition of
214
the type and which are stored in the compinfo. *)
216
| TEnum of enuminfo * attributes
217
(** A reference to an enumeration type. All such references must
218
share the enuminfo among them and with a [GEnumTag] global that
219
preceeds all uses. The attributes refer to this use of the
220
enumeration and are in addition to the attributes of the
221
enumeration itself, which are stored inside the enuminfo *)
223
| TBuiltin_va_list of attributes
224
(** This is the same as the gcc's type with the same name *)
226
(** Various kinds of integers *)
229
| IChar (** [char] *)
230
| ISChar (** [signed char] *)
231
| IUChar (** [unsigned char] *)
233
| IUInt (** [unsigned int] *)
234
| IShort (** [short] *)
235
| IUShort (** [unsigned short] *)
236
| ILong (** [long] *)
237
| IULong (** [unsigned long] *)
238
| ILongLong (** [long long] (or [_int64] on Microsoft Visual C) *)
239
| IULongLong (** [unsigned long long] (or [unsigned _int64] on Microsoft
242
(** Various kinds of floating-point numbers*)
244
FFloat (** [float] *)
245
| FDouble (** [double] *)
246
| FLongDouble (** [long double] *)
248
(** {b Attributes.} *)
251
| Attr of string * attrparam list
252
(** An attribute has a name and some optional parameters. The name should not
253
* start or end with underscore. When CIL parses attribute names it will
254
* strip leading and ending underscores (to ensure that the multitude of GCC
255
* attributes such as const, __const and __const__ all mean the same thing.) *)
256
| AttrAnnot of string
258
(** Attributes are lists sorted by the attribute name. Use the functions
259
* {!Cil.addAttribute} and {!Cil.addAttributes} to insert attributes in an
260
* attribute list and maintain the sortedness. *)
261
and attributes = attribute list
263
(** The type of parameters of attributes *)
265
| AInt of int (** An integer constant *)
266
| AStr of string (** A string constant *)
267
| ACons of string * attrparam list (** Constructed attributes. These
268
are printed [foo(a1,a2,...,an)].
269
The list of parameters can be
270
empty and in that case the
271
parentheses are not printed. *)
272
| ASizeOf of typ (** A way to talk about types *)
273
| ASizeOfE of attrparam
274
| ASizeOfS of typsig (** Replacement for ASizeOf in type
275
signatures. Only used for
276
attributes inside typsigs.*)
278
| AAlignOfE of attrparam
279
| AAlignOfS of typsig
280
| AUnOp of unop * attrparam
281
| ABinOp of binop * attrparam * attrparam
282
| ADot of attrparam * string (** a.foo **)
283
| AStar of attrparam (** * a *)
284
| AAddrOf of attrparam (** & a **)
285
| AIndex of attrparam * attrparam (** a1[a2] *)
286
| AQuestion of attrparam * attrparam * attrparam (** a1 ? a2 : a3 **)
289
(** {b Structures.} The {!Cil_types.compinfo} describes the definition of a
290
* structure or union type. Each such {!Cil_types.compinfo} must be defined at the
291
* top-level using the [GCompTag] constructor and must be shared by all
292
* references to this type (using either the [TComp] type constructor or from
293
* the definition of the fields.
295
If all you need is to scan the definition of each
296
* composite type once, you can do that by scanning all top-level [GCompTag].
298
* Constructing a {!Cil_types.compinfo} can be tricky since it must contain fields
299
* that might refer to the host {!Cil_types.compinfo} and furthermore the type of
300
* the field might need to refer to the {!Cil_types.compinfo} for recursive types.
301
* Use the {!Cil.mkCompInfo} function to create a {!Cil_types.compinfo}. You can
302
* easily fetch the {!Cil_types.fieldinfo} for a given field in a structure with
303
* {!Cil.getCompField}. *)
305
(** The definition of a structure or union type. Use {!Cil.mkCompInfo} to
306
* make one and use {!Cil.copyCompInfo} to copy one (this ensures that a new
307
* key is assigned and that the fields have the right pointers to parents.).
308
@plugin development guide *)
310
mutable cstruct: bool;
311
(** True if struct, False if union *)
312
mutable cname: string;
313
(** The name. Always non-empty. Use {!Cil.compFullName} to get the full
314
* name of a comp (along with the struct or union) *)
316
(** A unique integer. This is assigned by {!Cil.mkCompInfo} using a
317
* global variable in the Cil module. Thus two identical structs in two
318
* different files might have different keys. Use {!Cil.copyCompInfo} to
319
* copy structures so that a new key is assigned. *)
320
mutable cfields: fieldinfo list;
321
(** Information about the fields. Notice that each fieldinfo has a
322
* pointer back to the host compinfo. This means that you should not
323
* share fieldinfo's between two compinfo's *)
324
mutable cattr: attributes;
325
(** The attributes that are defined at the same time as the composite
326
* type. These attributes can be supplemented individually at each
327
* reference to this [compinfo] using the [TComp] type constructor. *)
328
mutable cdefined: bool;
329
(** This boolean flag can be used to distinguish between structures
330
that have not been defined and those that have been defined but have
331
no fields (such things are allowed in gcc). *)
332
mutable creferenced: bool;
333
(** True if used. Initially set to false. *)
336
(** {b Structure fields.} The {!Cil_types.fieldinfo} structure is used to describe
337
* a structure or union field. Fields, just like variables, can have
338
* attributes associated with the field itself or associated with the type of
339
* the field (stored along with the type of the field). *)
341
(** Information about a struct/union field.
342
@plugin development guide *)
344
mutable fcomp: compinfo;
345
(** The host structure that contains this field. There can be only one
346
* [compinfo] that contains the field. *)
347
mutable fname: string;
348
(** The name of the field. Might be the value of {!Cil.missingFieldName}
349
* in which case it must be a bitfield and is not printed and it does not
350
* participate in initialization *)
353
mutable fbitfield: int option;
354
(** If a bitfield then ftype should be an integer type and the width of
355
* the bitfield must be 0 or a positive integer smaller or equal to the
356
* width of the integer type. A field of width 0 is used in C to control
357
* the alignment of fields. *)
358
mutable fattr: attributes;
359
(** The attributes for this field (not for its type) *)
360
mutable floc: location;
361
(** The location where this field is defined *)
362
mutable faddrof: bool;
363
(** Adapted from CIL [vaddrof] field for variables. Only set for
364
* non-array fields. Variable whose field address is taken is not marked
365
* anymore as having its own address taken.
366
* True if the address of this field is taken. CIL will set these
367
* flags when it parses C, but you should make sure to set the flag
368
* whenever your transformation create [AddrOf] expression. *)
369
mutable fsize_in_bits: int option;
370
(** Similar to [fbitfield] for all types of fields. Useful when
371
* the type of the field is changed in the analyzer, to recall the size
372
* of the original field.
374
mutable foffset_in_bits: int option;
375
(** Store the offset at which the field starts in the structure. *)
376
mutable fpadding_in_bits: int option;
377
(** Store the size of the padding that follows the field, if any. *)
382
(** {b Enumerations.} Information about an enumeration. This is shared by all
383
* references to an enumeration. Make sure you have a [GEnumTag] for each
386
(** Information about an enumeration.
387
@plugin development guide *)
389
mutable ename: string;
390
(** The name. Always non-empty. *)
391
mutable eitems: enumitem list;
392
(** Items. The list must be non-empty *)
393
mutable eattr: attributes;
394
(** The attributes that are defined at the same time as the enumeration
395
* type. These attributes can be supplemented individually at each
396
* reference to this [enuminfo] using the [TEnum] type constructor. *)
397
mutable ereferenced: bool;
398
(** True if used. Initially set to false*)
402
{ mutable einame: string; (** the name, always non-empty. *)
403
mutable eival: exp; (** value of the item.
404
Must be a compile-time constant *)
405
mutable eihost: enuminfo; (** the host enumeration in which the
410
(** Information about a defined type.
411
@plugin development guide *)
413
mutable tname: string;
414
(** The name. Can be empty only in a [GType] when introducing a composite
415
* or enumeration tag. If empty cannot be refered to from the file *)
417
(** The actual type. This includes the attributes that were present in
419
mutable treferenced: bool;
420
(** True if used. Initially set to false*)
424
Each local or global variable is represented by a unique {!Cil_types.varinfo}
425
structure. A global {!Cil_types.varinfo} can be introduced with the [GVarDecl] or
426
[GVar] or [GFun] globals. A local varinfo can be introduced as part of a
427
function definition {!Cil_types.fundec}.
429
All references to a given global or local variable must refer to the same
430
copy of the [varinfo]. Each [varinfo] has a globally unique identifier that
431
can be used to index maps and hashtables (the name can also be used for this
432
purpose, except for locals from different functions). This identifier is
433
constructor using a global counter.
435
It is very important that you construct [varinfo] structures using only one
436
of the following functions:
437
- {!Cil.makeGlobalVar} : to make a global variable
438
- {!Cil.makeTempVar} : to make a temporary local variable whose name
439
will be generated so that to avoid conflict with other locals.
440
- {!Cil.makeLocalVar} : like {!Cil.makeTempVar} but you can specify the
441
exact name to be used.
442
- {!Cil.copyVarinfo}: make a shallow copy of a varinfo assigning a new name
443
and a new unique identifier
445
A [varinfo] is also used in a function type to denote the list of formals.
449
(** Information about a variable.
450
@plugin development guide *)
452
mutable vname: string;
453
(** The name of the variable. Cannot be empty. It is primarily your
454
* responsibility to ensure the uniqueness of a variable name. For local
455
* variables {!Cil.makeTempVar} helps you ensure that the name is unique.
459
(** the original name of the variable. Need not be unique. *)
462
(** The declared type of the variable. *)
464
mutable vattr: attributes;
465
(** A list of attributes associated with the variable.*)
466
mutable vstorage: storage;
467
(** The storage-class *)
470
(** True if this is a global variable*)
472
mutable vdefined: bool;
473
(** True if the variable or function is defined in the file.
474
* Only relevant for functions and global variables.
475
* Not used in particular for local variables and logic variables. *)
477
mutable vformal: bool;
478
(** True if the variable is a formal parameter of a function. *)
480
mutable vinline: bool;
481
(** Whether this varinfo is for an inline function. *)
483
mutable vdecl: location;
484
(** Location of variable declaration. *)
487
(** A unique integer identifier. This field will be
488
* set for you if you use one of the {!Cil.makeFormalVar},
489
* {!Cil.makeLocalVar}, {!Cil.makeTempVar}, {!Cil.makeGlobalVar}, or
490
* {!Cil.copyVarinfo}. *)
492
mutable vaddrof: bool;
493
(** True if the address of this variable is taken. CIL will set these
494
* flags when it parses C, but you should make sure to set the flag
495
* whenever your transformation create [AddrOf] expression. *)
497
mutable vreferenced: bool;
498
(** True if this variable is ever referenced. This is computed by
499
* [removeUnusedVars]. It is safe to just initialize this to False *)
501
mutable vdescr: string option; (** For most temporary variables, a
502
description of what the var holds.
503
(e.g. for temporaries used for
504
function call results, this string
505
is a representation of the function
508
mutable vdescrpure: bool; (** Indicates whether the vdescr above
509
is a pure expression or call.
510
True for all CIL expressions and
511
Lvals, but false for e.g. function
513
Printing a non-pure vdescr more
514
than once may yield incorrect
517
mutable vghost: bool; (** Indicates if the variable is declared in ghost code *)
520
(** False if this variable is a C variable. *)
522
mutable vlogic_var_assoc: logic_var option
523
(** logic variable representing this variable in the logic world*)
526
(** Storage-class information *)
528
NoStorage (** The default storage. Nothing is printed *)
534
(** {b Expressions.} The CIL expression language contains only the side-effect free expressions of
535
C. They are represented as the type {!Cil_types.exp}. There are several
536
interesting aspects of CIL expressions:
538
Integer and floating point constants can carry their textual representation.
539
This way the integer 15 can be printed as 0xF if that is how it occurred in the
542
CIL uses 64 bits to represent the integer constants and also stores the width
543
of the integer type. Care must be taken to ensure that the constant is
544
representable with the given width. Use the functions {!Cil.kinteger},
545
{!Cil.kinteger64} and {!Cil.integer} to construct constant
546
expressions. CIL predefines the constants {!Cil.zero},
547
{!Cil.one} and {!Cil.mone} (for -1).
549
Use the functions {!Cil.isConstant} and {!Cil.isInteger} to test if
550
an expression is a constant and a constant integer respectively.
552
CIL keeps the type of all unary and binary expressions. You can think of that
553
type qualifying the operator. Furthermore there are different operators for
554
arithmetic and comparisons on arithmetic types and on pointers.
556
Another unusual aspect of CIL is that the implicit conversion between an
557
expression of array type and one of pointer type is made explicit, using the
558
[StartOf] expression constructor (which is not printed). If you apply the
559
[AddrOf}]constructor to an lvalue of type [T] then you will be getting an
560
expression of type [TPtr(T)].
562
You can find the type of an expression with {!Cil.typeOf}.
564
You can perform constant folding on expressions using the function
568
(** Expressions (Side-effect free)*)
570
Const of constant (** Constant *)
571
| Lval of lval (** Lvalue *)
573
(** sizeof(<type>). Has [unsigned int] type (ISO 6.5.3.4). This is not
574
* turned into a constant because some transformations might want to
578
(** sizeof(<expression>) *)
580
| SizeOfStr of string
581
(** sizeof(string_literal). We separate this case out because this is the
582
* only instance in which a string literal should not be treated as
583
* having type pointer to character. *)
586
(** This corresponds to the GCC __alignof_. Has [unsigned int] type *)
590
| UnOp of unop * exp * typ
591
(** Unary operation. Includes the type of the result. *)
593
| BinOp of binop * exp * exp * typ
594
(** Binary operation. Includes the type of the result. The arithmetic
595
* conversions are made explicit for the arguments. *)
598
(** Use {!Cil.mkCast} to make casts. *)
601
(** Always use {!Cil.mkAddrOf} to construct one of these. Apply to an
602
* lvalue of type [T] yields an expression of type [TPtr(T)] *)
605
(** Conversion from an array to a pointer to the beginning of the array.
606
* Given an lval of type [TArray(T)] produces an expression of type
607
* [TPtr(T)]. In C this operation is implicit, the [StartOf] operator is
608
* not printed. We have it in CIL because it makes the typing rules
611
| Info of exp * exp_info
612
(** Additional information on the underlying expression *)
614
(** Additional information on an expression *)
617
exp_type : logic_type; (** when used as placeholder for a term *)
618
exp_name: string list;
621
(** {b Constants.} *)
623
(** Literal constants *)
625
| CInt64 of int64 * ikind * string option
626
(** Integer constant. Give the ikind (see ISO9899 6.1.3.2) and the
627
* textual representation, if available. (This allows us to print a
628
* constant as, for example, 0xF instead of 15.) Use {!Cil.integer} or
629
* {!Cil.kinteger} to create these. Watch out for integers that cannot be
630
* represented on 64 bits. OCAML does not give Overflow exceptions. *)
632
(** String constant. The escape characters inside the string have been
633
* already interpreted. This constant has pointer to character type! The
634
* only case when you would like a string literal to have an array type
635
* is when it is an argument to sizeof. In that case you should use
637
| CWStr of int64 list
638
(** Wide character string constant. Note that the local interpretation
639
* of such a literal depends on {!Cil.theMachine.wcharType} and {!Cil.theMachine.wcharKind}.
640
* Such a constant has type pointer to {!Cil.theMachine.wcharType}. The
641
* escape characters in the string have not been "interpreted" in
642
* the sense that L"A\xabcd" remains "A\xabcd" rather than being
643
* represented as the wide character list with two elements: 65 and
644
* 43981. That "interpretation" depends on the underlying wide
647
(** Character constant. This has type int, so use charConstToInt
648
* to read the value in case sign-extension is needed. *)
649
| CReal of float * fkind * string option
650
(** Floating point constant. Give the fkind (see ISO 6.4.4.2) and also
651
* the textual representation, if available. *)
653
(** An enumeration constant
654
* Use [Cillower.lowerEnumVisitor] to replace these with integer
657
(** Unary operators *)
659
Neg (** Unary minus *)
660
| BNot (** Bitwise complement (~) *)
661
| LNot (** Logical Not (!) *)
663
(** Binary operations *)
665
PlusA (** arithmetic + *)
666
| PlusPI (** pointer + integer *)
667
| IndexPI (** pointer + integer but only when
668
* it arises from an expression
669
* [e\[i\]] when [e] is a pointer and
670
* not an array. This is semantically
671
* the same as PlusPI but CCured uses
672
* this as a hint that the integer is
673
* probably positive. *)
674
| MinusA (** arithmetic - *)
675
| MinusPI (** pointer - integer *)
676
| MinusPP (** pointer - pointer *)
680
| Shiftlt (** shift left *)
681
| Shiftrt (** shift right *)
683
| Lt (** < (arithmetic comparison) *)
684
| Gt (** > (arithmetic comparison) *)
685
| Le (** <= (arithmetic comparison) *)
686
| Ge (** >= (arithmetic comparison) *)
687
| Eq (** == (arithmetic comparison) *)
688
| Ne (** != (arithmetic comparison) *)
689
| BAnd (** bitwise and *)
690
| BXor (** exclusive-or *)
691
| BOr (** inclusive-or *)
693
| LAnd (** logical and. Unlike other
694
* expressions this one does not
695
* always evaluate both operands. If
696
* you want to use these, you must
697
* set {!Cil.useLogicalOperators}. *)
698
| LOr (** logical or. Unlike other
699
* expressions this one does not
700
* always evaluate both operands. If
701
* you want to use these, you must
702
* set {!Cil.useLogicalOperators}. *)
704
(** {b Lvalues.} Lvalues are the sublanguage of expressions that can appear at the left of an assignment or as operand to the address-of operator.
705
In C the syntax for lvalues is not always a good indication of the meaning
706
of the lvalue. For example the C value
710
might involve 1, 2 or 3 memory reads when used in an expression context,
711
depending on the declared type of the variable [a]. If [a] has type [int
712
\[4\]\[4\]\[4\]] then we have one memory read from somewhere inside the area
713
that stores the array [a]. On the other hand if [a] has type [int ***] then
714
the expression really means [* ( * ( * (a + 0) + 1) + 2)], in which case it is
715
clear that it involves three separate memory operations.
717
An lvalue denotes the contents of a range of memory addresses. This range
718
is denoted as a host object along with an offset within the object. The
719
host object can be of two kinds: a local or global variable, or an object
720
whose address is in a pointer expression. We distinguish the two cases so
721
that we can tell quickly whether we are accessing some component of a
722
variable directly or we are accessing a memory location through a pointer.
724
tell what an lvalue means CIL represents lvalues as a host object and an
725
offset (see {!Cil_types.lval}). The host object (represented as
726
{!Cil_types.lhost}) can be a local or global variable or can be the object
727
pointed-to by a pointer expression. The offset (represented as
728
{!Cil_types.offset}) is a sequence of field or array index designators.
730
Both the typing rules and the meaning of an lvalue is very precisely
733
The following are a few useful function for operating on lvalues:
734
- {!Cil.mkMem} - makes an lvalue of [Mem] kind. Use this to ensure
735
that certain equivalent forms of lvalues are canonized.
736
For example, [*&x = x].
737
- {!Cil.typeOfLval} - the type of an lvalue
738
- {!Cil.typeOffset} - the type of an offset, given the type of the
740
- {!Cil.addOffset} and {!Cil.addOffsetLval} - extend sequences
742
- {!Cil.removeOffset} and {!Cil.removeOffsetLval} - shrink sequences
745
The following equivalences hold {v
746
Mem(AddrOf(Mem a, aoff)), off = Mem a, aoff + off
747
Mem(AddrOf(Var v, aoff)), off = Var v, aoff + off
748
AddrOf (Mem a, NoOffset) = a
754
(** The host part of an {!Cil_types.lval}. *)
757
(** The host is a variable. *)
760
(** The host is an object of type [T] when the expression has pointer
764
(** The offset part of an {!Cil_types.lval}. Each offset can be applied to certain
765
* kinds of lvalues and its effect is that it advances the starting address
766
* of the lvalue and changes the denoted type, essentially focussing to some
767
* smaller lvalue that is contained in the original one.
768
@plugin development guide *)
770
| NoOffset (** No offset. Can be applied to any lvalue and does
771
* not change either the starting address or the type.
772
* This is used when the lval consists of just a host
773
* or as a terminator in a list of other kinds of
776
| Field of fieldinfo * offset
777
(** A field offset. Can be applied only to an lvalue
778
* that denotes a structure or a union that contains
779
* the mentioned field. This advances the offset to the
780
* beginning of the mentioned field and changes the
781
* type to the type of the mentioned field. *)
783
| Index of exp * offset
784
(** An array index offset. Can be applied only to an
785
* lvalue that denotes an array. This advances the
786
* starting address of the lval to the beginning of the
787
* mentioned array element and changes the denoted type
788
* to be the type of the array element *)
791
(** {b Initializers.}
792
A special kind of expressions are those that can appear as initializers for
793
global variables (initialization of local variables is turned into
794
assignments). The initializers are represented as type {!Cil_types.init}. You
795
can create initializers with {!Cil.makeZeroInit} and you can conveniently
796
scan compound initializers them with {!Cil.foldLeftCompound}.
798
(** Initializers for global variables. *)
800
| SingleInit of exp (** A single initializer *)
801
| CompoundInit of typ * (offset * init) list
802
(** Used only for initializers of structures, unions and arrays.
803
* The offsets are all of the form [Field(f, NoOffset)] or
804
* [Index(i, NoOffset)] and specify the field or the index being
805
* initialized. For structures all fields
806
* must have an initializer (except the unnamed bitfields), in
807
* the proper order. This is necessary since the offsets are not
808
* printed. For arrays the list must contain a prefix of the
809
* initializers; the rest are 0-initialized.
810
* For unions there must be exactly one initializer. If
811
* the initializer is not for the first field then a field
812
* designator is printed, so you better be on GCC since MSVC does
813
* not understand this. You can scan an initializer list with
814
* {!Cil.foldLeftCompound}. *)
816
(** We want to be able to update an initializer in a global variable, so we
817
* define it as a mutable field *)
819
mutable init : init option;
822
(** {b Function definitions.}
823
A function definition is always introduced with a [GFun] constructor at the
824
top level. All the information about the function is stored into a
825
{!Cil_types.fundec}. Some of the information (e.g. its name, type,
826
storage, attributes) is stored as a {!Cil_types.varinfo} that is a field of the
827
[fundec]. To refer to the function from the expression language you must use
830
The function definition contains, in addition to the body, a list of all the
831
local variables and separately a list of the formals. Both kind of variables
832
can be referred to in the body of the function. The formals must also be shared
833
with the formals that appear in the function type. For that reason, to
834
manipulate formals you should use the provided functions
835
{!Cil.makeFormalVar} and {!Cil.setFormals}.
837
(** Function definitions.
838
@plugin development guide *)
840
{ mutable svar: varinfo;
841
(** Holds the name and type as a variable, so we can refer to it
842
* easily from the program. All references to this function either
843
* in a function call or in a prototype must point to the same
845
mutable sformals: varinfo list;
846
(** Formals. These must be in the same order and with the same
847
* information as the formal information in the type of the function.
848
* Use {!Cil.setFormals} or
849
* {!Cil.setFunctionType} to set these formals and ensure that they
850
* are reflected in the function type. Do not make copies of these
851
* because the body refers to them. *)
852
mutable slocals: varinfo list;
853
(** Locals. Does NOT include the sformals. Do not make copies of
854
* these because the body refers to them. *)
855
mutable smaxid: int; (** Max local id. Starts at 0. Used for
856
* creating the names of new temporary
857
* variables. Updated by
858
* {!Cil.makeLocalVar} and
859
* {!Cil.makeTempVar}. You can also use
860
* {!Cil.setMaxId} to set it after you
861
* have added the formals and locals. *)
862
mutable sbody: block; (** The function body. *)
863
mutable smaxstmtid: int option; (** max id of a (reachable) statement
864
* in this function, if we have
865
* computed it. range = 0 ...
866
* (smaxstmtid-1). This is computed by
867
* {!Cil.computeCFGInfo}. *)
868
mutable sallstmts: stmt list; (** After you call {!Cil.computeCFGInfo}
869
* this field is set to contain all
870
* statements in the function *)
871
mutable sspec: funspec;
875
(** A block is a sequence of statements with the control falling through from
876
one element to the next *)
878
{ mutable battrs: attributes; (** Attributes for the block *)
879
mutable bstmts: stmt list; (** The statements comprising the block*)
883
CIL statements are the structural elements that make the CFG. They are
884
represented using the type {!Cil_types.stmt}. Every
885
statement has a (possibly empty) list of labels. The
886
{!Cil_types.stmtkind} field of a statement indicates what kind of statement it
889
Use {!Cil.mkStmt} to make a statement and the fill-in the fields.
891
CIL also comes with support for control-flow graphs. The [sid] field in
892
[stmt] can be used to give unique numbers to statements, and the [succs]
893
and [preds] fields can be used to maintain a list of successors and
894
predecessors for every statement. The CFG information is not computed by
895
default. Instead you must explicitly use the functions
896
{!Cil.prepareCFG} and {!Cil.computeCFGInfo} to do it.
900
@plugin development guide *)
902
mutable labels: label list;
903
(** Whether the statement starts with some labels, case statements or
904
* default statements. *)
906
mutable skind: stmtkind;
907
(** The kind of statement *)
910
(** A number (>= 0) that is unique in a function. Filled in only after
911
* the CFG is computed. *)
912
mutable succs: stmt list;
913
(** The successor statements. They can always be computed from the skind
914
* and the context in which this statement appears. Filled in only after
915
* the CFG is computed. *)
916
mutable preds: stmt list;
917
(** The inverse of the succs function. *)
924
Label of string * location * bool
925
(** A real label. If the bool is "true", the label is from the
926
* input source program. If the bool is "false", the label was
927
* created by CIL or some other transformation *)
928
| Case of exp * location (** A case statement. This expression
929
* is lowered into a constant if
930
* {!Cil.lowerConstants} is set to
932
| Default of location (** A default statement *)
936
(* The various kinds of statements *)
939
(** A group of instructions that do not contain control flow. Control
940
* implicitly falls through. *)
942
| Return of exp option * location
943
(** The return statement. This is a leaf in the CFG. *)
945
| Goto of stmt ref * location
946
(** A goto statement. Appears from actual goto's in the code or from
947
* goto's that have been inserted during elaboration. The reference
948
* points to the statement that is the target of the Goto. This means that
949
* you have to update the reference whenever you replace the target
950
* statement. The target statement MUST have at least a label. *)
953
(** A break to the end of the nearest enclosing Loop or Switch *)
955
| Continue of location
956
(** A continue to the start of the nearest enclosing [Loop] *)
957
| If of exp * block * block * location
958
(** A conditional. Two successors, the "then" and the "else" branches.
959
* Both branches fall-through to the successor of the If statement. *)
961
| Switch of exp * block * (stmt list) * location
962
(** A switch statement. The statements that implement the cases can be
963
* reached through the provided list. For each such target you can find
964
* among its labels what cases it implements. The statements that
965
* implement the cases are somewhere within the provided [block]. *)
967
| Loop of code_annotation list *
968
block * location * (stmt option) * (stmt option)
969
(** A [while(1)] loop. The termination test is implemented in the body of
970
* a loop using a [Break] statement. If prepareCFG has been called,
971
* the first stmt option will point to the stmt containing the continue
972
* label for this loop and the second will point to the stmt containing
973
* the break label for this loop. *)
976
(** Just a block of statements. Use it as a way to keep some block
977
* attributes local *)
979
| UnspecifiedSequence of (stmt * lval list * lval list) list
980
(** statements whose order of execution is not specified by
981
ISO/C. This is important for the order of side effects
982
during evaluation of expressions. Each statement comes
983
together with a list of lval that are written during its
984
evaluation, together with the lval that are read.
985
Note that this include only a subset of the affectations
986
of the statement. Namely, the
987
temporary variables generated by cil are excluded (i.e. it
988
is assumed that the "compilation" is correct). In addition,
989
side effects caused by function applications are not taken
990
into account in the list. For a single statement, the written lvals
991
are supposed to be ordered (or their order of evaluation doesn't
992
matter), so that an alarm should be emitted only if the lvals read by
993
a statement overlap with the lvals written (or read) by another
994
statement of the sequence.
996
At this time this feature is
997
experimental and may miss some unspecified sequences.
999
In case you do not care about this feature just handle it
1000
like a block (see {!Cil.block_from_unspecified_sequence}) *)
1001
| TryFinally of block * block * location
1002
(** On MSVC we support structured exception handling. This is what you
1003
* might expect. Control can get into the finally block either from the
1004
* end of the body block, or if an exception is thrown. *)
1006
| TryExcept of block * (instr list * exp) * block * location
1007
(** On MSVC we support structured exception handling. The try/except
1008
* statement is a bit tricky:
1015
The argument to __except must be an expression. However, we keep a
1016
list of instructions AND an expression in case you need to make
1017
function calls. We'll print those as a comma expression. The control
1018
can get to the __except expression only if an exception is thrown.
1019
After that, depending on the value of the expression the control
1020
goes to the handler, propagates the exception, or retries the
1021
exception !!! The location corresponds to the try keyword.
1025
(** Instructions. They may cause effects directly but may not have control
1028
Set of lval * exp * location (** An assignment. A cast is present
1029
if the exp has different type
1031
| Call of lval option * exp * exp list * location
1032
(** optional: result is an lval. A cast might be
1033
necessary if the declared result type of the
1034
function is not the same as that of the
1035
destination. If the function is declared then
1036
casts are inserted for those arguments that
1037
correspond to declared formals. (The actual
1038
number of arguments might be smaller or larger
1039
than the declared number of arguments. C allows
1040
this.) If the type of the result variable is not
1041
the same as the declared type of the function
1042
result then an implicit cast exists. *)
1044
(* See the GCC specification for the meaning of ASM.
1045
* If the source is MS VC then only the templates
1047
(* sm: I've added a notes.txt file which contains more
1048
* information on interpreting Asm instructions *)
1049
| Asm of attributes * (* Really only const and volatile can appear
1051
string list * (* templates (CR-separated) *)
1052
(string option * string * lval) list *
1053
(* outputs must be lvals with
1054
* optional names and constraints.
1055
* I would like these
1056
* to be actually variables, but I
1057
* run into some trouble with ASMs
1058
* in the Linux sources *)
1059
(string option * string * exp) list *
1060
(* inputs with optional names and constraints *)
1061
string list * (* register clobbers *)
1063
(** An inline assembly instruction. The arguments are (1) a list of
1064
attributes (only const and volatile can appear here and only for
1065
GCC), (2) templates (CR-separated), (3) a list of
1066
outputs, each of which is an lvalue with a constraint, (4) a list
1067
of input expressions along with constraints, (5) clobbered
1068
registers, and (5) location information *)
1072
| Code_annot of code_annotation * location
1074
(** Describes a location in a source file *)
1075
and location = Lexing.position * Lexing.position
1077
(** Type signatures. Two types are identical iff they have identical
1080
TSArray of typsig * int64 option * attribute list
1081
| TSPtr of typsig * attribute list
1082
| TSComp of bool * string * attribute list
1083
| TSFun of typsig * typsig list * bool * attribute list
1084
| TSEnum of string * attribute list
1087
(** Abstract syntax trees for annotations *)
1089
(** Types of logic terms. *)
1091
| Ctype of typ (** a C type *)
1092
| Ltype of string * logic_type list
1093
(** an user-defined logic type with its parameters *)
1094
| Lvar of string (** a type variable. *)
1095
| Linteger (** mathematical integers, {i i.e.} Z *)
1096
| Lreal (** mathematical reals, {i i.e.} R *)
1097
| Larrow of logic_type list * logic_type (** (n-ary) function type *)
1099
(** sets of terms. *)
1101
TSSingleton of tsets_elem (** a single term *)
1102
| TSEmpty (** the empty set. *)
1103
| TSUnion of tsets list (** union of terms. *)
1104
| TSInter of tsets list (** intersection of terms. *)
1105
| TSComprehension of
1106
tsets * quantifiers * predicate named option
1107
(** set defined in comprehension ({t \{ t[i] | integer i; 0 <= i < 5\}})
1110
(** base address of a (set of) location. *)
1112
TSVar of logic_var (** variable *)
1113
| TSResult (** returned value of the specified function. *)
1114
| TSMem of tsets_elem (** memory access. *)
1116
(** A (set of) location: base address and offset *)
1117
and tsets_lval = tsets_lhost * tsets_offset
1119
(** Single elements of a tset *)
1121
| TSLval of tsets_lval (** location. *)
1122
| TSStartOf of tsets_lval (** start of an array. *)
1123
| TSAddrOf of tsets_lval (** (set of) addresses. *)
1124
| TSConst of constant (** An integer constant. *)
1125
| TSAdd_index of tsets_elem * term (** an element plus a given term. *)
1126
| TSAdd_range of tsets_elem * term option * term option
1127
(** an element plus a term in a given range. *)
1128
| TSCastE of typ * tsets_elem (** cast *)
1129
| TSat of tsets_elem * logic_label (** the element must be evaluated at
1130
a particular program point. *)
1131
| TSapp of logic_info * (logic_label * logic_label) list * term list
1132
(** application of a function returning a tsets
1133
(NB: the tset is not necessarily a singleton). *)
1135
(** offset of a tset element *)
1137
TSNoOffset (** no further offset*)
1138
| TSIndex of term * tsets_offset (** index *)
1139
| TSRange of term option * term option * tsets_offset
1140
(** index in a given range. *)
1141
| TSField of fieldinfo * tsets_offset
1142
(** field of a compound type. *)
1144
(** tsets with an unique identifier.
1145
Use [Logic_const.new_location] to generate a new id. *)
1146
and identified_tsets =
1147
{ its_id: int; (** the identifier. *)
1148
its_content: tsets (** the tset *)
1151
(** logic label referring to a particular program point. *)
1153
| StmtLabel of stmt ref (** label of a C statement. *)
1154
| LogicLabel of string (** builtin logic label ({t Here, Pre}, ...) *)
1156
(* Expressions follow CIL constructs (with prefix T) *)
1160
term_node : term_node; (** kind of term. *)
1161
term_loc : Lexing.position * Lexing.position;
1162
(** position in the source file. *)
1163
term_type : logic_type; (** type of the term. *)
1164
term_name: string list; (** names of the term if any. *)
1167
(** the various kind of terms. *)
1169
(* same constructs as exp *)
1170
| TConst of constant (** a constant. *)
1171
| TLval of term_lval (** an L-value *)
1172
| TSizeOf of typ (** size of a given C type. *)
1173
| TSizeOfE of term (** size of the type of an expression. *)
1174
| TSizeOfStr of string (** size of a string constant. *)
1175
| TAlignOf of typ (** alignment of a type. *)
1176
| TAlignOfE of term (** alignment of the type of an expression. *)
1177
| TUnOp of unop * term (** unary operator. *)
1178
| TBinOp of binop * term * term (** binary operators. *)
1179
| TCastE of typ * term (** cast to a C type. *)
1180
| TAddrOf of term_lval (** address of a term. *)
1181
| TStartOf of term_lval (** beginning of an array. *)
1182
(* additional constructs *)
1183
| Tapp of logic_info * (logic_label * logic_label) list * term list
1184
(** application of a logic function. *)
1185
| Tlambda of quantifiers * term (** lambda abstraction. *)
1186
| TDataCons of logic_ctor_info * term list
1187
(** constructor of logic sum-type. *)
1188
| Tif of term * term * term
1189
(** conditional operator*)
1190
| Told of term (** term refers to the pre-state of the function. *)
1191
| Tat of term * logic_label
1192
(** term refers to a particular program point. *)
1193
| Tbase_addr of term (** base address of a pointer. *)
1194
| Tblock_length of term (** length of the block pointed to by the term. *)
1195
| Tnull (** the null pointer. *)
1196
| TCoerce of term * typ (** coercion to a given C type. *)
1197
| TCoerceE of term * term (** coercion to the type of a given term. *)
1198
| TUpdate of term * fieldinfo * term
1199
(** functional update of a field. *)
1200
| Ttypeof of term (** type tag for a term. *)
1201
| Ttype of typ (** type tag for a C type. *)
1203
(** set of lval seen as a term. Note that a term t used where a tset is
1204
expected will be considered as [TSets(TSSingleton t)] (unless it has
1205
type [tsets<a>] of course)
1208
(** lvalue: base address and offset. *)
1210
term_lhost * term_offset
1212
(** base address of an lvalue. *)
1214
| TVar of logic_var (** a variable. *)
1215
| TResult (** value returned by a function. *)
1216
| TMem of term (** memory access. *)
1218
(** offset of an lvalue. *)
1220
| TNoOffset (** no further offset. *)
1221
| TField of fieldinfo * term_offset
1222
(** access to the field of a compound type. *)
1223
| TIndex of term * term_offset
1225
(** description of a logic function or predicate.
1226
@plugin development guide *)
1228
mutable l_name : string; (** name of the function. *)
1229
l_labels : logic_label list; (** label arguments of the function. *)
1230
l_tparams : string list; (** type parameters *)
1231
mutable l_type : logic_type option; (** return type. None for predicates *)
1232
mutable l_profile : logic_var list; (** type of the arguments. *)
1233
mutable l_body : logic_body; (** body of the function. *)
1237
| LBreads of tsets list (** read accesses performed by a function. *)
1238
| LBterm of term (** direct definition of a function. *)
1239
| LBpred of predicate named (** direct definition of a predicate. *)
1241
(string * logic_label list * string list * predicate named) list
1242
(** inductive definition *)
1244
(** description of a logic type*)
1245
and logic_type_info =
1246
{ nb_params : int; (** number of type parameters*)
1248
(* will be expanded when dealing with concrete types *)
1250
(** description of a logic variable
1251
@plugin development guide *)
1253
mutable lv_name : string; (** name of the variable. *)
1254
mutable lv_id : int; (** unique identifier *)
1255
mutable lv_type : logic_type; (** type of the variable. *)
1256
mutable lv_origin : varinfo option (** when the logic variable stems from a
1257
C variable, set to the original C variable.
1261
(** description of a constructor of a logic sum-type*)
1262
and logic_ctor_info =
1263
{ ctor_name: string; (** name of the constructor. *)
1264
ctor_type: logic_type; (** type to which the constructor belongs. *)
1265
ctor_params: logic_type list
1266
(** types of the parameters of the constructor. *)
1271
(** variables bound by a quantifier. *)
1272
and quantifiers = logic_var list
1274
(** comparison relations*)
1275
and relation = Rlt | Rgt | Rle | Rge | Req | Rneq
1279
| Pfalse (** always-false predicate. *)
1280
| Ptrue (** always-true predicate. *)
1281
| Papp of logic_info * (logic_label * logic_label) list * term list
1282
(** application of a predicate. *)
1283
| Pseparated of tsets list
1284
| Prel of relation * term * term
1285
(** comparison of two terms. *)
1286
| Pand of predicate named * predicate named
1288
| Por of predicate named * predicate named
1290
| Pxor of predicate named * predicate named
1292
| Pimplies of predicate named * predicate named
1294
| Piff of predicate named * predicate named
1296
| Pnot of predicate named
1298
| Pif of term * predicate named * predicate named
1300
| Plet of logic_var * term * predicate named
1301
(** definition of a local variable *)
1302
| Pforall of quantifiers * predicate named
1303
(** universal quantification. *)
1304
| Pexists of quantifiers * predicate named
1305
(** existential quantification. *)
1306
| Pold of predicate named
1307
(** predicate refers to the pre-state of a function. *)
1308
| Pat of predicate named * logic_label
1309
(** predicate refers to a particular program point. *)
1311
(** the given locations are valid. *)
1312
| Pvalid_index of term * term
1313
(** {b deprecated:} Use [Pvalid(TSSingleton(TSAdd_index(p,i)))] instead
1315
[Pvalid_index(p,i)] indicates that accessing the [i]th element
1318
| Pvalid_range of term * term * term
1319
(** {b deprecated:} Use [Pvalid(TSSingleton(TSAdd_range(p,i1,i2)))]
1322
similar to [Pvalid_index] but for a range of indices.*)
1324
(** The given term is newly allocated in the post-state of a function.*)
1325
| Psubtype of term * term
1326
(** First term is a type tag that is a subtype of the second. *)
1328
(* replaced by logic_info
1329
(** Description of a predicate
1330
@plugin development guide *)
1331
and predicate_info = {
1332
mutable p_name : string; (** name of the predicate. *)
1333
mutable p_profile : logic_var list; (** arguments of the predicate. *)
1334
p_labels : logic_label list; (** label arguments. *)
1335
mutable p_body : predicate_body (** definition. *)
1338
(** predicate with an unique identifier.
1339
Use [Logic_const.new_predicate] to create fresh predicates *)
1340
and identified_predicate = {
1341
ip_name: string list; (** names given to the predicate if any.*)
1342
ip_loc: location; (** location in the source code. *)
1343
ip_id: int; (** identifier *)
1344
ip_content: predicate; (** the predicate itself*)
1348
(** definition of a predicate *)
1349
and predicate_body =
1350
| PReads of tsets list (** read accesses performed by the predicate. *)
1351
| PDefinition of predicate named (** body of the predicate. *)
1354
(* Polymorphic types shared with parsed trees (Logic_ptree) *)
1355
(** variant of a loop or a recursive function. Type shared with Logic_ptree. *)
1356
and 'term variant = 'term * string option
1358
(** zone assigned by a C function. Type shared with Logic_ptree. *)
1360
Location of 'locs (** tsets *)
1361
| Nothing (** nothing is assigned. *)
1363
(** zone assigned with its dependencies. Type shared with Logic_ptree.*)
1364
and 'locs assigns = 'locs zone * ('locs zone list)
1366
(** object that can be named (in particular predicates). *)
1367
and 'a named = { name : string list; (** list of given names *)
1368
loc : location; (** position in the source code. *)
1369
content : 'a; (** content *)
1372
(** function contract. Type shared with Logic_ptree. *)
1373
and ('term,'pred,'locs) spec = {
1374
mutable spec_requires : 'pred list; (** global requirements. *)
1375
mutable spec_behavior : ('pred,'locs) behavior list;
1377
mutable spec_variant : 'term variant option;
1378
(** variant for recursive functions. *)
1379
mutable spec_terminates: 'pred option;
1380
(** termination condition. *)
1381
mutable spec_complete_behaviors: string list list;
1382
(** list of complete behaviors.
1383
It is possible to have more than one set of complete behaviors *)
1384
mutable spec_disjoint_behaviors: string list list;
1385
(** list of disjoint behaviors.
1386
It is possible to have more than one set of disjoint behaviors *)
1389
(* proposal for bug #305 *)
1391
and ('term,'pred,'locs) func_annot =
1392
Requires of string * 'pred
1393
| Assumes of string * 'pred
1394
| Ensures of string * 'pred
1395
| Variant of 'term variant
1396
| Terminates of 'pred
1397
| Complete_behaviors of string list
1398
| Disjoint_behaviors of string list
1400
and func_annotation =
1403
fa_content: (term, predicate named, tsets) func_annot
1409
(** behavior of a function. Type shared with Logic_ptree. *)
1410
and ('pred,'locs) behavior = {
1411
mutable b_name : string; (** name of the behavior. *)
1412
mutable b_assumes : 'pred list; (** assume clauses. *)
1413
mutable b_ensures : 'pred list; (** ensure clauses. *)
1414
mutable b_assigns : 'locs assigns list; (** assignments. *)
1417
(** pragmas for the value analysis plugin of Frama-C.
1418
Type shared with Logic_ptree.*)
1419
and 'term loop_pragma =
1420
| Unroll_level of 'term
1421
| Widen_hints of 'term list
1422
| Widen_variables of 'term list
1424
(** pragmas for the slicing plugin of Frama-C. Type shared with Logic_ptree.*)
1425
and 'term slice_pragma =
1430
(** pragmas for the impact plugin of Frama-C. Type shared with Logic_ptree.*)
1431
and 'term impact_pragma =
1435
(** the various kinds of pragmas. Type shared with Logic_ptree. *)
1437
| Loop_pragma of 'term loop_pragma
1438
| Slice_pragma of 'term slice_pragma
1439
| Impact_pragma of 'term impact_pragma
1441
(** Annotation status *)
1442
and validity = True | False | Maybe
1443
and annot_checked_status = { mutable emitter : string;
1444
mutable valid : validity }
1445
and annotation_status = | Unknown (* Nothing was ever tried to check it *)
1446
| Checked of annot_checked_status (* Something was tried *)
1447
and annot_status = { mutable status : annotation_status }
1448
(** all annotations that can be found in the code.
1449
Type shared with Logic_ptree. *)
1450
and ('term, 'pred, 'spec_pred, 'locs) code_annot =
1451
| AAssert of string list * 'pred * annot_status
1452
(** assertion to be checked. The list of strings is the list of
1453
behaviors to which this assertion applies. *)
1454
| AAssume of 'pred (** assertion assumed to be true *)
1455
| AStmtSpec of ('term, 'spec_pred, 'locs) spec (** statement contract. *)
1456
| AInvariant of string list * bool * 'pred
1457
(** code invariant. The list of strings is the list of
1458
behaviors to which this invariant applies.
1459
The boolean flag is true for normal loop invariants
1460
and false for invariant-as-assertions.*)
1461
| AVariant of 'term variant (** loop variant. Note that
1462
there can be at most one variant
1463
associated to a given statement
1465
| AAssigns of 'locs assigns (** loop assigns *)
1466
| APragma of 'term pragma (** pragma. *)
1468
(** function contract. *)
1469
and funspec = (term, identified_predicate, identified_tsets) spec
1471
(** code annotation with an unique identifier.
1472
Use [Logic_const.new_code_annotation] to create new code annotations with
1474
and code_annotation =
1476
(term, predicate named, identified_predicate, identified_tsets)
1477
code_annot; (** content of the annotation. *)
1478
annot_id: int (** identifier. *) }
1480
(** behavior of a function. *)
1481
and funbehavior = (identified_predicate,identified_tsets) behavior
1483
(** global annotations, not attached to a statement or a function. *)
1484
and global_annotation =
1485
| Dfun_or_pred of logic_info
1486
| Daxiomatic of string * global_annotation list
1488
| Dpredicate_reads of
1489
logic_info * string list
1490
* logic_var list * tsets list
1491
(** declaration of a predicate.
1492
[Dpredicate_info(infos,type_vars,profile,reads)]
1495
logic_info * string list * logic_var list *
1497
(** definition of a predicate. *)
1499
logic_info * string list * logic_var list *
1500
(string * predicate named) list
1501
(** inductive definition of a predicate. *)
1503
logic_info * string list *
1504
logic_var list * logic_type * tsets list
1505
(** declaration of a logic function.
1506
[Dlogic_reads(infos,type_vars,profile,rt_type,reads)]
1509
logic_info * string list *
1510
logic_var list * logic_type * term
1511
(** definition of a logic function. *)
1512
| Dlogic_axiomatic of
1513
logic_info * string list *
1514
logic_var list * logic_type * (string * predicate named) list
1515
(** definition of a logic function. *)
1517
| Dtype of string * string list (** declaration of a logic type. *)
1518
| Dlemma of string * bool * logic_label list * string list * predicate named
1519
(** definition of a lemma. The boolean flag is true if the property.
1520
should be taken as an axiom and false if it must be proved.
1522
| Dinvariant of logic_info
1523
(** global invariant. The predicate does not have any argument. *)
1524
| Dtype_annot of logic_info
1525
(** type invariant. The predicate has exactly one argument. *)
1532
version_major: int; (* Major version number *)
1533
version_minor: int; (* Minor version number *)
1534
version: string; (* version number *)
1535
underscore_name: bool; (* If assembly names have leading underscore *)
1536
sizeof_short: int; (* Size of "short" *)
1537
sizeof_int: int; (* Size of "int" *)
1538
sizeof_long: int ; (* Size of "long" *)
1539
sizeof_longlong: int; (* Size of "long long" *)
1540
sizeof_ptr: int; (* Size of pointers *)
1541
sizeof_enum: int; (* Size of enum types *)
1542
sizeof_float: int; (* Size of "float" *)
1543
sizeof_double: int; (* Size of "double" *)
1544
sizeof_longdouble: int; (* Size of "long double" *)
1545
sizeof_void: int; (* Size of "void" *)
1546
sizeof_fun: int; (* Size of function *)
1547
size_t: string; (* Type of "sizeof(T)" *)
1548
wchar_t: string; (* Type of "wchar_t" *)
1549
ptrdiff_t: string; (* Type of "ptrdiff_t" *)
1550
enum_are_signed: bool; (* Sign of enum types *)
1551
alignof_short: int; (* Alignment of "short" *)
1552
alignof_int: int; (* Alignment of "int" *)
1553
alignof_long: int; (* Alignment of "long" *)
1554
alignof_longlong: int; (* Alignment of "long long" *)
1555
alignof_ptr: int; (* Alignment of pointers *)
1556
alignof_enum: int; (* Alignment of enum types *)
1557
alignof_float: int; (* Alignment of "float" *)
1558
alignof_double: int; (* Alignment of "double" *)
1559
alignof_longdouble: int; (* Alignment of "long double" *)
1560
alignof_str: int; (* Alignment of strings *)
1561
alignof_fun: int; (* Alignment of function *)
1562
alignof_char_array: int; (* Alignment of arrays of char *)
1563
char_is_unsigned: bool; (* Whether "char" is unsigned *)
1564
const_string_literals: bool; (* Whether string literals have const chars *)
1565
little_endian: bool; (* whether the machine is little endian *)
1570
compile-command: "LC_ALL=C make -C ../.."
added
removed
cil/src/cil_types.mli
