--- /dev/null
+(* *********************************************************************)
+(* *)
+(* 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 ci.ci_alignof
+ | TUnion(name, _) ->
+ let ci = Env.find_union env name in ci.ci_alignof
+
+(* Compute the natural alignment of a struct or union. *)
+
+let 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 ci.ci_sizeof
+ | TUnion(name, _) ->
+ let ci = Env.find_union env name in ci.ci_sizeof
+
+(* Compute the size of a union.
+ It is the size is the max of the sizes of fields, rounded up to the
+ natural alignment. *)
+
+let 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
+
+(* Compute the size of a struct.
+ We lay out fields consecutively, inserting padding to preserve
+ their natural alignment. *)
+
+let 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
+
+(* Computing composite_info records *)
+
+let composite_info_decl env su =
+ { ci_kind = su; ci_members = []; ci_alignof = None; ci_sizeof = None }
+
+let composite_info_def env su m =
+ { ci_kind = su; ci_members = m;
+ ci_alignof = alignof_struct_union env m;
+ ci_sizeof =
+ match su with
+ | Struct -> sizeof_struct env m
+ | Union -> sizeof_union env m }
+
+(* 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
+
+
projects / pkg-cerco / acc-trusted.git / blobdiff