cparser/Elab.ml

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