1 files changed, 700 insertions, 0 deletions

diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
new file mode 100644
index 0000000..c0c26e5
--- /dev/null
+++ b/cparser/Cutil.ml
@@ -0,0 +1,700 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Operations on C types and abstract syntax *)
+
+open Printf
+open Errors
+open C
+open Env
+open Machine
+
+(* Set and Map structures over identifiers *)
+
+module Ident = struct
+  type t = ident
+  let compare id1 id2 = Pervasives.compare id1.stamp id2.stamp
+end
+
+module IdentSet = Set.Make(Ident)
+module IdentMap = Map.Make(Ident)
+
+(* Operations on attributes *)
+
+(* Lists of attributes are kept sorted in increasing order *)
+
+let rec add_attributes (al1: attributes) (al2: attributes) =
+  match al1, al2 with
+  | [], _ -> al2
+  | _, [] -> al1
+  | a1 :: al1', a2 :: al2' ->
+      if a1 < a2 then a1 :: add_attributes al1' al2
+      else if a1 > a2 then a2 :: add_attributes al1 al2'
+      else a1 :: add_attributes al1' al2'
+
+let rec remove_attributes (al1: attributes) (al2: attributes) = 
+  (* viewed as sets: al1 \ al2 *)
+  match al1, al2 with
+  | [], _ -> []
+  | _, [] -> al1
+  | a1 :: al1', a2 :: al2' ->
+      if a1 < a2 then a1 :: remove_attributes al1' al2
+      else if a1 > a2 then remove_attributes al1 al2'
+      else remove_attributes al1' al2'
+
+let rec incl_attributes (al1: attributes) (al2: attributes) =
+  match al1, al2 with
+  | [], _ -> true
+  | _ :: _, [] -> false
+  | a1 :: al1', a2 :: al2' ->
+      if a1 < a2 then false
+      else if a1 > a2 then incl_attributes al1 al2'
+      else incl_attributes al1' al2'
+
+(* Adding top-level attributes to a type.  Doesn't need to unroll defns. *)
+(* Array types cannot carry attributes, so add them to the element type. *)
+
+let rec add_attributes_type attr t =
+  match t with
+  | TVoid a -> TVoid (add_attributes attr a)
+  | TInt(ik, a) -> TInt(ik, add_attributes attr a)
+  | TFloat(fk, a) -> TFloat(fk, add_attributes attr a)
+  | TPtr(ty, a) -> TPtr(ty, add_attributes attr a)
+  | TArray(ty, sz, a) -> TArray(add_attributes_type attr ty, sz, a)
+  | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, add_attributes attr 
+a)
+  | TNamed(s, a) -> TNamed(s, add_attributes attr a)
+  | TStruct(s, a) -> TStruct(s, add_attributes attr a)
+  | TUnion(s, a) -> TUnion(s, add_attributes attr a)
+
+(* Unrolling of typedef *)
+
+let rec unroll env t =
+  match t with
+  | TNamed(name, attr) ->
+      let ty = Env.find_typedef env name in
+      unroll env (add_attributes_type attr ty)
+  | _ -> t
+
+(* Extracting the attributes of a type *)
+
+let rec attributes_of_type env t =
+  match t with
+  | TVoid a -> a
+  | TInt(ik, a) -> a
+  | TFloat(fk, a) -> a
+  | TPtr(ty, a) -> a
+  | TArray(ty, sz, a) -> a              (* correct? *)
+  | TFun(ty, params, vararg, a) -> a
+  | TNamed(s, a) -> attributes_of_type env (unroll env t)
+  | TStruct(s, a) -> a
+  | TUnion(s, a) -> a
+
+(* Changing the attributes of a type (at top-level) *)
+(* Same hack as above for array types. *)
+
+let rec change_attributes_type env (f: attributes -> attributes) t =
+  match t with
+  | TVoid a -> TVoid (f a)
+  | TInt(ik, a) -> TInt(ik, f a)
+  | TFloat(fk, a) -> TFloat(fk, f a)
+  | TPtr(ty, a) -> TPtr(ty, f a)
+  | TArray(ty, sz, a) ->
+      TArray(change_attributes_type env f ty, sz, a)
+  | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, f a)
+  | TNamed(s, a) ->
+      let t1 = unroll env t in
+      let t2 = change_attributes_type env f t1 in
+      if t2 = t1 then t else t2         (* avoid useless expansion *)
+  | TStruct(s, a) -> TStruct(s, f a)
+  | TUnion(s, a) -> TUnion(s, f a)
+
+let remove_attributes_type env attr t =
+  change_attributes_type env (fun a -> remove_attributes a attr) t
+
+let erase_attributes_type env t =
+  change_attributes_type env (fun a -> []) t
+
+(* Type compatibility *)
+
+exception Incompat
+
+let combine_types ?(noattrs = false) env t1 t2 =
+
+  let comp_attr a1 a2 =
+    if a1 = a2 then a2
+    else if noattrs then add_attributes a1 a2
+    else raise Incompat
+  and comp_base x1 x2 =
+    if x1 = x2 then x2 else raise Incompat
+  and comp_array_size sz1 sz2 =
+    match sz1, sz2 with
+    | None, _ -> sz2
+    | _, None -> sz1
+    | Some n1, Some n2 -> if n1 = n2 then Some n2 else raise Incompat
+  and comp_conv (id, ty) =
+    match unroll env ty with
+    | TInt(kind, attr) ->
+        begin match kind with
+        | IBool | IChar | ISChar | IUChar | IShort | IUShort -> raise Incompat
+        | _ -> ()
+        end
+    | TFloat(kind, attr) ->
+        begin match kind with
+        | FFloat -> raise Incompat
+        | _ -> ()
+        end
+    | _ -> () in
+
+  let rec comp t1 t2 =
+    match t1, t2 with
+    | TVoid a1, TVoid a2 ->
+        TVoid(comp_attr a1 a2)
+    | TInt(ik1, a1), TInt(ik2, a2) ->
+        TInt(comp_base ik1 ik2, comp_attr a1 a2)
+    | TFloat(fk1, a1), TFloat(fk2, a2) ->
+        TFloat(comp_base fk1 fk2, comp_attr a1 a2)
+    | TPtr(ty1, a1), TPtr(ty2, a2) ->
+        TPtr(comp ty1 ty2, comp_attr a1 a2)
+    | TArray(ty1, sz1, a1), TArray(ty2, sz2, a2) ->
+        TArray(comp ty1 ty2, comp_array_size sz1 sz2, comp_attr a1 a2)
+    | TFun(ty1, params1, vararg1, a1), TFun(ty2, params2, vararg2, a2) ->
+        let (params, vararg) =
+          match params1, params2 with
+          | None, None -> None, false
+          | None, Some l2 -> List.iter comp_conv l2; (params2, vararg2)
+          | Some l1, None -> List.iter comp_conv l1; (params1, vararg1)
+          | Some l1, Some l2 ->
+              if List.length l1 <> List.length l2 then raise Incompat;
+              (Some(List.map2 (fun (id1, ty1) (id2, ty2) -> (id2, comp ty1 ty2))
+                              l1 l2),
+               comp_base vararg1 vararg2)
+        in
+          TFun(comp ty1 ty2, params, vararg, comp_attr a1 a2)
+    | TNamed _, _ -> comp (unroll env t1) t2
+    | _, TNamed _ -> comp t1 (unroll env t2)
+    | TStruct(s1, a1), TStruct(s2, a2) ->
+        TStruct(comp_base s1 s2, comp_attr a1 a2)
+    | TUnion(s1, a1), TUnion(s2, a2) -> 
+        TUnion(comp_base s1 s2, comp_attr a1 a2)
+    | _, _ ->
+        raise Incompat
+
+  in try Some(comp t1 t2) with Incompat -> None
+
+let compatible_types  ?noattrs env t1 t2 =
+  match combine_types ?noattrs env t1 t2 with Some _ -> true | None -> false
+
+(* Naive placement algorithm for bit fields, might not match that
+   of the compiler. *)
+
+let pack_bitfields ml =
+  let rec pack nbits = function
+  | [] ->
+      (nbits, [])
+  | m :: ms as ml ->
+      match m.fld_bitfield with
+      | None -> (nbits, ml)
+      | Some n ->
+          if n = 0 then
+            (nbits, ms) (* bit width 0 means end of pack *)
+          else if nbits + n >= 8 * !config.sizeof_int then
+            (nbits, ml) (* doesn't fit in current word *)
+          else
+            pack (nbits + n) ms (* add to current word *)
+  in
+  let (nbits, ml') = pack 0 ml in
+  let sz =
+    if nbits <= 8 then 1 else
+    if nbits <= 16 then 2 else
+    if nbits <= 32 then 4 else
+    if nbits <= 64 then 8 else assert false in
+  (sz, ml')
+
+(* Natural alignment, in bytes *)
+
+let alignof_ikind = function
+  | IBool | IChar | ISChar | IUChar -> 1
+  | IInt | IUInt -> !config.alignof_int
+  | IShort | IUShort -> !config.alignof_short
+  | ILong | IULong -> !config.alignof_long
+  | ILongLong | IULongLong -> !config.alignof_longlong
+
+let alignof_fkind = function
+  | FFloat -> !config.alignof_float
+  | FDouble -> !config.alignof_double
+  | FLongDouble -> !config.alignof_longdouble
+
+(* Return natural alignment of given type, or None if the type is incomplete *)
+
+let rec alignof env t =
+  match t with
+  | TVoid _ -> !config.alignof_void
+  | TInt(ik, _) -> Some(alignof_ikind ik)
+  | TFloat(fk, _) -> Some(alignof_fkind fk)
+  | TPtr(_, _) -> Some(!config.alignof_ptr)
+  | TArray(ty, _, _) -> alignof env ty
+  | TFun(_, _, _, _) -> !config.alignof_fun
+  | TNamed(_, _) -> alignof env (unroll env t)
+  | TStruct(name, _) ->
+      let ci = Env.find_struct env name in
+      if ci.ci_incomplete
+      then None
+      else alignof_struct_union
+             (Env.add_composite env name {ci with ci_incomplete = true})
+             ci.ci_members
+  | TUnion(name, _) ->
+      let ci = Env.find_union env name in
+      if ci.ci_incomplete
+      then None
+      else alignof_struct_union
+             (Env.add_composite env name {ci with ci_incomplete = true})
+             ci.ci_members
+
+(* We set ci_incomplete to true before recursing so that we stop and
+   return None on ill-formed structs such as struct a { struct a x; }. *)
+
+and alignof_struct_union env members =
+  let rec align_rec al = function
+  | [] -> Some al
+  | m :: rem as ml ->
+      if m.fld_bitfield = None then begin
+        match alignof env m.fld_typ with
+        | None -> None
+        | Some a -> align_rec (max a al) rem
+      end else begin
+        let (sz, ml') = pack_bitfields ml in
+        align_rec (max sz al) ml'
+      end
+  in align_rec 1 members
+
+let align x boundary =
+  (* boundary must be a power of 2 *)
+  (x + boundary - 1) land (lnot (boundary - 1))
+
+(* Size of, in bytes *)
+
+let sizeof_ikind = function
+  | IBool | IChar | ISChar | IUChar -> 1
+  | IInt | IUInt -> !config.sizeof_int
+  | IShort | IUShort -> !config.sizeof_short
+  | ILong | IULong -> !config.sizeof_long
+  | ILongLong | IULongLong -> !config.sizeof_longlong
+
+let sizeof_fkind = function
+  | FFloat -> !config.sizeof_float
+  | FDouble -> !config.sizeof_double
+  | FLongDouble -> !config.sizeof_longdouble
+
+(* Overflow-avoiding multiplication of an int64 and an int, with
+   result in type int. *)
+
+let cautious_mul (a: int64) (b: int) =
+  if b = 0 || a <= Int64.of_int (max_int / b)
+  then Some(Int64.to_int a * b)
+  else None
+
+(* Return size of type, in bytes, or [None] if the type is incomplete *)
+
+let rec sizeof env t =
+  match t with
+  | TVoid _ -> !config.sizeof_void
+  | TInt(ik, _) -> Some(sizeof_ikind ik)
+  | TFloat(fk, _) -> Some(sizeof_fkind fk)
+  | TPtr(_, _) -> Some(!config.sizeof_ptr)
+  | TArray(ty, None, _) -> None
+  | TArray(ty, Some n, _) as t' ->
+      begin match sizeof env ty with
+      | None -> None
+      | Some s ->
+          match cautious_mul n s with
+          | Some sz -> Some sz
+          | None -> error "sizeof(%a) overflows" Cprint.typ t'; Some 1
+      end
+  | TFun(_, _, _, _) -> !config.sizeof_fun
+  | TNamed(_, _) -> sizeof env (unroll env t)
+  | TStruct(name, _) ->
+      let ci = Env.find_struct env name in
+      if ci.ci_incomplete
+      then None
+      else sizeof_struct
+             (Env.add_composite env name {ci with ci_incomplete = true})
+             ci.ci_members
+  | TUnion(name, _) ->
+      let ci = Env.find_union env name in
+      if ci.ci_incomplete
+      then None
+      else sizeof_union
+             (Env.add_composite env name {ci with ci_incomplete = true})
+             ci.ci_members
+
+(* We set ci_incomplete to true before recursing so that we stop and
+   return None on ill-formed structs such as struct a { struct a x; }. *)
+
+(* For a union, the size is the max of the sizes of fields,
+   rounded up to the natural alignment. *)
+
+and sizeof_union env members =
+  let rec sizeof_rec sz = function
+  | [] ->
+      begin match alignof_struct_union env members with
+      | None -> None                    (* should not happen? *)
+      | Some al -> Some (align sz al)
+      end
+  | m :: rem ->
+      begin match sizeof env m.fld_typ with
+      | None -> None
+      | Some s -> sizeof_rec (max sz s) rem
+      end
+  in sizeof_rec 0 members
+
+(* For a struct, we lay out fields consecutively, inserting padding
+   to preserve their natural alignment. *)
+
+and sizeof_struct env members =
+  let rec sizeof_rec ofs = function
+  | [] | [ { fld_typ = TArray(_, None, _) } ] ->
+      (* C99: ty[] allowed as last field *)
+      begin match alignof_struct_union env members with
+      | None -> None                    (* should not happen? *)
+      | Some al -> Some (align ofs al)
+      end
+  | m :: rem as ml ->
+      if m.fld_bitfield = None then begin
+        match alignof env m.fld_typ, sizeof env m.fld_typ with
+        | Some a, Some s -> sizeof_rec (align ofs a + s) rem
+        | _, _ -> None
+      end else begin
+        let (sz, ml') = pack_bitfields ml in
+        sizeof_rec (align ofs sz + sz) ml'
+      end
+  in sizeof_rec 0 members
+
+(* Determine whether a type is incomplete *)
+
+let incomplete_type env t =
+  match sizeof env t with None -> true | Some _ -> false
+
+(* Type of a function definition *)
+
+let fundef_typ fd =
+  TFun(fd.fd_ret, Some fd.fd_params, fd.fd_vararg, [])
+
+(* Signedness of integer kinds *)
+
+let is_signed_ikind = function
+  | IBool -> false
+  | IChar -> !config.char_signed
+  | ISChar -> true
+  | IUChar -> false
+  | IInt -> true
+  | IUInt -> false
+  | IShort -> true
+  | IUShort -> false
+  | ILong -> true
+  | IULong -> false
+  | ILongLong -> true
+  | IULongLong -> false
+
+(* Conversion to unsigned ikind *)
+
+let unsigned_ikind_of = function
+  | IBool -> IBool
+  | IChar | ISChar | IUChar -> IUChar
+  | IInt | IUInt -> IUInt
+  | IShort | IUShort -> IUShort
+  | ILong | IULong -> IULong
+  | ILongLong | IULongLong -> IULongLong
+
+(* Some classification functions over types *)
+
+let is_void_type env t =
+  match unroll env t with
+  | TVoid _ -> true
+  | _ -> false
+
+let is_integer_type env t =
+  match unroll env t with
+  | TInt(_, _) -> true
+  | _ -> false
+
+let is_arith_type env t =
+  match unroll env t with
+  | TInt(_, _) -> true
+  | TFloat(_, _) -> true
+  | _ -> false
+
+let is_pointer_type env t =
+  match unroll env t with
+  | TPtr _ -> true
+  | _ -> false
+
+let is_scalar_type env t =
+  match unroll env t with
+  | TInt(_, _) -> true
+  | TFloat(_, _) -> true
+  | TPtr _ -> true
+  | TArray _ -> true                    (* assume implicit decay *)
+  | TFun _ -> true                      (* assume implicit decay *)
+  | _ -> false
+
+let is_composite_type env t =
+  match unroll env t with
+  | TStruct _ | TUnion _ -> true
+  | _ -> false
+
+let is_function_type env t =
+  match unroll env t with
+  | TFun _ -> true
+  | _ -> false
+
+(* Ranking of integer kinds *)
+
+let integer_rank = function
+  | IBool -> 1
+  | IChar | ISChar | IUChar -> 2
+  | IShort | IUShort -> 3
+  | IInt | IUInt -> 4
+  | ILong | IULong -> 5
+  | ILongLong | IULongLong -> 6
+
+(* Ranking of float kinds *)
+
+let float_rank = function
+  | FFloat -> 1
+  | FDouble -> 2
+  | FLongDouble -> 3
+
+(* Array and function types "decay" to pointer types in many cases *)
+
+let pointer_decay env t =
+  match unroll env t with
+  | TArray(ty, _, _) -> TPtr(ty, [])
+  | TFun _ as ty -> TPtr(ty, [])
+  | t -> t
+
+(* The usual unary conversions (H&S 6.3.3) *) 
+
+let unary_conversion env t = 
+  match unroll env t with
+  (* Promotion of small integer types *)
+  | TInt(kind, attr) ->
+      begin match kind with
+      | IBool | IChar | ISChar | IUChar | IShort | IUShort ->
+          TInt(IInt, attr)
+      | IInt | IUInt | ILong | IULong | ILongLong | IULongLong ->
+          TInt(kind, attr)
+      end
+  (* Arrays and functions decay automatically to pointers *)
+  | TArray(ty, _, _) -> TPtr(ty, [])
+  | TFun _ as ty -> TPtr(ty, [])
+  (* Other types are not changed *)
+  | t -> t
+
+(* The usual binary conversions  (H&S 6.3.4).
+   Applies only to arithmetic types.
+   Return the type to which both sides are to be converted. *)
+
+let binary_conversion env t1 t2 =
+  let t1 = unary_conversion env t1 in
+  let t2 = unary_conversion env t2 in
+  match unroll env t1, unroll env t2 with
+  | TFloat(FLongDouble, _), (TInt _ | TFloat _) -> t1
+  | (TInt _ | TFloat _), TFloat(FLongDouble, _) -> t2
+  | TFloat(FDouble, _), (TInt _ | TFloat _)     -> t1
+  | (TInt _ | TFloat _), TFloat(FDouble, _)     -> t2
+  | TFloat(FFloat, _), (TInt _ | TFloat _)      -> t1
+  | (TInt _), TFloat(FFloat, _)      -> t2
+  | TInt(k1, _), TInt(k2, _)  ->
+      if k1 = k2 then t1 else begin
+        match is_signed_ikind k1, is_signed_ikind k2 with
+        | true, true | false, false ->
+            (* take the bigger of the two types *)
+            if integer_rank k1 >= integer_rank k2 then t1 else t2
+        | false, true ->
+            (* if rank (unsigned type) >= rank (signed type),
+               take the unsigned type *)
+            if integer_rank k1 >= integer_rank k2 then t1
+            (* if rank (unsigned type) < rank (signed type)
+               and all values of the unsigned type can be represented
+               in the signed type, take the signed type *)
+            else if sizeof_ikind k2 > sizeof_ikind k1 then t2
+            (* if rank (unsigned type) < rank (signed type)
+               and some values of the unsigned type cannot be represented
+               in the signed type,
+               take the unsigned type corresponding to the signed type *)
+            else TInt(unsigned_ikind_of k2, [])
+        | true, false ->
+            if integer_rank k2 >= integer_rank k1 then t2
+            else if sizeof_ikind k1 > sizeof_ikind k2 then t1
+            else TInt(unsigned_ikind_of k1, [])
+      end
+  | _, _ -> assert false
+
+(* Conversion on function arguments (with protoypes) *)
+
+let argument_conversion env t = 
+  (* Arrays and functions degrade automatically to pointers *)
+  (* Other types are not changed *)
+  match unroll env t with
+  | TArray(ty, _, _) -> TPtr(ty, [])
+  | TFun _ as ty -> TPtr(ty, [])
+  | _ -> t (* preserve typedefs *)
+
+(* Conversion on function arguments (old-style unprototyped, or vararg *)
+(* H&S 6.3.5 *)
+
+let default_argument_conversion env t =
+  match unary_conversion env t with
+  | TFloat(FFloat, attr) -> TFloat(FDouble, attr)
+  | t' -> t'
+
+(** Is the type Tptr(ty, a) appropriate for pointer arithmetic? *)
+
+let pointer_arithmetic_ok env ty =
+  match unroll env ty with
+  | TVoid _ | TFun _ -> false
+  | _ -> not (incomplete_type env ty)
+
+(** Special types *)
+
+let find_matching_unsigned_ikind sz =
+  if sz = !config.sizeof_int then IUInt
+  else if sz = !config.sizeof_long then IULong
+  else if sz = !config.sizeof_longlong then IULongLong
+  else assert false
+
+let find_matching_signed_ikind sz =
+  if sz = !config.sizeof_int then IInt
+  else if sz = !config.sizeof_long then ILong
+  else if sz = !config.sizeof_longlong then ILongLong
+  else assert false
+
+let wchar_ikind = find_matching_unsigned_ikind !config.sizeof_wchar
+let size_t_ikind = find_matching_unsigned_ikind !config.sizeof_size_t
+let ptr_t_ikind = find_matching_unsigned_ikind !config.sizeof_ptr
+let ptrdiff_t_ikind = find_matching_signed_ikind !config.sizeof_ptrdiff_t
+let enum_ikind = IInt
+
+(** The type of a constant *)
+
+let type_of_constant = function
+  | CInt(_, ik, _) -> TInt(ik, [])
+  | CFloat(_, fk, _) -> TFloat(fk, [])
+  | CStr _ -> TPtr(TInt(IChar, []), [])          (* XXX or array? const? *)
+  | CWStr _ -> TPtr(TInt(wchar_ikind, []), [])   (* XXX or array? const? *)
+  | CEnum(_, _) -> TInt(IInt, [])
+
+(* Check that a C expression is a lvalue *)
+
+let rec is_lvalue env e =
+  (* Type must not be array or function *)
+  match unroll env e.etyp with
+  | TFun _ | TArray _ -> false
+  | _ ->
+    match e.edesc with
+    | EVar id -> true
+    | EUnop((Oderef | Oarrow _), _) -> true
+    | EUnop(Odot _, e') -> is_lvalue env e'
+    | EBinop(Oindex, _, _, _) -> true
+    | _ -> false
+
+(* Check that a C expression is the literal "0", which can be used
+   as a pointer. *)
+
+let is_literal_0 e =
+  match e.edesc with
+  | EConst(CInt(0L, _, _)) -> true
+  | _ -> false
+
+(* Check that an assignment is allowed *)
+
+let valid_assignment env from tto =
+  match pointer_decay env from.etyp, pointer_decay env tto with
+  | (TInt _ | TFloat _), (TInt _ | TFloat _) -> true
+  | TInt _, TPtr _ -> is_literal_0 from
+  | TPtr(ty, _), TPtr(ty', _) ->
+      incl_attributes (attributes_of_type env ty) (attributes_of_type env ty')
+      && (is_void_type env ty || is_void_type env ty'
+          || compatible_types env
+               (erase_attributes_type env ty)
+               (erase_attributes_type env ty'))
+  | TStruct(s, _), TStruct(s', _) -> s = s'
+  | TUnion(s, _), TUnion(s', _) -> s = s'
+  | _, _ -> false
+
+(* Check that a cast is allowed *)
+
+let valid_cast env tfrom tto =
+  compatible_types ~noattrs:true env tfrom tto ||
+  begin match unroll env tfrom, unroll env tto with
+  | _, TVoid _ -> true
+  (* from any int-or-pointer (with array and functions decaying to pointers)
+     to any int-or-pointer *)
+  | (TInt _ | TPtr _ | TArray _ | TFun _), (TInt _ | TPtr _) -> true
+  (* between int and float types *)
+  | (TInt _ | TFloat _), (TInt _ | TFloat _) -> true
+  | _, _ -> false
+  end
+
+(* Construct an integer constant *)
+
+let intconst v ik =
+  { edesc = EConst(CInt(v, ik, "")); etyp = TInt(ik, []) }
+
+(* Construct a float constant *)
+
+let floatconst v fk =
+  { edesc = EConst(CFloat(v, fk, "")); etyp = TFloat(fk, []) }
+
+(* Construct the literal "0" with void * type *)
+
+let nullconst =
+  { edesc = EConst(CInt(0L, ptr_t_ikind, "0")); etyp = TPtr(TVoid [], []) }
+
+(* Construct a sequence *)
+
+let sseq loc s1 s2 =
+  match s1.sdesc, s2.sdesc with
+  | Sskip, _ -> s2
+  | _, Sskip -> s1
+  | _, Sblock sl -> { sdesc = Sblock(s1 :: sl); sloc = loc }
+  | _, _ -> { sdesc = Sseq(s1, s2); sloc = loc }
+
+(* Construct an assignment statement *)
+
+let sassign loc lv rv =
+  { sdesc = Sdo {edesc = EBinop(Oassign, lv, rv, lv.etyp); etyp = lv.etyp};
+    sloc = loc }
+
+(* Empty location *)
+
+let no_loc = ("", -1)
+
+(* Dummy skip statement *)
+
+let sskip = { sdesc = Sskip; sloc = no_loc }
+
+(* Print a location *)
+
+let printloc oc (filename, lineno) =
+  if filename <> "" then Printf.fprintf oc "%s:%d: " filename lineno
+
+(* Format a location *)
+
+let formatloc pp (filename, lineno) =
+  if filename <> "" then Format.fprintf pp "%s:%d: " filename lineno
+
+