source: Deliverables/D2.3/8051-memoryspaces-branch/cparser/Elab.ml @ 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: 63.7 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(* Elaboration from Cabs parse tree to C simplified, typed syntax tree *)
17
18open Format
19open Errors
20open Machine
21open Cabs
22open Cabshelper
23open C
24open Cutil
25open Env
26
27(** * Utility functions *)
28
29(* Error reporting  *)
30
31let fatal_error loc fmt =
32  Errors.fatal_error ("%a: Error:@ " ^^ fmt) format_cabsloc loc
33
34let error loc fmt =
35  Errors.error ("%a: Error:@ " ^^ fmt) format_cabsloc loc
36
37let warning loc fmt =
38  Errors.warning ("%a: Warning:@ " ^^ fmt) format_cabsloc loc
39
40(* Error reporting for Env functions *)
41
42let wrap fn loc env arg =
43  try fn env arg
44  with Env.Error msg -> fatal_error loc "%s" (Env.error_message msg)
45
46(* Translation of locations *)
47
48let elab_loc l = (l.filename, l.lineno)
49
50(* Buffering of the result (a list of topdecl *)
51
52let top_declarations = ref ([] : globdecl list)
53
54let emit_elab loc td =
55  top_declarations := { gdesc = td; gloc = loc } :: !top_declarations
56
57let reset() = top_declarations := []
58
59let elaborated_program () =
60  let p = !top_declarations in
61  top_declarations := [];
62  (* Reverse it and eliminate unreferenced declarations *)
63  Cleanup.program p
64
65(* Location stuff *)
66
67let loc_of_name (_, _, _, loc) = loc
68
69let loc_of_namelist = function [] -> cabslu | name :: _ -> loc_of_name name
70
71let loc_of_init_name_list =
72  function [] -> cabslu | (name, init) :: _ -> loc_of_name name
73
74(* Monadic map for functions env -> 'a -> 'b * env *)
75
76let rec mmap f env = function
77  | [] -> ([], env)
78  | hd :: tl ->
79      let (hd', env1) = f env hd in
80      let (tl', env2) = mmap f env1 tl in
81      (hd' :: tl', env2)
82
83(* To detect redefinitions within the same scope *)
84
85let redef fn env arg =
86  try
87    let (id, info) = fn env arg in
88    if Env.in_current_scope env id then Some(id, info) else None
89  with Env.Error _ ->
90    None
91
92(* Forward declarations *)
93
94let elab_expr_f : (cabsloc -> Env.t -> Cabs.expression -> C.exp) ref
95  = ref (fun _ _ _ -> assert false)
96
97let elab_block_f : (cabsloc -> C.typ -> Env.t -> Cabs.block -> C.stmt) ref
98  = ref (fun _ _ _ _ -> assert false)
99
100
101(** * Elaboration of constants *)
102
103let has_suffix s suff = 
104  let ls = String.length s and lsuff = String.length suff in
105  ls >= lsuff && String.sub s (ls - lsuff) lsuff = suff
106
107let chop_last s n =
108  assert (String.length s >= n);
109  String.sub s 0 (String.length s - n)
110
111let has_prefix s pref = 
112  let ls = String.length s and lpref = String.length pref in
113  ls >= lpref && String.sub s 0 lpref = pref
114
115let chop_first s n =
116  assert (String.length s >= n);
117  String.sub s n (String.length s - n)
118
119exception Overflow
120exception Bad_digit
121
122let parse_int base s =
123  let max_val = (* (2^64-1) / base, unsigned *)
124    match base with
125    |  8 -> 2305843009213693951L
126    | 10 -> 1844674407370955161L
127    | 16 -> 1152921504606846975L
128    |  _ -> assert false in
129  let v = ref 0L in
130  for i = 0 to String.length s - 1 do
131    if !v > max_val then raise Overflow;
132    v := Int64.mul !v (Int64.of_int base);
133    let c = s.[i] in
134    let digit =
135      if c >= '0' && c <= '9' then Char.code c - 48
136      else if c >= 'A' && c <= 'F' then Char.code c - 55
137      else raise Bad_digit in
138    if digit >= base then raise Bad_digit;
139    v := Int64.add !v (Int64.of_int digit)
140  done;
141  !v
142
143let integer_representable v ik =
144  let bitsize = sizeof_ikind ik * 8
145  and signed = is_signed_ikind ik in
146  if bitsize >= 64 then
147    (not signed) || (v >= 0L && v <= 0x7FFF_FFFF_FFFF_FFFFL)
148  else if not signed then
149    v >= 0L && v < Int64.shift_left 1L bitsize
150  else
151    v >= 0L && v < Int64.shift_left 1L (bitsize - 1)
152
153let elab_int_constant loc s0 =
154  let s = String.uppercase s0 in
155  (* Determine possible types and chop type suffix *)
156  let (s, dec_kinds, hex_kinds) =
157    if has_suffix s "ULL" || has_suffix s "LLU" then
158      (chop_last s 3, [IULongLong], [IULongLong])
159    else if has_suffix s "LL" then
160      (chop_last s 2, [ILongLong], [ILongLong; IULongLong])
161    else if has_suffix s "UL" || has_suffix s "LU" then
162      (chop_last s 2, [IULong; IULongLong], [IULong; IULongLong])
163    else if has_suffix s "L" then
164      (chop_last s 1, [ILong; ILongLong],
165                      [ILong; IULong; ILongLong; IULongLong])
166    else if has_suffix s "U" then
167      (chop_last s 1, [IUInt; IULong; IULongLong],
168                      [IUInt; IULong; IULongLong])
169    else
170      (s, [IInt; ILong; IULong; ILongLong],
171          [IInt; IUInt; ILong; IULong; ILongLong; IULongLong])
172  in
173  (* Determine base *)
174  let (s, base) =
175    if has_prefix s "0X" then
176      (chop_first s 2, 16)
177    else if has_prefix s "0" then
178      (chop_first s 1, 8)
179    else
180      (s, 10)
181  in
182  (* Parse digits *)
183  let v =
184    try parse_int base s
185    with
186    | Overflow ->
187        error loc "integer literal '%s' is too large" s0;
188        0L
189    | Bad_digit ->
190        error loc "bad digit in integer literal '%s'" s0;
191        0L
192  in
193  (* Find smallest allowable type that fits *)
194  let ty =
195    try List.find (fun ty -> integer_representable v ty) 
196                  (if base = 10 then dec_kinds else hex_kinds)
197    with Not_found ->
198      error loc "integer literal '%s' cannot be represented" s0;
199      IInt
200  in
201  (v, ty)
202
203let elab_float_constant loc s0 =
204  let s = String.uppercase s0 in
205  (* Determine type and chop suffix *)
206  let (s, ty) =
207    if has_suffix s "L" then
208      (chop_last s 1, FLongDouble)
209    else if has_suffix s "F" then
210      (chop_last s 1, FFloat)
211    else
212      (s, FDouble) in
213  (* Convert to Caml float - XXX loss of precision for long double *)
214  let v =
215    try float_of_string s
216    with Failure _ -> error loc "bad float literal '%s'" s0; 0.0 in
217  (v, ty)
218
219let elab_char_constant loc sz cl =
220  let nbits = 8 * sz in
221  (* Treat multi-char constants as a number in base 2^nbits *)
222  let max_val = Int64.shift_left 1L (64 - nbits) in
223  let v =
224    List.fold_left
225      (fun acc d ->
226        if acc >= max_val then begin
227          error loc "character literal overflows";
228        end;
229        Int64.add (Int64.shift_left acc nbits) d)
230      0L cl in
231  let ty =
232    if v < 256L then IInt
233    else if v < Int64.shift_left 1L (8 * sizeof_ikind IULong) then IULong
234    else IULongLong in
235  (v, ty)
236
237let elab_constant loc = function
238  | CONST_INT s ->
239      let (v, ik) = elab_int_constant loc s in
240      CInt(v, ik, s)
241  | CONST_FLOAT s ->
242      let (v, fk) = elab_float_constant loc s in
243      CFloat(v, fk, s)
244  | CONST_CHAR cl ->
245      let (v, ik) = elab_char_constant loc 1 cl in
246      CInt(v, ik, "")
247  | CONST_WCHAR cl -> 
248      let (v, ik) = elab_char_constant loc !config.sizeof_wchar cl in
249      CInt(v, ik, "")
250  | CONST_STRING s -> CStr s
251  | CONST_WSTRING s -> CWStr s
252
253
254(** * Elaboration of type expressions, type specifiers, name declarations *)
255
256(* Elaboration of attributes *)
257
258let elab_attribute loc = function
259  | ("const", []) -> Some AConst
260  | ("restrict", []) -> Some ARestrict
261  | ("volatile", []) -> Some AVolatile
262  | (name, args) -> 
263      (* warning loc "ignoring '%s' attribute" name; *)
264      None
265
266let rec elab_attributes loc = function
267  | [] -> []
268  | a1 :: al ->
269      match elab_attribute loc a1 with
270      | None -> elab_attributes loc al
271      | Some a -> add_attributes [a] (elab_attributes loc al)
272
273let elab_attribute_space = function
274  | ("data", []) -> Some Data
275  | ("idata", []) -> Some IData
276  | ("pdata", []) -> Some PData
277  | ("xdata", []) -> Some XData
278  | ("code", []) -> Some Code
279  | _ -> None
280
281let rec elab_attributes_space loc attrs =
282  let rec aux = function
283    | [] -> None
284    | h::t -> (match elab_attribute_space h with
285                | None -> aux t
286                | Some v -> Some (v,t))
287  in match aux attrs with
288    | None -> Any
289    | Some (space, rest) ->
290       (match aux rest with 
291         | None -> ()
292         | Some _ -> warning loc "Multiple memory spaces given");
293       space
294
295(* Auxiliary for typespec elaboration *)
296
297let typespec_rank = function (* Don't change this *)
298  | Cabs.Tvoid -> 0
299  | Cabs.Tsigned -> 1
300  | Cabs.Tunsigned -> 2
301  | Cabs.Tchar -> 3
302  | Cabs.Tshort -> 4
303  | Cabs.Tlong -> 5
304  | Cabs.Tint -> 6
305  | Cabs.Tint64 -> 7
306  | Cabs.Tfloat -> 8
307  | Cabs.Tdouble -> 9
308  | Cabs.T_Bool -> 10
309  | _ -> 11 (* There should be at most one of the others *)
310
311let typespec_order t1 t2 = compare (typespec_rank t1) (typespec_rank t2)
312
313
314(* Elaboration of a type specifier.  Returns 4-tuple:
315     (storage class, "inline" flag, elaborated type, new env)
316   Optional argument "only" is true if this is a standalone
317   struct or union declaration, without variable names.
318*)
319
320let rec elab_specifier ?(only = false) loc env specifier =
321  (* We first divide the parts of the specifier as follows:
322       - a storage class
323       - a set of attributes (const, volatile, restrict)
324       - a list of type specifiers *)
325  let sto = ref Storage_default
326  and inline = ref false
327  and attr = ref []
328  and tyspecs = ref []
329  and space = ref Any in
330
331  let do_specifier = function
332  | SpecTypedef -> ()
333  | SpecCV cv ->
334      let a =
335        match cv with
336        | CV_CONST -> AConst
337        | CV_VOLATILE -> AVolatile
338        | CV_RESTRICT -> ARestrict in
339      attr := add_attributes [a] !attr
340  | SpecAttr a ->
341      attr := add_attributes (elab_attributes loc [a]) !attr;
342      (match elab_attribute_space a with
343        | None -> ()
344        | Some sp ->
345           if !space <> Any then
346             error loc "multiple memory space specifiers";
347           space := sp)
348  | SpecStorage st ->
349      if !sto <> Storage_default then
350        error loc "multiple storage specifiers";
351      begin match st with
352      | NO_STORAGE -> ()
353      | AUTO -> ()
354      | STATIC -> sto := Storage_static
355      | EXTERN -> sto := Storage_extern
356      | REGISTER -> sto := Storage_register
357      end
358  | SpecInline -> inline := true
359  | SpecType tys -> tyspecs := tys :: !tyspecs in
360
361  List.iter do_specifier specifier;
362
363  let simple ty = (!space, !sto, !inline, add_attributes_type !attr ty, env) in
364
365  (* Now interpret the list of type specifiers.  Much of this code
366     is stolen from CIL. *)
367  match List.stable_sort typespec_order (List.rev !tyspecs) with
368    | [Cabs.Tvoid] -> simple (TVoid [])
369
370    | [Cabs.T_Bool] -> simple (TInt(IBool, []))
371    | [Cabs.Tchar] -> simple (TInt(IChar, []))
372    | [Cabs.Tsigned; Cabs.Tchar] -> simple (TInt(ISChar, []))
373    | [Cabs.Tunsigned; Cabs.Tchar] -> simple (TInt(IUChar, []))
374
375    | [Cabs.Tshort] -> simple (TInt(IShort, []))
376    | [Cabs.Tsigned; Cabs.Tshort] -> simple (TInt(IShort, []))
377    | [Cabs.Tshort; Cabs.Tint] -> simple (TInt(IShort, []))
378    | [Cabs.Tsigned; Cabs.Tshort; Cabs.Tint] -> simple (TInt(IShort, []))
379
380    | [Cabs.Tunsigned; Cabs.Tshort] -> simple (TInt(IUShort, []))
381    | [Cabs.Tunsigned; Cabs.Tshort; Cabs.Tint] -> simple (TInt(IUShort, []))
382
383    | [] -> simple (TInt(IInt, []))
384    | [Cabs.Tint] -> simple (TInt(IInt, []))
385    | [Cabs.Tsigned] -> simple (TInt(IInt, []))
386    | [Cabs.Tsigned; Cabs.Tint] -> simple (TInt(IInt, []))
387
388    | [Cabs.Tunsigned] -> simple (TInt(IUInt, []))
389    | [Cabs.Tunsigned; Cabs.Tint] -> simple (TInt(IUInt, []))
390
391    | [Cabs.Tlong] -> simple (TInt(ILong, []))
392    | [Cabs.Tsigned; Cabs.Tlong] -> simple (TInt(ILong, []))
393    | [Cabs.Tlong; Cabs.Tint] -> simple (TInt(ILong, []))
394    | [Cabs.Tsigned; Cabs.Tlong; Cabs.Tint] -> simple (TInt(ILong, []))
395
396    | [Cabs.Tunsigned; Cabs.Tlong] -> simple (TInt(IULong, []))
397    | [Cabs.Tunsigned; Cabs.Tlong; Cabs.Tint] -> simple (TInt(IULong, []))
398
399    | [Cabs.Tlong; Cabs.Tlong] -> simple (TInt(ILongLong, []))
400    | [Cabs.Tsigned; Cabs.Tlong; Cabs.Tlong] -> simple (TInt(ILongLong, []))
401    | [Cabs.Tlong; Cabs.Tlong; Cabs.Tint] -> simple (TInt(ILongLong, []))
402    | [Cabs.Tsigned; Cabs.Tlong; Cabs.Tlong; Cabs.Tint] -> simple (TInt(ILongLong, []))
403
404    | [Cabs.Tunsigned; Cabs.Tlong; Cabs.Tlong] -> simple (TInt(IULongLong, []))
405    | [Cabs.Tunsigned; Cabs.Tlong; Cabs.Tlong; Cabs.Tint] -> simple (TInt(IULongLong, []))
406
407    (* int64 is a MSVC extension *)
408    | [Cabs.Tint64] -> simple (TInt(ILongLong, []))
409    | [Cabs.Tsigned; Cabs.Tint64] -> simple (TInt(ILongLong, []))
410    | [Cabs.Tunsigned; Cabs.Tint64] -> simple (TInt(IULongLong, []))
411
412    | [Cabs.Tfloat] -> simple (TFloat(FFloat, []))
413    | [Cabs.Tdouble] -> simple (TFloat(FDouble, []))
414
415    | [Cabs.Tlong; Cabs.Tdouble] -> simple (TFloat(FLongDouble, []))
416
417    (* Now the other type specifiers *)
418
419    | [Cabs.Tnamed id] ->
420        let (id', info) = wrap Env.lookup_typedef loc env id in
421        simple (TNamed(id', []))
422
423    | [Cabs.Tstruct(id, optmembers, a)] ->
424        let (id', env') =
425          elab_struct_or_union only Struct loc id optmembers env in
426        let attr' = add_attributes !attr (elab_attributes loc a) in
427        (!space, !sto, !inline, TStruct(id', attr'), env')
428
429    | [Cabs.Tunion(id, optmembers, a)] ->
430        let (id', env') =
431          elab_struct_or_union only Union loc id optmembers env in
432        let attr' = add_attributes !attr (elab_attributes loc a) in
433        (!space, !sto, !inline, TUnion(id', attr'), env')
434
435    | [Cabs.Tenum(id, optmembers, a)] ->
436        let env' = 
437          elab_enum loc id optmembers env in
438        let attr' = add_attributes !attr (elab_attributes loc a) in
439        (!space, !sto, !inline, TInt(enum_ikind, attr'), env')
440
441    | [Cabs.TtypeofE _] ->
442        fatal_error loc "GCC __typeof__ not supported"
443    | [Cabs.TtypeofT _] ->
444        fatal_error loc "GCC __typeof__ not supported"
445
446    (* Specifier doesn't make sense *)
447    | _ ->
448        fatal_error loc "illegal combination of type specifiers"
449
450(* Elaboration of a type declarator.  *)
451
452and elab_type_declarator loc env space ty = function
453  | Cabs.JUSTBASE ->
454      (space, ty, env)
455  | Cabs.PARENTYPE(attr1, d, attr2) ->
456      (* XXX ignoring the distinction between attrs after and before *)
457      let a = elab_attributes loc (attr1 @ attr2) in
458      (* XXX ought to use space from attrs? *)
459      elab_type_declarator loc env space (add_attributes_type a ty) d
460  | Cabs.ARRAY(d, attr, sz) ->
461      let a = elab_attributes loc attr in
462      let sz' =
463        match sz with
464        | Cabs.NOTHING ->
465            None
466        | _ ->
467            match Ceval.integer_expr env (!elab_expr_f loc env sz) with
468            | Some n ->
469                if n < 0L then error loc "array size is negative";
470                Some n
471            | None ->
472                error loc "array size is not a compile-time constant";
473                Some 1L in (* produces better error messages later *)
474       elab_type_declarator loc env space (TArray(space, ty, sz', a)) d
475  | Cabs.PTR(attr, d) ->
476      let a = elab_attributes loc attr in
477      let space' = elab_attributes_space loc attr in
478       elab_type_declarator loc env space' (TPtr(space, ty, a)) d
479  | Cabs.PROTO(d, params, vararg) ->
480       begin match unroll env ty with
481       | TArray _ | TFun _ ->
482           error loc "illegal function return type@ %a" Cprint.typ ty
483       | _ -> ()
484       end;
485       let params' = elab_parameters env params in
486       elab_type_declarator loc env space (TFun(ty, params', vararg, [])) d
487
488(* Elaboration of parameters in a prototype *)
489
490and elab_parameters env params =
491  match params with
492  | [] -> (* old-style K&R prototype *)
493      None
494  | _ ->
495      (* Prototype introduces a new scope *)
496      let (vars, _) = mmap elab_parameter (Env.new_scope env) params in
497      (* Catch special case f(void) *)
498      match vars with
499        | [ ( {name=""}, TVoid _) ] -> Some []
500        | _ -> Some vars
501
502(* Elaboration of a function parameter *)
503
504and elab_parameter env (spec, name) =
505  let (id, sto, inl, ty, env1) = elab_name env spec name in
506  if sto <> Storage_default && sto <> Storage_register then
507    error (loc_of_name name)
508      "'extern' or 'static' storage not supported for function parameter";
509  (* replace array and function types by pointer types *)
510  let ty1 = argument_conversion env1 ty in
511  let (id', env2) = Env.enter_ident env1 id sto ty1 Any (* stack *) in
512  ( (id', ty1) , env2 )
513
514(* Elaboration of a (specifier, Cabs "name") pair *)
515
516and elab_name env spec (id, decl, attr, loc) =
517  let (space, sto, inl, bty, env') = elab_specifier loc env spec in
518  let (_, ty, env'') = elab_type_declarator loc env' space bty decl in 
519  let a = elab_attributes loc attr in
520  (id, sto, inl, add_attributes_type a ty, env'')
521
522(* Elaboration of a name group *)
523
524and elab_name_group env (spec, namelist) =
525  let (space, sto, inl, bty, env') =
526    elab_specifier (loc_of_namelist namelist) env spec in
527  let elab_one_name env (id, decl, attr, loc) =
528    let (_, ty, env1) =
529      elab_type_declarator loc env space bty decl in 
530    let a = elab_attributes loc attr in
531    ((id, sto, add_attributes_type a ty), env1) in
532  mmap elab_one_name env' namelist
533
534(* Elaboration of an init-name group *)
535
536and elab_init_name_group env (spec, namelist) =
537  let (space, sto, inl, bty, env') =
538    elab_specifier (loc_of_init_name_list namelist) env spec in
539  let elab_one_name env ((id, decl, attr, loc), init) =
540    let (space', ty, env1) =
541      elab_type_declarator loc env space bty decl in 
542    let a = elab_attributes loc attr in
543    ((space', id, sto, add_attributes_type a ty, init), env1) in
544  mmap elab_one_name env' namelist
545
546(* Elaboration of a field group *)
547
548and elab_field_group env (spec, fieldlist) =
549  let (names, env') =
550    elab_name_group env (spec, List.map fst fieldlist) in
551
552  let elab_bitfield ((_, _, _, loc), optbitsize) (id, sto, ty) =
553    if sto <> Storage_default then
554      error loc "member '%s' has non-default storage" id;
555    let optbitsize' =
556      match optbitsize with
557      | None -> None
558      | Some sz ->
559          let ik =
560            match unroll env' ty with
561            | TInt(ik, _) -> ik
562            | _ -> ILongLong (* trigger next error message *) in
563          if integer_rank ik > integer_rank IInt then
564              error loc
565                "the type of a bit field must be an integer type \
566                 no bigger than 'int'";
567          match Ceval.integer_expr env' (!elab_expr_f loc env sz) with
568          | Some n ->
569              if n < 0L then begin
570                error loc "bit size of member (%Ld) is negative" n;
571                None
572              end else
573              if n > Int64.of_int(sizeof_ikind ik * 8) then begin
574                error loc "bit size of member (%Ld) is too large" n;
575                None
576              end else
577                Some(Int64.to_int n)
578          | None ->
579              error loc "bit size of member is not a compile-time constant";
580              None in
581    { fld_name = id; fld_typ = ty; fld_bitfield = optbitsize' } 
582  in
583  (List.map2 elab_bitfield fieldlist names, env')
584
585(* Elaboration of a struct or union *)
586
587and elab_struct_or_union_info kind loc env members =
588  let (m, env') = mmap elab_field_group env members in
589  let m = List.flatten m in
590  (* Check for incomplete types *)
591  let rec check_incomplete = function
592  | [] -> ()
593  | [ { fld_typ = TArray(_, ty_elt, None, _) } ] when kind = Struct -> ()
594        (* C99: ty[] allowed as last field of a struct *)
595  | fld :: rem ->
596      if incomplete_type env' fld.fld_typ then
597        error loc "member '%s' has incomplete type" fld.fld_name;
598      check_incomplete rem in
599  check_incomplete m;
600  (composite_info_def env' kind m, env')
601
602(* Elaboration of a struct or union *)
603
604and elab_struct_or_union only kind loc tag optmembers env =
605  let optbinding =
606    if tag = "" then None else Env.lookup_composite env tag in
607  match optbinding, optmembers with
608  | Some(tag', ci), None
609    when (not only) || Env.in_current_scope env tag' ->
610      (* Reference to an already declared struct or union.
611         Special case: if this is an "only" declaration (without variable names)
612         and the composite was bound in another scope,
613         create a new incomplete composite instead via the case
614         "_, None" below. *)
615      (tag', env)
616  | Some(tag', ({ci_sizeof = None} as ci)), Some members
617    when Env.in_current_scope env tag' ->
618      if ci.ci_kind <> kind then
619        error loc "struct/union mismatch on tag '%s'" tag;
620      (* finishing the definition of an incomplete struct or union *)
621      let (ci', env') = elab_struct_or_union_info kind loc env members in
622      (* Emit a global definition for it *)
623      emit_elab (elab_loc loc)
624                (Gcompositedef(kind, tag', ci'.ci_members));
625      (* Replace infos but keep same ident *)
626      (tag', Env.add_composite env' tag' ci')
627  | Some(tag', {ci_sizeof = Some _}), Some _
628    when Env.in_current_scope env tag' ->
629      error loc "redefinition of struct or union '%s'" tag;
630      (tag', env)
631  | _, None ->
632      (* declaration of an incomplete struct or union *)
633      if tag = "" then
634        error loc "anonymous, incomplete struct or union";
635      let ci = composite_info_decl env kind in
636      (* enter it with a new name *)
637      let (tag', env') = Env.enter_composite env tag ci in
638      (* emit it *)
639      emit_elab (elab_loc loc)
640                (Gcompositedecl(kind, tag'));
641      (tag', env')
642  | _, Some members ->
643      (* definition of a complete struct or union *)
644      let ci1 = composite_info_decl env kind in
645      (* enter it, incomplete, with a new name *)
646      let (tag', env') = Env.enter_composite env tag ci1 in
647      (* emit a declaration so that inner structs and unions can refer to it *)
648      emit_elab (elab_loc loc)
649                (Gcompositedecl(kind, tag'));
650      (* elaborate the members *)
651      let (ci2, env'') = elab_struct_or_union_info kind loc env' members in
652      (* emit a definition *)
653      emit_elab (elab_loc loc)
654                (Gcompositedef(kind, tag', ci2.ci_members));
655      (* Replace infos but keep same ident *)
656      (tag', Env.add_composite env'' tag' ci2)
657
658(* Elaboration of an enum item *)
659
660and elab_enum_item env (s, exp, loc) nextval =
661  let (v, exp') =
662    match exp with
663    | NOTHING ->
664        (nextval, None)
665    | _ ->
666        let exp' = !elab_expr_f loc env exp in
667        match Ceval.integer_expr env exp' with
668        | Some n -> (n, Some exp')
669        | None ->
670            error loc
671              "value of enumerator '%s' is not a compile-time constant" s;
672            (nextval, Some exp') in
673  if redef Env.lookup_ident env s <> None then
674    error loc "redefinition of enumerator '%s'" s;
675  let (id, env') = Env.enter_enum_item env s v in
676  ((id, exp'), Int64.succ v, env')
677
678(* Elaboration of an enumeration declaration *)
679
680and elab_enum loc tag optmembers env =
681  match optmembers with
682  | None -> env
683  | Some members ->
684      let rec elab_members env nextval = function
685      | [] -> ([], env)
686      | hd :: tl ->
687          let (dcl1, nextval1, env1) = elab_enum_item env hd nextval in
688          let (dcl2, env2) = elab_members env1 nextval1 tl in
689          (dcl1 :: dcl2, env2) in
690      let (dcls, env') = elab_members env 0L members in
691      let tag' = Env.fresh_ident tag in
692      emit_elab (elab_loc loc) (Genumdef(tag', dcls));
693      env'
694
695(* Elaboration of a naked type, e.g. in a cast *)
696
697let elab_type loc env spec decl =
698  let (space, sto, inl, bty, env') = elab_specifier loc env spec in
699  let (_, ty, env'') = elab_type_declarator loc env' space bty decl in 
700  if sto <> Storage_default || inl then
701    error loc "'extern', 'static', 'register' and 'inline' are meaningless in cast";
702  ty
703
704
705let join_spaces s1 s2 =
706if s1 = s2 then s1 else Any
707
708
709(* Elaboration of expressions *)
710
711let elab_expr loc env a =
712
713  let err fmt = error loc fmt in  (* non-fatal error *)
714  let error fmt = fatal_error loc fmt in
715  let warning fmt = warning loc fmt in
716
717  let rec elab = function
718
719  | NOTHING ->
720      error "empty expression"
721
722(* 7.3 Primary expressions *)
723
724  | VARIABLE s ->
725      begin match wrap Env.lookup_ident loc env s with
726      | (id, II_ident(sto, ty, spc)) ->
727          { edesc = EVar id; etyp = ty; espace=spc }
728      | (id, II_enum v) ->
729          { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []); espace = Code }
730      end
731
732  | CONSTANT cst ->
733      let cst' = elab_constant loc cst in
734      { edesc = EConst cst'; etyp = type_of_constant cst'; espace = Code }
735
736  | PAREN e ->
737      elab e
738
739(* 7.4 Postfix expressions *)
740
741  | INDEX(a1, a2) ->            (* e1[e2] *)
742      let b1 = elab a1 in let b2 = elab a2 in
743      let space, tres =
744        match (unroll env b1.etyp, unroll env b2.etyp) with
745        | (TPtr(space, t, _) | TArray(space, t, _, _)), TInt _ -> space, t
746        | TInt _, (TPtr(space, t, _) | TArray(space, t, _, _)) -> space, t
747        | t1, t2 -> error "incorrect types for array subscripting" in
748      { edesc = EBinop(Oindex, b1, b2, TPtr(space, tres, [])); etyp = tres; espace = space }
749
750  | MEMBEROF(a1, fieldname) ->
751      let b1 = elab a1 in
752      let (fld, attrs) =
753        match unroll env b1.etyp with
754        | TStruct(id, attrs) ->
755            (wrap Env.find_struct_member loc env (id, fieldname), attrs)
756        | TUnion(id, attrs) ->
757            (wrap Env.find_union_member loc env (id, fieldname), attrs)
758        | _ ->
759            error "left-hand side of '.' is not a struct or union" in
760      (* A field of a const/volatile struct or union is itself const/volatile *)
761      { edesc = EUnop(Odot fieldname, b1);
762        etyp = add_attributes_type attrs fld.fld_typ;
763        espace = b1.espace }
764
765  | MEMBEROFPTR(a1, fieldname) ->
766      let b1 = elab a1 in
767      let (space, fld, attrs) =
768        match unroll env b1.etyp with
769        | TPtr(space, t, _) ->
770            begin match unroll env t with
771            | TStruct(id, attrs) ->
772                (space, wrap Env.find_struct_member loc env (id, fieldname), attrs)
773            | TUnion(id, attrs) ->
774                (space, wrap Env.find_union_member loc env (id, fieldname), attrs)
775            | _ ->
776                error "left-hand side of '->' is not a pointer to a struct or union"
777            end
778        | _ ->
779            error "left-hand side of '->' is not a pointer " in
780      { edesc = EUnop(Oarrow fieldname, b1);
781        etyp = add_attributes_type attrs fld.fld_typ;
782        espace = space }
783
784(* Hack to treat vararg.h functions the GCC way.  Helps with testing.
785    va_start(ap,n)
786      (preprocessing) --> __builtin_va_start(ap, arg)
787      (elaboration)   --> __builtin_va_start(ap, &arg)
788    va_arg(ap, ty)
789      (preprocessing) --> __builtin_va_arg(ap, ty)
790      (parsing)       --> __builtin_va_arg(ap, sizeof(ty))
791*)
792  | CALL((VARIABLE "__builtin_va_start" as a1), [a2; a3]) ->
793      let b1 = elab a1 and b2 = elab a2 and b3 = elab a3 in
794      { edesc = ECall(b1, [b2; {edesc = EUnop(Oaddrof, b3);
795                                etyp = TPtr(b3.espace, b3.etyp, []);
796                                espace = Any }]);
797        etyp = TVoid [];
798        espace = Any (* XXX ? *) }
799  | CALL((VARIABLE "__builtin_va_arg" as a1),
800         [a2; (TYPE_SIZEOF _) as a3]) ->
801      let b1 = elab a1 and b2 = elab a2 and b3 = elab a3 in
802      let ty = match b3.edesc with ESizeof ty -> ty | _ -> assert false in
803      { edesc = ECall(b1, [b2; b3]); etyp = ty; espace = Any (* XXX ? *) }
804
805  | CALL(a1, al) ->
806      let b1 =
807        (* Catch the old-style usage of calling a function without
808           having declared it *)
809        match a1 with
810        | VARIABLE n when not (Env.ident_is_bound env n) ->
811            let ty = TFun(TInt(IInt, []), None, false, []) in
812            (* Emit an extern declaration for it *)
813            let id = Env.fresh_ident n in
814            emit_elab (elab_loc loc) (Gdecl(Code, (Storage_extern, id, ty, None)));
815            { edesc = EVar id; etyp = ty; espace = Any }
816        | _ -> elab a1 in
817      let bl = List.map elab al in
818      (* Extract type information *)
819      let (res, args, vararg) =
820        match unroll env b1.etyp with
821        | TFun(res, args, vararg, a) -> (res, args, vararg)
822        | TPtr(_, ty, a) ->
823            begin match unroll env ty with
824            | TFun(res, args, vararg, a) -> (res, args, vararg)
825            | _ -> error "the function part of a call does not have a function type"
826            end
827        | _ -> error "the function part of a call does not have a function type"
828      in
829      (* Type-check the arguments against the prototype *)
830      let bl' =
831        match args with
832        | None -> bl
833        | Some proto -> elab_arguments 1 bl proto vararg in
834      { edesc = ECall(b1, bl'); etyp = res; espace = Any (* Stack *) }
835
836  | UNARY(POSINCR, a1) ->
837      elab_pre_post_incr_decr Opostincr "postfix '++'" a1
838  | UNARY(POSDECR, a1) ->
839      elab_pre_post_incr_decr Opostdecr "postfix '--'" a1
840
841(* 7.5 Unary expressions *)
842
843  | CAST ((spec, dcl), SINGLE_INIT a1) ->
844      let ty = elab_type loc env spec dcl in
845      let b1 = elab a1 in
846      if not (valid_cast env b1.etyp ty) then
847        err "illegal cast from %a@ to %a" Cprint.typ b1.etyp Cprint.typ ty;
848      { edesc = ECast(ty, b1); etyp = ty; espace = b1.espace }
849
850  | CAST ((spec, dcl), _) ->
851      error "cast of initializer expression is not supported"
852
853  | EXPR_SIZEOF(CONSTANT(CONST_STRING s)) ->
854      let cst = CInt(Int64.of_int (String.length s), size_t_ikind, "") in
855      { edesc = EConst cst; etyp = type_of_constant cst; espace = Code }
856
857  | EXPR_SIZEOF a1 ->
858      let b1 = elab a1 in
859      if sizeof env b1.etyp = None then
860        err "incomplete type %a" Cprint.typ b1.etyp;
861      { edesc = ESizeof b1.etyp; etyp = TInt(size_t_ikind, []); espace = Code }
862
863  | TYPE_SIZEOF (spec, dcl) ->
864      let ty = elab_type loc env spec dcl in
865      if sizeof env ty = None then
866        err "incomplete type %a" Cprint.typ ty;
867      { edesc = ESizeof ty; etyp = TInt(size_t_ikind, []); espace = Code }
868
869  | UNARY(PLUS, a1) ->
870      let b1 = elab a1 in
871      if not (is_arith_type env b1.etyp) then
872        error "argument of unary '+' is not an arithmetic type";
873      { edesc = EUnop(Oplus, b1); etyp = unary_conversion env b1.etyp; espace = Any }
874
875  | UNARY(MINUS, a1) ->
876      let b1 = elab a1 in
877      if not (is_arith_type env b1.etyp) then
878        error "argument of unary '-' is not an arithmetic type";
879      { edesc = EUnop(Ominus, b1); etyp = unary_conversion env b1.etyp; espace = Any }
880
881  | UNARY(BNOT, a1) ->
882      let b1 = elab a1 in
883      if not (is_integer_type env b1.etyp) then
884        error "argument of '~' is not an integer type";
885      { edesc = EUnop(Onot, b1); etyp = unary_conversion env b1.etyp; espace = Any }
886
887  | UNARY(NOT, a1) ->
888      let b1 = elab a1 in
889      if not (is_scalar_type env b1.etyp) then
890        error "argument of '!' is not a scalar type";
891      { edesc = EUnop(Olognot, b1); etyp = TInt(IInt, []); espace = Any }
892
893  | UNARY(ADDROF, a1) ->
894      let b1 = elab a1 in
895      begin match unroll env b1.etyp with
896      | TArray _ | TFun _ -> ()
897      | _ -> 
898        if not (is_lvalue env b1) then err "argument of '&' is not a l-value"
899      end;
900      { edesc = EUnop(Oaddrof, b1); etyp = TPtr(b1.espace, b1.etyp, []); espace = Any }
901
902  | UNARY(MEMOF, a1) ->
903      let b1 = elab a1 in
904      begin match unroll env b1.etyp with
905      (* '*' applied to a function type has no effect *)
906      | TFun _ -> b1
907      | TPtr(space, ty, _) | TArray(space, ty, _, _) ->
908          { edesc = EUnop(Oderef, b1); etyp = ty; espace = space }
909      | _ ->
910          error "argument of unary '*' is not a pointer"
911      end
912
913  | UNARY(PREINCR, a1) ->
914      elab_pre_post_incr_decr Opreincr "prefix '++'" a1
915  | UNARY(PREDECR, a1) ->
916      elab_pre_post_incr_decr Opredecr "prefix '--'" a1
917
918(* 7.6 Binary operator expressions *)
919
920  | BINARY(MUL, a1, a2) ->
921      elab_binary_arithmetic "*" Omul a1 a2
922
923  | BINARY(DIV, a1, a2) ->
924      elab_binary_arithmetic "/" Odiv a1 a2
925
926  | BINARY(MOD, a1, a2) ->
927      elab_binary_integer "/" Omod a1 a2
928
929  | BINARY(ADD, a1, a2) ->
930      let b1 = elab a1 in
931      let b2 = elab a2 in
932      let tyres =
933        if is_arith_type env b1.etyp && is_arith_type env b2.etyp then
934          binary_conversion env b1.etyp b2.etyp
935        else begin
936          let (space, ty, attr) =
937            match unroll env b1.etyp, unroll env b2.etyp with
938            | (TPtr(space, ty, a) | TArray(space, ty, _, a)), TInt _ -> (space, ty, a)
939            | TInt _, (TPtr(space, ty, a) | TArray(space, ty, _, a)) -> (space, ty, a)
940            | _, _ -> error "type error in binary '+'" in
941          if not (pointer_arithmetic_ok env ty) then
942            err "illegal pointer arithmetic in binary '+'";
943          TPtr(space, ty, attr)
944        end in
945      { edesc = EBinop(Oadd, b1, b2, tyres); etyp = tyres; espace = Any }
946
947  | BINARY(SUB, a1, a2) ->
948      let b1 = elab a1 in
949      let b2 = elab a2 in
950      let (tyop, tyres) =
951        if is_arith_type env b1.etyp && is_arith_type env b2.etyp then begin
952          let tyres = binary_conversion env b1.etyp b2.etyp in
953          (tyres, tyres)
954        end else begin
955          match unroll env b1.etyp, unroll env b2.etyp with
956          | (TPtr(space, ty, a) | TArray(space, ty, _, a)), TInt _ ->
957              if not (pointer_arithmetic_ok env ty) then
958                err "illegal pointer arithmetic in binary '-'";
959              (TPtr(space, ty, a), TPtr(space, ty, a))
960          | TInt _, (TPtr(space, ty, a) | TArray(space, ty, _, a)) ->
961              if not (pointer_arithmetic_ok env ty) then
962                err "illegal pointer arithmetic in binary '-'";
963              (TPtr(space, ty, a), TPtr(space, ty, a))
964          | (TPtr(space1, ty1, a1) | TArray(space1, ty1, _, a1)),
965            (TPtr(space2, ty2, a2) | TArray(space2, ty2, _, a2)) ->
966(* TODO: automatic cast on space mismatch? *)
967              if not (compatible_types ~noattrs:true env ty1 ty2) || space1 != space2 then
968                err "mismatch between pointer types in binary '-'";
969              if not (pointer_arithmetic_ok env ty1) then
970                err "illegal pointer arithmetic in binary '-'";
971              (TPtr(space1, ty1, []), TInt(ptrdiff_t_ikind, []))
972          | _, _ -> error "type error in binary '-'"
973        end in
974      { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres; espace = Any }
975
976  | BINARY(SHL, a1, a2) ->
977      elab_shift "<<" Oshl a1 a2
978
979  | BINARY(SHR, a1, a2) ->
980      elab_shift ">>" Oshr a1 a2
981
982  | BINARY(EQ, a1, a2) ->
983      elab_comparison Oeq a1 a2
984  | BINARY(NE, a1, a2) ->
985      elab_comparison One a1 a2
986  | BINARY(LT, a1, a2) ->
987      elab_comparison Olt a1 a2
988  | BINARY(GT, a1, a2) ->
989      elab_comparison Ogt a1 a2
990  | BINARY(LE, a1, a2) ->
991      elab_comparison Ole a1 a2
992  | BINARY(GE, a1, a2) ->
993      elab_comparison Oge a1 a2
994
995  | BINARY(BAND, a1, a2) ->
996      elab_binary_integer "&" Oand a1 a2
997  | BINARY(BOR, a1, a2) ->
998      elab_binary_integer "|" Oor a1 a2
999  | BINARY(XOR, a1, a2) ->
1000      elab_binary_integer "^" Oxor a1 a2
1001
1002(* 7.7 Logical operator expressions *)
1003
1004  | BINARY(AND, a1, a2) ->
1005      elab_logical_operator "&&" Ologand a1 a2
1006  | BINARY(OR, a1, a2) ->
1007      elab_logical_operator "||" Ologor a1 a2
1008
1009(* 7.8 Conditional expressions *)
1010  | QUESTION(a1, a2, a3) ->
1011      let b1 = elab a1 in
1012      let b2 = elab a2 in
1013      let b3 = elab a3 in
1014      let space = join_spaces b2.espace b3.espace in
1015      if not (is_scalar_type env b1.etyp) then
1016        err ("the first argument of '? :' is not a scalar type");
1017      begin match pointer_decay env b2.etyp, pointer_decay env b3.etyp with
1018      | (TInt _ | TFloat _), (TInt _ | TFloat _) ->
1019          { edesc = EConditional(b1, b2, b3);
1020            etyp = binary_conversion env b2.etyp b3.etyp;
1021            espace = space }
1022      (* TODO: maybe we should automatically cast to a generic pointer when the spaces don't match? *)
1023      | TPtr(sp1, ty1, a1), TPtr(sp2, ty2, a2) ->
1024          let tyres =
1025            if (is_void_type env ty1 || is_void_type env ty2) && sp1 = sp2 then
1026              TPtr(sp1, TVoid [], add_attributes a1 a2)
1027            else
1028              match combine_types ~noattrs:true env
1029                                  (TPtr(sp1, ty1, a1)) (TPtr(sp2, ty2, a2)) with
1030              | None ->
1031                  error "the second and third arguments of '? :' \
1032                         have incompatible pointer types"
1033              | Some ty -> ty
1034            in
1035          { edesc = EConditional(b1, b2, b3); etyp = tyres; espace = space }
1036      | TPtr(sp1, ty1, a1), TInt _ when is_literal_0 b3 ->
1037          { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(sp1, ty1, a1); espace = space }
1038      | TInt _, TPtr(sp2, ty2, a2) when is_literal_0 b2 ->
1039          { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(sp2, ty2, a2); espace = space }
1040      | ty1, ty2 ->
1041          match combine_types env ty1 ty2 with
1042          | None ->
1043              error ("the second and third arguments of '? :' have incompatible types")
1044          | Some tyres ->
1045              { edesc = EConditional(b1, b2, b3); etyp = tyres; espace = space }
1046      end
1047
1048(* 7.9 Assignment expressions *)
1049
1050  | BINARY(ASSIGN, a1, a2) ->
1051      let b1 = elab a1 in
1052      let b2 = elab a2 in
1053      if not (is_lvalue env b1) then
1054        err "left-hand side of assignment is not a l-value";
1055      if List.mem AConst (attributes_of_type env b1.etyp) then
1056        err "left-hand side of assignment has 'const' type";
1057      if not (valid_assignment env b2 b1.etyp) then begin
1058        if valid_cast env b2.etyp b1.etyp then
1059          warning "assigning a value of type@ %a@ to a lvalue of type@ %a"
1060                  Cprint.typ b2.etyp Cprint.typ b1.etyp
1061        else
1062          err "assigning a value of type@ %a@ to a lvalue of type@ %a"
1063                  Cprint.typ b2.etyp Cprint.typ b1.etyp;
1064      end;
1065      { edesc = EBinop(Oassign, b1, b2, b1.etyp); etyp = b1.etyp; espace = b1.espace }
1066
1067  | BINARY((ADD_ASSIGN | SUB_ASSIGN | MUL_ASSIGN | DIV_ASSIGN | MOD_ASSIGN
1068            | BAND_ASSIGN | BOR_ASSIGN | XOR_ASSIGN | SHL_ASSIGN | SHR_ASSIGN
1069            as op), a1, a2) ->
1070      let (sop, top) =
1071        match op with
1072        | ADD_ASSIGN -> (ADD, Oadd_assign)
1073        | SUB_ASSIGN -> (SUB, Osub_assign)
1074        | MUL_ASSIGN -> (MUL, Omul_assign)
1075        | DIV_ASSIGN -> (DIV, Odiv_assign)
1076        | MOD_ASSIGN -> (MOD, Omod_assign)
1077        | BAND_ASSIGN -> (BAND, Oand_assign)
1078        | BOR_ASSIGN -> (BOR, Oor_assign)
1079        | XOR_ASSIGN -> (XOR, Oxor_assign)
1080        | SHL_ASSIGN -> (SHL, Oshl_assign)
1081        | SHR_ASSIGN -> (SHR, Oshr_assign)
1082        | _ -> assert false in
1083      begin match elab (BINARY(sop, a1, a2)) with
1084      | { edesc = EBinop(_, b1, b2, _); etyp = ty } as b ->
1085          if not (is_lvalue env b1) then
1086            err ("left-hand side of assignment is not a l-value");
1087          if List.mem AConst (attributes_of_type env b1.etyp) then
1088            err "left-hand side of assignment has 'const' type";
1089          if not (valid_assignment env b b1.etyp) then begin
1090            if valid_cast env ty b1.etyp then
1091              warning "assigning a value of type@ %a@ to a lvalue of type@ %a"
1092                      Cprint.typ ty Cprint.typ b1.etyp
1093            else
1094              err "assigning a value of type@ %a@ to a lvalue of type@ %a"
1095                      Cprint.typ ty Cprint.typ b1.etyp;
1096          end;
1097          { edesc = EBinop(top, b1, b2, ty); etyp = b1.etyp; espace = b1.espace }
1098      | _ -> assert false
1099      end
1100
1101(* 7.10 Sequential expressions *)
1102
1103  | COMMA [] ->
1104      error "empty sequential expression"
1105  | COMMA (a1 :: al) ->                 (* watch for left associativity *)
1106      let rec elab_comma accu = function
1107      | [] -> accu
1108      | a :: l ->
1109          let b = elab a in
1110          elab_comma { edesc = EBinop(Ocomma, accu, b, b.etyp); etyp = b.etyp; espace = b.espace } l
1111      in elab_comma (elab a1) al
1112
1113(* Extensions that we do not handle *)
1114
1115  | LABELADDR _ ->
1116      error "GCC's &&label construct is not supported"
1117  | GNU_BODY _ ->
1118      error "GCC's statements within expressions are not supported"
1119  | EXPR_ALIGNOF _ | TYPE_ALIGNOF _ ->
1120      error "GCC's __alignof__ construct is not supported"
1121
1122(*
1123  | EXPR_ALIGNOF a1 ->
1124      warning "nonstandard `alignof' expression, turned into a constant";
1125      let b1 = elab a1 in
1126      begin match alignof env b1.etyp with
1127      | None -> error "incomplete type %a" Cprint.typ b1.etyp
1128      | Some al -> intconst (Int64.of_int al) size_t_ikind
1129      end
1130  | TYPE_ALIGNOF (spec, dcl) ->
1131      warning "nonstandard `alignof' expression, turned into a constant";
1132      let ty = elab_type loc env spec dcl in
1133      begin match alignof env ty with
1134      | None -> error "incomplete type %a" Cprint.typ ty
1135      | Some al -> intconst (Int64.of_int al) size_t_ikind
1136      end
1137*)
1138
1139(* Elaboration of pre- or post- increment/decrement *)
1140  and elab_pre_post_incr_decr op msg a1 =
1141      let b1 = elab a1 in
1142      if not (is_lvalue env b1) then
1143        err "the argument of %s is not a l-value" msg;
1144      if not (is_scalar_type env b1.etyp) then
1145        err "the argument of %s must be an arithmetic or pointer type" msg;
1146      { edesc = EUnop(op, b1); etyp = b1.etyp; espace = b1.espace }
1147
1148(* Elaboration of binary operators over integers *)
1149  and elab_binary_integer msg op a1 a2 =
1150      let b1 = elab a1 in
1151      if not (is_integer_type env b1.etyp) then
1152        error "the first argument of '%s' is not an integer type" msg;
1153      let b2 = elab a2 in
1154      if not (is_integer_type env b2.etyp) then
1155        error "the second argument of '%s' is not an integer type" msg;
1156      let tyres = binary_conversion env b1.etyp b2.etyp in
1157      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres; espace = Any }
1158
1159(* Elaboration of binary operators over arithmetic types *)
1160  and elab_binary_arithmetic msg op a1 a2 =
1161      let b1 = elab a1 in
1162      if not (is_arith_type env b1.etyp) then
1163        error "the first argument of '%s' is not an arithmetic type" msg;
1164      let b2 = elab a2 in
1165      if not (is_arith_type env b2.etyp) then
1166        error "the second argument of '%s' is not an arithmetic type" msg;
1167      let tyres = binary_conversion env b1.etyp b2.etyp in
1168      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres; espace = Any }
1169
1170(* Elaboration of shift operators *)
1171  and elab_shift msg op a1 a2 =
1172      let b1 = elab a1 in
1173      if not (is_integer_type env b1.etyp) then
1174        error "the first argument of '%s' is not an integer type" msg;
1175      let b2 = elab a2 in
1176      if not (is_integer_type env b2.etyp) then
1177        error "the second argument of '%s' is not an integer type" msg;
1178      let tyres = unary_conversion env b1.etyp in
1179      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres; espace = Any }
1180
1181(* Elaboration of comparisons *)
1182  and elab_comparison op a1 a2 =
1183      let b1 = elab a1 in
1184      let b2 = elab a2 in
1185      let resdesc =
1186        match pointer_decay env b1.etyp, pointer_decay env b2.etyp with
1187        | (TInt _ | TFloat _), (TInt _ | TFloat _) ->
1188            EBinop(op, b1, b2, binary_conversion env b1.etyp b2.etyp)
1189        | TInt _, TPtr(sp, ty, _) when is_literal_0 b1 ->
1190            EBinop(op, nullconst, b2, TPtr(sp, ty, []))
1191        | TPtr(sp, ty, _), TInt _ when is_literal_0 b2 ->
1192            EBinop(op, b1, nullconst, TPtr(sp, ty, []))
1193        | TPtr(sp1, ty1, _), TPtr(sp2, ty2, _)
1194          when is_void_type env ty1 ->
1195            EBinop(op, b1, b2, TPtr(sp2, ty2, []))  (* XXX sp1? *)
1196        | TPtr(sp1, ty1, _), TPtr(sp2, ty2, _)
1197          when is_void_type env ty2 ->
1198            EBinop(op, b1, b2, TPtr(sp1, ty1, []))  (* XXX sp2? *)
1199        | TPtr(sp1, ty1, _), TPtr(sp2, ty2, _) ->
1200            if not (compatible_types ~noattrs:true env ty1 ty2) then
1201              warning "comparison between incompatible pointer types";
1202            EBinop(op, b1, b2, TPtr(sp1, ty1, []))  (* XXX sp1? *)
1203        | TPtr (sp,_,_), TInt _
1204        | TInt _, TPtr (sp,_,_) ->
1205            warning "comparison between integer and pointer";
1206            EBinop(op, b1, b2, TPtr(sp,TVoid [], []))
1207        | ty1, ty2 ->
1208            error "illegal comparison between types@ %a@ and %a"
1209                  Cprint.typ b1.etyp Cprint.typ b2.etyp in
1210      { edesc = resdesc; etyp = TInt(IInt, []); espace = Any }
1211
1212(* Elaboration of && and || *)
1213  and elab_logical_operator msg op a1 a2 =
1214      let b1 = elab a1 in
1215      if not (is_scalar_type env b1.etyp) then
1216        err "the first argument of '%s' is not a scalar type" msg;
1217      let b2 = elab a2 in
1218      if not (is_scalar_type env b2.etyp) then
1219        err "the second argument of '%s' is not a scalar type" msg;
1220      { edesc = EBinop(op, b1, b2, TInt(IInt, [])); etyp = TInt(IInt, []); espace = Any }
1221
1222(* Type-checking of function arguments *)
1223  and elab_arguments argno args params vararg =
1224    match args, params with
1225    | [], [] -> []
1226    | [], _::_ -> err "not enough arguments in function call"; []
1227    | _::_, [] -> 
1228        if vararg
1229        then args
1230        else (err "too many arguments in function call"; args)
1231    | arg1 :: argl, (_, ty_p) :: paraml ->
1232        let ty_a = argument_conversion env arg1.etyp in
1233        if not (valid_assignment env {arg1 with etyp = ty_a} ty_p) then begin
1234          if valid_cast env ty_a ty_p then
1235            warning
1236              "argument #%d of function call has type@ %a@ \
1237               instead of the expected type@ %a"
1238              argno Cprint.typ ty_a Cprint.typ ty_p
1239          else
1240            err
1241              "argument #%d of function call has type@ %a@ \
1242               instead of the expected type@ %a"
1243              argno Cprint.typ ty_a Cprint.typ ty_p
1244        end;
1245        arg1 :: elab_arguments (argno + 1) argl paraml vararg
1246
1247  in elab a
1248
1249(* Filling in forward declaration *)
1250let _ = elab_expr_f := elab_expr
1251
1252let elab_opt_expr loc env = function
1253  | NOTHING -> None
1254  | a -> Some (elab_expr loc env a)
1255
1256let elab_for_expr loc env = function
1257  | NOTHING -> { sdesc = Sskip; sloc = elab_loc loc }
1258  | a -> { sdesc = Sdo (elab_expr loc env a); sloc = elab_loc loc }
1259
1260
1261(* Elaboration of initializers *)
1262
1263(* Initializers are first elaborated to the following type: *)
1264
1265let project_init loc il =
1266  List.map
1267   (fun (what, i) ->
1268      if what <> NEXT_INIT then
1269        error loc "C99 initializers are not supported";
1270      i)
1271   il
1272
1273let below_optsize n opt_sz =
1274  match opt_sz with None -> true | Some sz -> n < sz
1275
1276let init_char_array_string opt_size s =
1277  let init = ref []
1278  and len = ref 0L in
1279  let enter x =
1280    if below_optsize !len opt_size then begin
1281      init := Init_single (intconst x IChar) :: !init;
1282      len := Int64.succ !len
1283    end in
1284  for i = 0 to String.length s - 1 do
1285    enter (Int64.of_int (Char.code s.[i]))
1286  done;
1287  enter 0L;
1288  Init_array (List.rev !init)
1289
1290let init_int_array_wstring opt_size s =
1291  let init = ref []
1292  and len = ref 0L in
1293  let enter x =
1294    if below_optsize !len opt_size then begin
1295      init := Init_single (intconst x IInt) :: !init;
1296      len := Int64.succ !len
1297    end in
1298  List.iter enter s;
1299  enter 0L;
1300  Init_array (List.rev !init)
1301
1302let check_init_type loc env a ty =
1303  if valid_assignment env a ty then ()
1304  else if valid_cast env a.etyp ty then
1305    warning loc
1306      "initializer has type@ %a@ instead of the expected type @ %a"
1307      Cprint.typ a.etyp Cprint.typ ty
1308  else
1309    error loc
1310      "initializer has type@ %a@ instead of the expected type @ %a"
1311      Cprint.typ a.etyp Cprint.typ ty
1312
1313(* Build an initializer for type [ty], consuming initialization items
1314   from the list [ile].  Return a pair (initializer, items not consumed). *)
1315
1316let rec elab_init loc env ty ile =
1317  match unroll env ty with
1318  | TArray(space, ty_elt, opt_sz, _) ->
1319      let rec elab_init_array n accu rem =
1320        match opt_sz, rem with
1321        | Some sz, _ when n >= sz ->
1322            (Init_array(List.rev accu), rem)
1323        | None, [] ->
1324            (Init_array(List.rev accu), rem)
1325        | _, _ ->
1326          let (i, rem') = elab_init loc env ty_elt rem in
1327          elab_init_array (Int64.succ n) (i :: accu) rem' in
1328      begin match ile with
1329      (* char array = "string literal" *)
1330      | (SINGLE_INIT (CONSTANT (CONST_STRING s)) 
1331         | COMPOUND_INIT [_, SINGLE_INIT(CONSTANT (CONST_STRING s))]) :: ile1
1332        when (match unroll env ty_elt with
1333              | TInt((IChar|IUChar|ISChar), _) -> true
1334              | _ -> false) ->
1335          (init_char_array_string opt_sz s, ile1)
1336      (* wchar array = L"wide string literal" *)
1337      | (SINGLE_INIT (CONSTANT (CONST_WSTRING s))
1338         | COMPOUND_INIT [_, SINGLE_INIT(CONSTANT (CONST_WSTRING s))]) :: ile1
1339        when (match unroll env ty_elt with
1340              | TInt _ -> true
1341              | _ -> false) ->
1342          (init_int_array_wstring opt_sz s, ile1)
1343      (* array = { elt, ..., elt } *)
1344      | COMPOUND_INIT ile1 :: ile2 ->
1345          let (ie, rem) = elab_init_array 0L [] (project_init loc ile1) in
1346          if rem <> [] then
1347            warning loc "excess elements at end of array initializer";
1348          (ie, ile2)
1349      (* array = elt, ..., elt  (within a bigger compound initializer) *)
1350      | _ ->
1351          elab_init_array 0L [] ile
1352      end
1353  | TStruct(id, _) ->
1354      let ci = wrap Env.find_struct loc env id in
1355      let rec elab_init_fields fld accu rem =
1356        match fld with
1357        | [] -> 
1358            (Init_struct(id, List.rev accu), rem)
1359        | fld1 :: fld' ->
1360            let (i, rem') = elab_init loc env fld1.fld_typ rem in
1361            elab_init_fields fld' ((fld1, i) :: accu) rem' in
1362      begin match ile with
1363      (* struct = { elt, ..., elt } *)
1364      | COMPOUND_INIT ile1 :: ile2 ->
1365          let (ie, rem) = 
1366            elab_init_fields ci.ci_members [] (project_init loc ile1) in
1367          if rem <> [] then
1368            warning loc "excess elements at end of struct initializer";
1369          (ie, ile2)
1370      (* struct = elt, ..., elt (within a bigger compound initializer) *)
1371      | _ ->
1372          elab_init_fields ci.ci_members [] ile
1373      end
1374  | TUnion(id, _) ->
1375      let ci = wrap Env.find_union loc env id in
1376      let fld1 =
1377        match ci.ci_members with [] -> assert false | hd :: tl -> hd in
1378      begin match ile with
1379      (* union = { elt } *)
1380      | COMPOUND_INIT ile1 :: ile2 ->
1381          let (i, rem) = 
1382            elab_init loc env fld1.fld_typ (project_init loc ile1) in
1383          if rem <> [] then
1384            warning loc "excess elements at end of union initializer";
1385          (Init_union(id, fld1, i), ile2)
1386      (* union = elt (within a bigger compound initializer) *)
1387      | _ ->
1388          let (i, rem) = elab_init loc env fld1.fld_typ ile in
1389          (Init_union(id, fld1, i), rem)
1390      end
1391  | TInt _ | TFloat _ | TPtr _ ->
1392      begin match ile with
1393      (* scalar = elt *)
1394      | SINGLE_INIT a :: ile1 ->
1395          let a' = elab_expr loc env a in
1396          check_init_type loc env a' ty;
1397          (Init_single a', ile1)
1398      (* scalar = nothing (within a bigger compound initializer) *)
1399      | (NO_INIT :: ile1) | ([] as ile1) ->
1400          begin match unroll env ty with
1401          | TInt _   -> (Init_single (intconst 0L IInt), ile1)
1402          | TFloat _ -> (Init_single (floatconst 0.0 FDouble), ile1)
1403          | TPtr _   -> (Init_single nullconst, ile1)
1404          | _        -> assert false
1405          end
1406      | COMPOUND_INIT _ :: ile1 ->
1407          fatal_error loc "compound initializer for type@ %a" Cprint.typ ty
1408      end
1409  | _ ->
1410      fatal_error loc "impossible to initialize at type@ %a" Cprint.typ ty
1411
1412let elab_initial loc env ty ie =
1413  match unroll env ty, ie with
1414  | _, NO_INIT -> None
1415  (* scalar or composite = expr *)
1416  | (TInt _ | TFloat _ | TPtr _ | TStruct _ | TUnion _), SINGLE_INIT a ->
1417      let a' = elab_expr loc env a in
1418      check_init_type loc env a' ty;
1419      Some (Init_single a')
1420  (* array = expr or
1421     array or struct or union = { elt, ..., elt } *)
1422  | (TArray _, SINGLE_INIT _)
1423  | ((TArray _ | TStruct _ | TUnion _), COMPOUND_INIT _) ->
1424      let (i, rem) = elab_init loc env ty [ie] in 
1425      if rem <> [] then
1426        warning loc "excess elements at end of compound initializer";
1427      Some i
1428  | _, _ ->
1429      error loc "ill-formed initializer for type@ %a" Cprint.typ ty;
1430      None
1431
1432(* Complete an array type with the size obtained from the initializer:
1433   "int x[] = { 1, 2, 3 }" becomes "int x[3] = ..." *)
1434
1435let fixup_typ env ty init =
1436  match unroll env ty, init with
1437  | TArray(space, ty_elt, None, attr), Init_array il ->
1438      TArray(space, ty_elt, Some(Int64.of_int(List.length il)), attr)
1439  | _ -> ty
1440
1441(* Entry point *)
1442
1443let elab_initializer loc env ty ie =
1444  match elab_initial loc env ty ie with
1445  | None ->
1446      (ty, None)
1447  | Some init ->
1448      (fixup_typ env ty init, Some init)
1449
1450
1451(* Elaboration of top-level and local definitions *)
1452
1453let enter_typedef loc env (s, sto, ty) =
1454  if sto <> Storage_default then
1455    error loc "Non-default storage on 'typedef' definition";
1456  if redef Env.lookup_typedef env s <> None then
1457    error loc "Redefinition of typedef '%s'" s;
1458  let (id, env') =
1459    Env.enter_typedef env s ty in
1460  emit_elab (elab_loc loc) (Gtypedef(id, ty));
1461  env'
1462
1463let enter_or_refine_ident local loc env s sto ty space =
1464  match redef Env.lookup_ident env s with
1465  | Some(id, II_ident(old_sto, old_ty, old_space)) ->
1466      let new_ty =
1467        if local then begin
1468          error loc "redefinition of local variable '%s'" s;
1469          ty
1470        end else begin
1471          match combine_types env old_ty ty with
1472          | Some new_ty ->
1473              new_ty
1474          | None ->
1475              warning loc "redefinition of '%s' with incompatible type" s; ty
1476        end in
1477      let new_sto =
1478        if old_sto = Storage_extern then sto else
1479        if sto = Storage_extern then old_sto else
1480        if old_sto = sto then sto else begin
1481          warning loc "redefinition of '%s' with incompatible storage class" s;
1482          sto
1483        end in
1484      let new_space = join_spaces old_space space (* XXX: incompatible? *) in
1485      (id, Env.add_ident env id new_sto new_ty new_space)
1486  | Some(id, II_enum v) ->
1487      error loc "illegal redefinition of enumerator '%s'" s;
1488      (id, Env.add_ident env id sto ty space)
1489  | _ ->
1490      Env.enter_ident env s sto ty space
1491
1492let rec enter_decdefs local loc env = function
1493  | [] ->
1494      ([], env)
1495  | (space, s, sto, ty, init) :: rem ->
1496      (* Sanity checks on storage class *)
1497      begin match sto with
1498      | Storage_extern ->
1499          if init <> NO_INIT then error loc
1500                           "'extern' declaration cannot have an initializer"
1501      | Storage_register ->
1502          if not local then error loc "'register' on global declaration"
1503      | _ -> ()
1504      end;
1505      (* function declarations are always extern *)
1506      let sto' =
1507        match unroll env ty with TFun _ -> Storage_extern | _ -> sto in
1508      (* enter ident in environment with declared type, because
1509         initializer can refer to the ident *)
1510      let (id, env1) = enter_or_refine_ident local loc env s sto' ty space in
1511      (* process the initializer *)
1512      let (ty', init') = elab_initializer loc env1 ty init in
1513      (* update environment with refined type *)
1514      let env2 = Env.add_ident env1 id sto' ty' space in
1515      (* check for incomplete type *)
1516      if sto' <> Storage_extern && incomplete_type env ty' then
1517        warning loc "'%s' has incomplete type" s;
1518      if local && sto <> Storage_extern && sto <> Storage_static then begin
1519        (* Local definition *)
1520        let (decls, env3) = enter_decdefs local loc env2 rem in
1521        ((sto', id, ty', init') :: decls, env3)
1522      end else begin
1523        (* Global definition *)
1524        emit_elab (elab_loc loc) (Gdecl(space, (sto, id, ty', init')));
1525        enter_decdefs local loc env2 rem
1526      end
1527
1528let elab_fundef env (spec, name) body loc1 loc2 =
1529  let (s, sto, inline, ty, env1) = elab_name env spec name in
1530  if sto = Storage_register then
1531    error loc1 "a function definition cannot have 'register' storage class";
1532  (* Fix up the type.  We can have params = None but only for an
1533     old-style parameterless function "int f() {...}" *)
1534  let ty =
1535    match ty with
1536    | TFun(ty_ret, None, vararg, attr) -> TFun(ty_ret, Some [], vararg, attr)
1537    | _ -> ty in
1538  (* Extract info from type *)
1539  let (ty_ret, params, vararg) =
1540    match ty with
1541    | TFun(ty_ret, Some params, vararg, attr) -> (ty_ret, params, vararg)
1542    | _ -> fatal_error loc1 "wrong type for function definition" in
1543  (* Enter function in the environment, for recursive references *)
1544  let (fun_id, env1) = enter_or_refine_ident false loc1 env s sto ty Code in
1545  (* Enter parameters in the environment *)
1546  let env2 =
1547    List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty Any)
1548                   (Env.new_scope env1) params in
1549  (* Elaborate function body *)
1550  let body' = !elab_block_f loc2 ty_ret env2 body in
1551  (* Build and emit function definition *)
1552  let fn =
1553    { fd_storage = sto;
1554      fd_inline = inline;
1555      fd_name = fun_id;
1556      fd_ret = ty_ret;
1557      fd_params = params;
1558      fd_vararg = vararg;
1559      fd_locals = [];
1560      fd_body = body' } in
1561  emit_elab (elab_loc loc1) (Gfundef fn);
1562  env1
1563
1564let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition)
1565                    : decl list * Env.t =
1566  match def with
1567  (* "int f(int x) { ... }" *)
1568  | FUNDEF(spec_name, body, loc1, loc2) ->
1569      if local then error loc1 "local definition of a function";
1570      let env1 = elab_fundef env spec_name body loc1 loc2 in
1571      ([], env1)
1572
1573  (* "int x = 12, y[10], *z" *)
1574  | DECDEF(init_name_group, loc) ->
1575      let (dl, env1) = elab_init_name_group env init_name_group in
1576      enter_decdefs local loc env1 dl
1577
1578  (* "typedef int * x, y[10]; " *)
1579  | TYPEDEF(namegroup, loc) ->
1580      let (dl, env1) = elab_name_group env namegroup in
1581      let env2 = List.fold_left (enter_typedef loc) env1 dl in
1582      ([], env2)
1583
1584  (* "struct s { ...};" or "union u;" *)
1585  | ONLYTYPEDEF(spec, loc) ->
1586      let (space, sto, inl, ty, env') = elab_specifier ~only:true loc env spec in
1587      if sto <> Storage_default || inl then
1588        error loc "Non-default storage or 'inline' on 'struct' or 'union' declaration";
1589      ([], env')
1590
1591  (* global asm statement *)
1592  | GLOBASM(_, loc) ->
1593      error loc "Top-level 'asm' statement is not supported";
1594      ([], env)
1595
1596  (* pragma *)
1597  | PRAGMA(s, loc) ->
1598      emit_elab (elab_loc loc) (Gpragma s);
1599      ([], env)
1600
1601  (* extern "C" { ... } *)
1602  | LINKAGE(_, loc, defs) ->
1603      elab_definitions local env defs
1604
1605and elab_definitions local env = function
1606  | [] -> ([], env)
1607  | d1 :: dl ->
1608      let (decl1, env1) = elab_definition local env d1 in
1609      let (decl2, env2) = elab_definitions local env1 dl in
1610      (decl1 @ decl2, env2)
1611
1612
1613(* Elaboration of statements *)
1614
1615(* Extract list of Cabs statements from a Cabs block *)
1616
1617let block_body loc b =
1618  if b.blabels <> [] then
1619    error loc "GCC's '__label__' declaration is not supported";
1620  if b.battrs <> [] then
1621    warning loc "ignoring attributes on this block";
1622  b.bstmts
1623
1624(* Elaboration of a block.  Return the corresponding C statement. *)
1625
1626let elab_block loc return_typ env b =
1627
1628let rec elab_stmt env s =
1629
1630  match s with
1631
1632(* 8.2 Expression statements *)
1633
1634  | COMPUTATION(a, loc) ->
1635      { sdesc = Sdo (elab_expr loc env a); sloc = elab_loc loc }
1636
1637(* 8.3 Labeled statements *)
1638
1639  | LABEL(lbl, s1, loc) ->
1640      { sdesc = Slabeled(Slabel lbl, elab_stmt env s1); sloc = elab_loc loc }
1641
1642  | CASE(a, s1, loc) ->
1643      let a' = elab_expr loc env a in
1644      begin match Ceval.integer_expr env a' with
1645        | None ->
1646            error loc "argument of 'case' must be an integer compile-time constant"
1647        | Some n -> ()
1648      end;
1649      { sdesc = Slabeled(Scase a', elab_stmt env s1); sloc = elab_loc loc }
1650
1651  | CASERANGE(_, _, _, loc) ->
1652      error loc "GCC's 'case' with range of values is not supported";
1653      sskip
1654
1655  | DEFAULT(s1, loc) ->
1656      { sdesc = Slabeled(Sdefault, elab_stmt env s1); sloc = elab_loc loc }
1657
1658(* 8.4 Compound statements *)
1659
1660  | BLOCK(b, loc) ->
1661      elab_blk loc env b
1662
1663(* 8.5 Conditional statements *)
1664
1665  | IF(a, s1, s2, loc) ->
1666      let a' = elab_expr loc env a in
1667      if not (is_scalar_type env a'.etyp) then
1668        error loc "the condition of 'if' does not have scalar type";
1669      let s1' = elab_stmt env s1 in
1670      let s2' = elab_stmt env s2 in
1671      { sdesc = Sif(a', s1', s2'); sloc = elab_loc loc }
1672
1673(* 8.6 Iterative statements *)
1674
1675  | WHILE(a, s1, loc) ->
1676      let a' = elab_expr loc env a in
1677      if not (is_scalar_type env a'.etyp) then
1678        error loc "the condition of 'while' does not have scalar type";
1679      let s1' = elab_stmt env s1 in
1680      { sdesc = Swhile(a', s1'); sloc = elab_loc loc }
1681
1682  | DOWHILE(a, s1, loc) ->
1683      let s1' = elab_stmt env s1 in
1684      let a' = elab_expr loc env a in
1685      if not (is_scalar_type env a'.etyp) then
1686        error loc "the condition of 'while' does not have scalar type";
1687      { sdesc = Sdowhile(s1', a'); sloc = elab_loc loc }
1688
1689  | FOR(fc, a2, a3, s1, loc) ->
1690      let a1' =
1691        match fc with
1692        | FC_EXP a1 ->
1693            elab_for_expr loc env a1
1694        | FC_DECL def ->
1695            error loc "C99 declaration within `for' not supported";
1696            sskip in
1697      let a2' =
1698        if a2 = NOTHING
1699        then intconst 1L IInt
1700        else elab_expr loc env a2 in
1701      if not (is_scalar_type env a2'.etyp) then
1702        error loc "the condition of 'for' does not have scalar type";
1703      let a3' = elab_for_expr loc env a3 in
1704      let s1' = elab_stmt env s1 in
1705      { sdesc = Sfor(a1', a2', a3', s1'); sloc = elab_loc loc }
1706
1707(* 8.7 Switch statement *)
1708  | SWITCH(a, s1, loc) ->
1709      let a' = elab_expr loc env a in
1710      if not (is_arith_type env a'.etyp) then
1711        error loc "the argument of 'switch' does not have arithmetic type";
1712      let s1' = elab_stmt env s1 in
1713      { sdesc = Sswitch(a', s1'); sloc = elab_loc loc }
1714
1715(* 8,8 Break and continue statements *)
1716  | BREAK loc ->
1717      { sdesc = Sbreak; sloc = elab_loc loc }
1718  | CONTINUE loc ->
1719      { sdesc = Scontinue; sloc = elab_loc loc }
1720
1721(* 8.9 Return statements *)
1722  | RETURN(a, loc) ->
1723      let a' = elab_opt_expr loc env a in
1724      begin match (unroll env return_typ, a') with
1725      | TVoid _, None -> ()
1726      | TVoid _, Some _ ->
1727          error loc
1728            "'return' with a value in a function of return type 'void'"
1729      | _, None ->
1730          warning loc
1731            "'return' without a value in a function of return type@ %a"
1732            Cprint.typ return_typ
1733      | _, Some b ->
1734          if not (valid_assignment env b return_typ) then begin
1735            if valid_cast env b.etyp return_typ then
1736              warning loc
1737                "return value has type@ %a@ \
1738                 instead of the expected type@ %a"
1739                Cprint.typ b.etyp Cprint.typ return_typ
1740            else
1741              error loc
1742                "return value has type@ %a@ \
1743                 instead of the expected type@ %a"
1744                Cprint.typ b.etyp Cprint.typ return_typ
1745          end
1746      end;
1747      { sdesc = Sreturn a'; sloc = elab_loc loc }
1748
1749(* 8.10 Goto statements *)
1750  | GOTO(lbl, loc) ->
1751      { sdesc = Sgoto lbl; sloc = elab_loc loc }
1752
1753(* 8.11 Null statements *)
1754  | NOP loc ->
1755      { sdesc = Sskip; sloc = elab_loc loc }
1756
1757(* Unsupported *)
1758  | DEFINITION def ->
1759      error (get_definitionloc def) "ill-placed definition";
1760      sskip
1761  | COMPGOTO(a, loc) ->
1762      error loc "GCC's computed 'goto' is not supported";
1763      sskip
1764  | ASM(_, _, _, loc) ->
1765      error loc "'asm' statement is not supported";
1766      sskip
1767  | TRY_EXCEPT(_, _, _, loc) ->
1768      error loc "'try ... except' statement is not supported";
1769      sskip
1770  | TRY_FINALLY(_, _, loc) ->
1771      error loc "'try ... finally' statement is not supported";
1772      sskip
1773     
1774and elab_blk loc env b =
1775  let b' = elab_blk_body (Env.new_scope env) (block_body loc b) in
1776  { sdesc = Sblock b'; sloc = elab_loc loc }
1777
1778and elab_blk_body env sl =
1779  match sl with
1780  | [] ->
1781      []
1782  | DEFINITION def :: sl1 ->
1783      let (dcl, env') = elab_definition true env def in
1784      let loc = elab_loc (get_definitionloc def) in
1785      List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl
1786      @ elab_blk_body env' sl1
1787  | s :: sl1 ->
1788      let s' = elab_stmt env s in
1789      s' :: elab_blk_body env sl1
1790
1791in elab_blk loc env b
1792
1793(* Filling in forward declaration *)
1794let _ = elab_block_f := elab_block
1795
1796
1797(** * Entry point *)
1798
1799let elab_preprocessed_file name ic =
1800  let lb = Lexer.init name ic in
1801  reset();
1802  ignore (elab_definitions false (Builtins.environment())
1803                                 (Parser.file Lexer.initial lb));
1804  Lexer.finish();
1805  elaborated_program()
Note: See TracBrowser for help on using the repository browser.