1 (* *********************************************************************)
3 (* The Compcert verified compiler *)
5 (* Xavier Leroy, INRIA Paris-Rocquencourt *)
7 (* Copyright Institut National de Recherche en Informatique et en *)
8 (* Automatique. All rights reserved. This file is distributed *)
9 (* under the terms of the GNU General Public License as published by *)
10 (* the Free Software Foundation, either version 2 of the License, or *)
11 (* (at your option) any later version. This file is also distributed *)
12 (* under the terms of the INRIA Non-Commercial License Agreement. *)
14 (* *********************************************************************)
16 (* C abstract syntax after elaboration *)
20 type location = string * int (* filename, line number *)
25 { name: string; (* name as in the source *)
26 stamp: int } (* unique ID *)
28 (* kinds of integers *)
31 | IBool (** [_Bool] *)
33 | ISChar (** [signed char] *)
34 | IUChar (** [unsigned char] *)
36 | IUInt (** [unsigned int] *)
37 | IShort (** [short] *)
38 | IUShort (** [unsigned short] *)
40 | IULong (** [unsigned long] *)
41 | ILongLong (** [long long] (or [_int64] on Microsoft Visual C) *)
42 | IULongLong (** [unsigned long long] (or [unsigned _int64] on Microsoft
45 (** Kinds of floating-point numbers*)
49 | FDouble (** [double] *)
50 | FLongDouble (** [long double] *)
56 | CInt of int64 * ikind * string (* as it appeared in the source *)
57 | CFloat of float * fkind * string (* as it appeared in the source *)
60 | CEnum of ident * int64 (* enum tag, integer value *)
64 type attribute = AConst | AVolatile | ARestrict
66 type attributes = attribute list
68 (** Storage classes *)
76 (** Unary operators *)
79 | Ominus (* unary "-" *)
80 | Oplus (* unary "+" *)
83 | Oderef (* unary "*" *)
85 | Opreincr (* "++" prefix *)
86 | Opredecr (* "--" prefix *)
87 | Opostincr (* "++" postfix *)
88 | Opostdecr (* "--" postfix *)
89 | Odot of string (* ".field" *)
90 | Oarrow of string (* "->field" *)
92 type binary_operator =
93 | Oadd (* binary "+" *)
94 | Osub (* binary "-" *)
95 | Omul (* binary "*" *)
109 | Oindex (* "a[i]" *)
111 | Oadd_assign (* "+=" *)
112 | Osub_assign (* "-=" *)
113 | Omul_assign (* "*=" *)
114 | Odiv_assign (* "/=" *)
115 | Omod_assign (* "%=" *)
116 | Oand_assign (* "&=" *)
117 | Oor_assign (* "|=" *)
118 | Oxor_assign (* "^=" *)
119 | Oshl_assign (* "<<=" *)
120 | Oshr_assign (* ">>=" *)
128 | TVoid of attributes
129 | TInt of ikind * attributes
130 | TFloat of fkind * attributes
131 | TPtr of typ * attributes
132 | TArray of typ * int64 option * attributes
133 | TFun of typ * (ident * typ) list option * bool * attributes
134 | TNamed of ident * attributes
135 | TStruct of ident * attributes
136 | TUnion of ident * attributes
140 type exp = { edesc: exp_desc; etyp: typ }
146 | EUnop of unary_operator * exp
147 | EBinop of binary_operator * exp * exp * typ
148 (* the type at which the operation is performed *)
149 | EConditional of exp * exp * exp
151 | ECall of exp * exp list
155 type stmt = { sdesc: stmt_desc; sloc: location }
160 | Sseq of stmt * stmt
161 | Sif of exp * stmt * stmt
162 | Swhile of exp * stmt
163 | Sdowhile of stmt * exp
164 | Sfor of stmt * exp * stmt * stmt
167 | Sswitch of exp * stmt
168 | Slabeled of slabel * stmt
170 | Sreturn of exp option
171 | Sblock of stmt list
182 storage * ident * typ * init option
188 | Init_array of init list
189 | Init_struct of ident * (field * init) list
190 | Init_union of ident * field * init
192 (** Struct or union field *)
197 fld_bitfield: int option
200 type struct_or_union =
204 (** Function definitions *)
210 fd_ret: typ; (* return type *)
211 fd_params: (ident * typ) list; (* formal parameters *)
212 fd_vararg: bool; (* variable arguments? *)
213 fd_locals: decl list; (* local variables *)
217 (** Global declarations *)
220 { gdesc: globdecl_desc; gloc: location }
223 | Gdecl of decl (* variable declaration, function prototype *)
224 | Gfundef of fundef (* function definition *)
225 | Gcompositedecl of struct_or_union * ident (* struct/union declaration *)
226 | Gcompositedef of struct_or_union * ident * field list
227 (* struct/union definition *)
228 | Gtypedef of ident * typ (* typedef *)
229 | Genumdef of ident * (ident * exp option) list (* enum definition *)
230 | Gpragma of string (* #pragma directive *)
232 type program = globdecl list