cparser/Machine.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 (* Machine-dependent aspects *)
  17
  18 type t = {
  19   char_signed: bool;
  20   sizeof_ptr: int;
  21   sizeof_short: int;
  22   sizeof_int: int;
  23   sizeof_long: int;
  24   sizeof_longlong: int;
  25   sizeof_float: int;
  26   sizeof_double: int;
  27   sizeof_longdouble: int;
  28   sizeof_void: int option;
  29   sizeof_fun: int option;
  30   sizeof_wchar: int;
  31   sizeof_size_t: int;
  32   sizeof_ptrdiff_t: int;
  33   alignof_ptr: int;
  34   alignof_short: int;
  35   alignof_int: int;
  36   alignof_long: int;
  37   alignof_longlong: int;
  38   alignof_float: int;
  39   alignof_double: int;
  40   alignof_longdouble: int;
  41   alignof_void: int option;
  42   alignof_fun: int option
  43 }
  44
  45 let ilp32ll64 = {
  46   char_signed = false;
  47   sizeof_ptr = 4;
  48   sizeof_short = 2;
  49   sizeof_int = 4;
  50   sizeof_long = 4;
  51   sizeof_longlong = 8;
  52   sizeof_float = 4;
  53   sizeof_double = 8;
  54   sizeof_longdouble = 16;
  55   sizeof_void = None;
  56   sizeof_fun = None;
  57   sizeof_wchar = 4;
  58   sizeof_size_t = 4;
  59   sizeof_ptrdiff_t = 4;
  60   alignof_ptr = 4;
  61   alignof_short = 2;
  62   alignof_int = 4;
  63   alignof_long = 4;
  64   alignof_longlong = 8;
  65   alignof_float = 4;
  66   alignof_double = 8;
  67   alignof_longdouble = 16;
  68   alignof_void = None;
  69   alignof_fun = None
  70 }
  71
  72 let i32lpll64 = {
  73   char_signed = false;
  74   sizeof_ptr = 8;
  75   sizeof_short = 2;
  76   sizeof_int = 4;
  77   sizeof_long = 8;
  78   sizeof_longlong = 8;
  79   sizeof_float = 4;
  80   sizeof_double = 8;
  81   sizeof_longdouble = 16;
  82   sizeof_void = None;
  83   sizeof_fun = None;
  84   sizeof_wchar = 4;
  85   sizeof_size_t = 8;
  86   sizeof_ptrdiff_t = 8;
  87   alignof_ptr = 8;
  88   alignof_short = 2;
  89   alignof_int = 4;
  90   alignof_long = 8;
  91   alignof_longlong = 8;
  92   alignof_float = 4;
  93   alignof_double = 8;
  94   alignof_longdouble = 16;
  95   alignof_void = None;
  96   alignof_fun = None
  97 }
  98
  99 let il32pll64 = {
 100   char_signed = false;
 101   sizeof_ptr = 8;
 102   sizeof_short = 2;
 103   sizeof_int = 4;
 104   sizeof_long = 4;
 105   sizeof_longlong = 8;
 106   sizeof_float = 4;
 107   sizeof_double = 8;
 108   sizeof_longdouble = 16;
 109   sizeof_void = None;
 110   sizeof_fun = None;
 111   sizeof_wchar = 4;
 112   sizeof_size_t = 8;
 113   sizeof_ptrdiff_t = 8;
 114   alignof_ptr = 8;
 115   alignof_short = 2;
 116   alignof_int = 4;
 117   alignof_long = 4;
 118   alignof_longlong = 8;
 119   alignof_float = 4;
 120   alignof_double = 8;
 121   alignof_longdouble = 16;
 122   alignof_void = None;
 123   alignof_fun = None
 124 }
 125
 126 let make_char_signed c = {c with char_signed = true}
 127
 128 let gcc_extensions c =
 129   { c with sizeof_void = Some 1; sizeof_fun = Some 1;
 130            alignof_void = Some 1; alignof_fun = Some 1 }
 131
 132 let config =
 133   ref (match Sys.word_size with
 134            | 32 -> ilp32ll64
 135            | 64 -> if Sys.os_type = "Win32" then il32pll64 else i32lpll64
 136            | _  -> assert false)