1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
|
(*
*
* Copyright (c) 2001-2002,
* George C. Necula <necula@cs.berkeley.edu>
* Scott McPeak <smcpeak@cs.berkeley.edu>
* Wes Weimer <weimer@cs.berkeley.edu>
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* 1. Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* 2. Redistributions in binary form must reproduce the above copyright
* notice, this list of conditions and the following disclaimer in the
* documentation and/or other materials provided with the distribution.
*
* 3. The names of the contributors may not be used to endorse or promote
* products derived from this software without specific prior written
* permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
* IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
* OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
* EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
* PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
* PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
* LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
* NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*
*)
(** This file was originally part of Hugues Casee's frontc 2.0, and has been
* extensively changed since.
**
** 1.0 3.22.99 Hugues Cassé First version.
** 2.0 George Necula 12/12/00: Many extensions
**)
(*
** Types
*)
type cabsloc = {
lineno : int;
filename: string;
byteno: int;
ident : int;
}
type typeSpecifier = (* Merge all specifiers into one type *)
Tvoid (* Type specifier ISO 6.7.2 *)
| Tchar
| Tshort
| Tint
| Tlong
| Tint64
| T_Bool
| Tfloat
| Tdouble
| Tsigned
| Tunsigned
| Tnamed of string
(* each of the following three kinds of specifiers contains a field
* or item list iff it corresponds to a definition (as opposed to
* a forward declaration or simple reference to the type); they
* also have a list of __attribute__s that appeared between the
* keyword and the type name (definitions only) *)
| Tstruct of string * field_group list option * attribute list
| Tunion of string * field_group list option * attribute list
| Tenum of string * enum_item list option * attribute list
| TtypeofE of expression (* GCC __typeof__ *)
| TtypeofT of specifier * decl_type (* GCC __typeof__ *)
and storage =
NO_STORAGE | AUTO | STATIC | EXTERN | REGISTER
and funspec =
INLINE | VIRTUAL | EXPLICIT
and cvspec =
CV_CONST | CV_VOLATILE | CV_RESTRICT
(* Type specifier elements. These appear at the start of a declaration *)
(* Everywhere they appear in this file, they appear as a 'spec_elem list', *)
(* which is not interpreted by cabs -- rather, this "word soup" is passed *)
(* on to the compiler. Thus, we can represent e.g. 'int long float x' even *)
(* though the compiler will of course choke. *)
and spec_elem =
SpecTypedef
| SpecCV of cvspec (* const/volatile *)
| SpecAttr of attribute (* __attribute__ *)
| SpecStorage of storage
| SpecInline
| SpecType of typeSpecifier
(* decided to go ahead and replace 'spec_elem list' with specifier *)
and specifier = spec_elem list
(* Declarator type. They modify the base type given in the specifier. Keep
* them in the order as they are printed (this means that the top level
* constructor for ARRAY and PTR is the inner-level in the meaning of the
* declared type) *)
and decl_type =
| JUSTBASE (* Prints the declared name *)
| PARENTYPE of attribute list * decl_type * attribute list
(* Prints "(attrs1 decl attrs2)".
* attrs2 are attributes of the
* declared identifier and it is as
* if they appeared at the very end
* of the declarator. attrs1 can
* contain attributes for the
* identifier or attributes for the
* enclosing type. *)
| ARRAY of decl_type * attribute list * expression
(* Prints "decl [ attrs exp ]".
* decl is never a PTR. *)
| PTR of attribute list * decl_type (* Prints "* attrs decl" *)
| PROTO of decl_type * single_name list * bool
(* Prints "decl (args[, ...])".
* decl is never a PTR.*)
(* The base type and the storage are common to all names. Each name might
* contain type or storage modifiers *)
(* e.g.: int x, y; *)
and name_group = specifier * name list
(* The optional expression is the bitfield *)
and field_group = specifier * (name * expression option) list
(* like name_group, except the declared variables are allowed to have initializers *)
(* e.g.: int x=1, y=2; *)
and init_name_group = specifier * init_name list
(* The decl_type is in the order in which they are printed. Only the name of
* the declared identifier is pulled out. The attributes are those that are
* printed after the declarator *)
(* e.g: in "int *x", "*x" is the declarator; "x" will be pulled out as *)
(* the string, and decl_type will be PTR([], JUSTBASE) *)
and name = string * decl_type * attribute list * cabsloc
(* A variable declarator ("name") with an initializer *)
and init_name = name * init_expression
(* Single names are for declarations that cannot come in groups, like
* function parameters and functions *)
and single_name = specifier * name
and enum_item = string * expression * cabsloc
(*
** Declaration definition (at toplevel)
*)
and definition =
FUNDEF of single_name * block * cabsloc * cabsloc
| DECDEF of init_name_group * cabsloc (* global variable(s), or function prototype *)
| TYPEDEF of name_group * cabsloc
| ONLYTYPEDEF of specifier * cabsloc
| GLOBASM of string * cabsloc
| PRAGMA of string * cabsloc
| LINKAGE of string * cabsloc * definition list (* extern "C" { ... } *)
(* the string is a file name, and then the list of toplevel forms *)
and file = string * definition list
(*
** statements
*)
(* A block contains a list of local label declarations ( GCC's ({ __label__
* l1, l2; ... }) ) , a list of definitions and a list of statements *)
and block =
{ blabels: string list;
battrs: attribute list;
bstmts: statement list
}
(* GCC asm directives have lots of extra information to guide the optimizer *)
and asm_details =
{ aoutputs: (string option * string * expression) list; (* optional name, constraints and expressions for outputs *)
ainputs: (string option * string * expression) list; (* optional name, constraints and expressions for inputs *)
aclobbers: string list (* clobbered registers *)
}
and statement =
NOP of cabsloc
| COMPUTATION of expression * cabsloc
| BLOCK of block * cabsloc
(* | SEQUENCE of statement * statement * cabsloc *)
| IF of expression * statement * statement * cabsloc
| WHILE of expression * statement * cabsloc
| DOWHILE of expression * statement * cabsloc
| FOR of for_clause * expression * expression * statement * cabsloc
| BREAK of cabsloc
| CONTINUE of cabsloc
| RETURN of expression * cabsloc
| SWITCH of expression * statement * cabsloc
| CASE of expression * statement * cabsloc
| CASERANGE of expression * expression * statement * cabsloc
| DEFAULT of statement * cabsloc
| LABEL of string * statement * cabsloc
| GOTO of string * cabsloc
| COMPGOTO of expression * cabsloc (* GCC's "goto *exp" *)
| DEFINITION of definition (*definition or declaration of a variable or type*)
| ASM of attribute list * (* typically only volatile and const *)
string list * (* template *)
asm_details option * (* extra details to guide GCC's optimizer *)
cabsloc
(** MS SEH *)
| TRY_EXCEPT of block * expression * block * cabsloc
| TRY_FINALLY of block * block * cabsloc
and for_clause =
FC_EXP of expression
| FC_DECL of definition
(*
** Expressions
*)
and binary_operator =
ADD | SUB | MUL | DIV | MOD
| AND | OR
| BAND | BOR | XOR | SHL | SHR
| EQ | NE | LT | GT | LE | GE
| ASSIGN
| ADD_ASSIGN | SUB_ASSIGN | MUL_ASSIGN | DIV_ASSIGN | MOD_ASSIGN
| BAND_ASSIGN | BOR_ASSIGN | XOR_ASSIGN | SHL_ASSIGN | SHR_ASSIGN
and unary_operator =
MINUS | PLUS | NOT | BNOT | MEMOF | ADDROF
| PREINCR | PREDECR | POSINCR | POSDECR
and expression =
NOTHING
| UNARY of unary_operator * expression
| LABELADDR of string (* GCC's && Label *)
| BINARY of binary_operator * expression * expression
| QUESTION of expression * expression * expression
(* A CAST can actually be a constructor expression *)
| CAST of (specifier * decl_type) * init_expression
(* There is a special form of CALL in which the function called is
__builtin_va_arg and the second argument is sizeof(T). This
should be printed as just T *)
| CALL of expression * expression list
| COMMA of expression list
| CONSTANT of constant
| PAREN of expression
| VARIABLE of string
| EXPR_SIZEOF of expression
| TYPE_SIZEOF of specifier * decl_type
| EXPR_ALIGNOF of expression
| TYPE_ALIGNOF of specifier * decl_type
| INDEX of expression * expression
| MEMBEROF of expression * string
| MEMBEROFPTR of expression * string
| GNU_BODY of block
and constant =
| CONST_INT of string (* the textual representation *)
| CONST_FLOAT of string (* the textual representaton *)
| CONST_CHAR of int64 list
| CONST_WCHAR of int64 list
| CONST_STRING of string
| CONST_WSTRING of int64 list
(* ww: wstrings are stored as an int64 list at this point because
* we might need to feed the wide characters piece-wise into an
* array initializer (e.g., wchar_t foo[] = L"E\xabcd";). If that
* doesn't happen we will convert it to an (escaped) string before
* passing it to Cil. *)
and init_expression =
| NO_INIT
| SINGLE_INIT of expression
| COMPOUND_INIT of (initwhat * init_expression) list
and initwhat =
NEXT_INIT
| INFIELD_INIT of string * initwhat
| ATINDEX_INIT of expression * initwhat
| ATINDEXRANGE_INIT of expression * expression
(* Each attribute has a name and some
* optional arguments *)
and attribute = string * expression list
|