source: Deliverables/D2.3/8051-memoryspaces-branch/cparser/C.mli @ 460

Last change on this file since 460 was 460, checked in by campbell, 9 years ago

Port memory spaces changes to latest prototype compiler.

File size: 6.5 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
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.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* C abstract syntax after elaboration *)
17
18(* Locations *)
19
20type location = string * int            (* filename, line number *)
21
22(* Identifiers *)
23
24type ident =
25  { name: string;                       (* name as in the source *)
26    stamp: int }                        (* unique ID *)
27
28(* kinds of integers *)
29
30type ikind = 
31  | IBool       (** [_Bool] *)
32  | IChar       (** [char] *)
33  | ISChar      (** [signed char] *)
34  | IUChar      (** [unsigned char] *)
35  | IInt        (** [int] *)
36  | IUInt       (** [unsigned int] *)
37  | IShort      (** [short] *)
38  | IUShort     (** [unsigned short] *)
39  | ILong       (** [long] *)
40  | IULong      (** [unsigned long] *)
41  | ILongLong   (** [long long] (or [_int64] on Microsoft Visual C) *)
42  | IULongLong  (** [unsigned long long] (or [unsigned _int64] on Microsoft
43                    Visual C) *)
44
45(** Kinds of floating-point numbers*)
46
47type fkind = 
48    FFloat      (** [float] *)
49  | FDouble     (** [double] *)
50  | FLongDouble (** [long double] *)
51
52
53(** Constants *)
54
55type constant =
56  | CInt of int64 * ikind * string      (* as it appeared in the source *)
57  | CFloat of float * fkind * string    (* as it appeared in the source *)
58  | CStr of string
59  | CWStr of int64 list
60  | CEnum of ident * int64              (* enum tag, integer value *)
61
62(** Attributes *)
63
64type attribute = AConst | AVolatile | ARestrict
65
66type attributes = attribute list
67
68(** Storage classes *)
69
70type storage =
71  | Storage_default
72  | Storage_extern
73  | Storage_static
74  | Storage_register
75
76(** Unary operators *)
77
78type unary_operator =
79  | Ominus      (* unary "-" *)
80  | Oplus       (* unary "+" *)
81  | Olognot     (* "!" *)
82  | Onot        (* "~" *)
83  | Oderef      (* unary "*" *)
84  | Oaddrof     (* "&" *)
85  | Opreincr    (* "++" prefix *)
86  | Opredecr    (* "--" prefix *)
87  | Opostincr   (* "++" postfix *)
88  | Opostdecr   (* "--" postfix *)
89  | Odot of string (* ".field" *)
90  | Oarrow of string (* "->field" *)
91
92type binary_operator =
93  | Oadd        (* binary "+" *)
94  | Osub        (* binary "-" *)
95  | Omul        (* binary "*" *)
96  | Odiv        (* "/" *)
97  | Omod        (* "%" *)
98  | Oand        (* "&" *)
99  | Oor         (* "|" *)
100  | Oxor        (* "^" *)
101  | Oshl        (* "<<" *)
102  | Oshr        (* ">>" *)
103  | Oeq         (* "==" *)
104  | One         (* "!=" *)
105  | Olt         (* "<" *)
106  | Ogt         (* ">" *)
107  | Ole         (* "<=" *)
108  | Oge         (* ">=" *)
109  | Oindex      (* "a[i]" *)
110  | Oassign     (* "=" *)
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 (* ">>=" *)
121  | Ocomma      (* "," *)
122  | Ologand     (* "&&" *)
123  | Ologor      (* "||" *)
124
125(** Types *)
126
127type memory_space =
128  | Any
129  | Data
130  | IData
131  | PData
132  | XData
133  | Code
134
135type typ =
136  | TVoid of attributes
137  | TInt of ikind * attributes
138  | TFloat of fkind * attributes
139  | TPtr of memory_space * typ * attributes
140  | TArray of memory_space * typ * int64 option * attributes
141  | TFun of typ * (ident * typ) list option * bool * attributes
142  | TNamed of ident * attributes
143  | TStruct of ident * attributes
144  | TUnion of ident * attributes
145
146(** Expressions *)
147
148type exp = { edesc: exp_desc; etyp: typ; espace: memory_space }
149
150and exp_desc =
151  | EConst of constant
152  | ESizeof of typ
153  | EVar of ident
154  | EUnop of unary_operator * exp
155  | EBinop of binary_operator * exp * exp * typ
156                           (* the type at which the operation is performed *)
157  | EConditional of exp * exp * exp
158  | ECast of typ * exp
159  | ECall of exp * exp list
160
161(** Statements *)
162
163type stmt = { sdesc: stmt_desc; sloc: location }
164
165and stmt_desc =
166  | Sskip
167  | Sdo of exp
168  | Sseq of stmt * stmt
169  | Sif of exp * stmt * stmt
170  | Swhile of exp * stmt
171  | Sdowhile of stmt * exp
172  | Sfor of stmt * exp * stmt * stmt
173  | Sbreak
174  | Scontinue
175  | Sswitch of exp * stmt
176  | Slabeled of slabel * stmt
177  | Sgoto of string
178  | Sreturn of exp option
179  | Sblock of stmt list
180  | Sdecl of decl
181
182and slabel = 
183  | Slabel of string
184  | Scase of exp
185  | Sdefault
186
187(** Declarations *)
188
189and decl =
190  storage * ident * typ * init option
191
192(** Initializers *)
193
194and init =
195  | Init_single of exp
196  | Init_array of init list
197  | Init_struct of ident * (field * init) list
198  | Init_union of ident * field * init
199
200(** Struct or union field *)
201
202and field = {
203    fld_name: string;
204    fld_typ: typ;
205    fld_bitfield: int option
206}
207
208type struct_or_union =
209  | Struct
210  | Union
211
212(** Function definitions *)
213
214type fundef = {
215    fd_storage: storage;
216    fd_inline: bool;
217    fd_name: ident;
218    fd_ret: typ; (* return type *)
219    fd_params: (ident * typ) list; (* formal parameters *)
220    fd_vararg: bool;               (* variable arguments? *)
221    fd_locals: decl list;          (* local variables *)
222    fd_body: stmt
223}
224
225(** Global declarations *)
226
227type globdecl =
228  { gdesc: globdecl_desc; gloc: location }
229
230and globdecl_desc =
231  | Gdecl of memory_space * decl  (* variable declaration, function prototype *)
232  | Gfundef of fundef                   (* function definition *)
233  | Gcompositedecl of struct_or_union * ident (* struct/union declaration *)
234  | Gcompositedef of struct_or_union * ident * field list
235                                        (* struct/union definition *)
236  | Gtypedef of ident * typ             (* typedef *)
237  | Genumdef of ident * (ident * exp option) list  (* enum definition *)
238  | Gpragma of string                   (* #pragma directive *)
239
240type program = globdecl list
Note: See TracBrowser for help on using the repository browser.