convert.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-Clang                                      *)
(*                                                                        *)
(*  Copyright (C) 2012-2022                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file LICENSE).                      *)
(*                                                                        *)
(**************************************************************************)

open Intermediate_format
open Cabs
open Cil

let lambda_unique_name typ infix id =
  (Mangling.mangle_cc_type typ) ^ infix ^ Int64.to_string id

let lambda_unique_overload_name id =
  "__fc_lambda_overload_" ^ Int64.to_string id

let closure_name = "__fc_closure"

let fc_implicit_attr = "__fc_implicit"

let fc_pure_template_decl_attr = "__fc_pure_template_decl"

let capture_name_type env =
  function
  | Cap_id (s, typ, is_ref) ->
    let typ = if is_ref then Cxx_utils.obj_lvref typ else typ in (s, typ)
  | Cap_this(is_ref) ->
    let (name,tkind as cname) =
      Option.get (Convert_env.get_current_class env)
    in
    let typ =
      if is_ref then Cxx_utils.unqual_type (Struct (name, tkind))
      else Cxx_utils.class_lvref cname
    in ("this", typ)

let id x = x

let raw_block stmts = {blabels = []; battrs = []; bstmts = stmts}

let make_block env stmts =
  let loc = Convert_env.get_loc env in
  BLOCK(raw_block stmts,loc, loc)

let make_stmt env stmt_node =
  { stmt_ghost = Convert_env.is_ghost env; stmt_node }

let make_block_stmt env stmts = make_stmt env (make_block env stmts)

let make_computation env expr =
  make_stmt env (COMPUTATION (expr, expr.expr_loc))

let is_static l = List.mem Static l

(* f(void) means no argument, not one argument of type void *)
let remove_void prm =
  match prm with
    [ { plain_type = Void } ] -> []
  | prm -> prm

let convert_cv = function
  | Const -> SpecCV CV_CONST
  | Volatile -> SpecCV CV_VOLATILE
  | Restrict -> SpecCV CV_RESTRICT
  | Static -> SpecStorage STATIC

let cv_to_attr = function
  | SpecCV CV_CONST -> "const",[]
  | SpecCV CV_VOLATILE -> "volatile",[]
  | SpecCV CV_RESTRICT -> "restrict", []
  | SpecStorage STATIC -> "static", []
  | _ -> "unknown_cv_specifier", []

(* creates an array[dim] of d. Because Cabs follows closely the C
   syntax, we have to take some precautions here. *)
let rec protect_array_type al dim d =
  match d with
  | JUSTBASE -> ARRAY(d,al,dim)
  | PARENTYPE (al1,d',al2) ->
    PARENTYPE(al1,protect_array_type al dim d', al2)
  | ARRAY(d',al',dim') ->
    (* array dim of array dim' of d' is d' foo[dim][dim'] *)
    ARRAY(protect_array_type al dim d',al',dim')
  | PTR (al',d') ->
    (* array dim of ptr to d' is d' *foo[dim] *)
    PTR(al',protect_array_type al dim d')
    (* array dim of ptr to function returning d' is d' ( *foo[dim]()) *)
  | PROTO(d',args,ghost_args,variadic) ->
    PROTO(protect_array_type al dim d',args,ghost_args, variadic)

(* creates a *d. Similar issue as for protect_array_type. *)
let rec protect_ptr_type al d =
  match d with
  | JUSTBASE -> PTR(al,d)
  | PARENTYPE(al1,d',al2) -> PARENTYPE(al1,protect_ptr_type al d', al2)
  | ARRAY(d',al',dim') ->
    (* pointer to array dim of d is d ( *foo)[dim] *)
    ARRAY(PARENTYPE([],protect_ptr_type al d',[]),al',dim')
  | PTR(al',d') -> PTR(al', protect_ptr_type al d')
  | PROTO _ ->
    (* pointer to function is handled differently. Here, we have a function
       returning a pointer to something else. *)
    PTR (al, d)

let spec_type t = SpecType t

let spec_of_ikind s =
  Cil_types.(
    match s with
      | IBool -> [ SpecType Tbool ]
      | IChar -> [ SpecType Tchar ]
      | ISChar -> [ SpecType Tsigned; SpecType Tchar ]
      | IUChar -> [ SpecType Tunsigned; SpecType Tchar ]
      | IInt -> [ SpecType Tint ]
      | IUInt -> [ SpecType Tunsigned ]
      | IShort -> [ SpecType Tshort ]
      | IUShort -> [ SpecType Tunsigned; SpecType Tshort ]
      | ILong -> [ SpecType Tlong ]
      | IULong -> [ SpecType Tunsigned; SpecType Tlong ]
      | ILongLong -> [ SpecType Tlong; SpecType Tlong ]
      | IULongLong -> [ SpecType Tunsigned; SpecType Tlong; SpecType Tlong ]
  )

let make_integral_constant_kind k v =
  let v = Integer.to_string v in
  let s =
    match k with
      | IBool
      | IChar_s | ISChar | IWChar_s | IWSChar
      | IChar | IWChar | IShort | IInt -> ""
      | IChar_u | IUChar | IChar16 | IChar32 | IWChar_u | IWUChar
      | IUShort | IUInt -> "U"
      | ILong -> "L"
      | IULong -> "UL"
      | ILongLong -> "LL"
      | IULongLong -> "ULL"
  in CONST_INT (v ^ s)

let is_unsigned_kind = function
  | IBool -> true (* standard says that bool is neither signed nor unsigned,
                     but at some point you have to take sides. *)
  | IChar_s | ISChar | IWChar_s | IWSChar -> false
  | IChar | IWChar -> Cil.theMachine.theMachine.char_is_unsigned
  | IShort | IInt -> false
  | IChar_u | IUChar | IChar16 | IChar32 | IWChar_u | IWUChar
  | IUShort | IUInt -> true
  | ILong | ILongLong -> false
  | IULong | IULongLong -> true

let mk_expr_l expr_loc expr_node = { expr_loc; expr_node }

let mk_expr env node = mk_expr_l (Convert_env.get_loc env) node

let mk_cast_n typ e = CAST (typ, SINGLE_INIT e)

let mk_cast env typ e = mk_expr env (mk_cast_n typ e)

let mk_var_l loc name = mk_expr_l loc (VARIABLE name)

let mk_var env name = mk_expr env (VARIABLE name)

let mk_addrof env e = mk_expr env (UNARY(ADDROF,e))

let mk_int64_cst_n env ?(kind=IInt) i =
  let mk_node i = CONSTANT (make_integral_constant_kind kind i) in
  let mk_node_64 i = mk_node (Integer.of_int64 i) in
  let mk_exp_64 i = mk_expr env (mk_node_64 i) in
  if i < Int64.zero then begin
    if is_unsigned_kind kind then begin
      (* must convert back into unsigned version. *)
      let v = Integer.of_int64 i in
      let v =
        Integer.(add (neg (mul (of_int 2) (of_int64 Int64.min_int)))) v
      in
      mk_node v
    end else if i = Int64.min_int then begin
      let m = Int64.neg (Int64.succ i) in
      BINARY(
        SUB, mk_expr env (UNARY (MINUS, (mk_exp_64 m))), mk_exp_64 Int64.one)
    end else UNARY(MINUS, mk_exp_64 (Int64.neg i))
  end else mk_node_64 i

let mk_int64_cst env ?kind i = mk_expr env (mk_int64_cst_n env ?kind i)

let mk_zero ?kind env = (mk_int64_cst env ?kind Int64.zero)

let mk_assign env dst src = mk_expr env (BINARY(ASSIGN, dst, src))

let make_closure_access env id_name is_ref =
  let access = MEMBEROFPTR (mk_var env closure_name, id_name) in
  if is_ref then UNARY(MEMOF,mk_expr env access) else access

let mk_signature res_type param_types =
  { result = res_type; parameter = param_types; variadic = false }

let mk_arg_decl ty name loc =
  { arg_type = ty; arg_name = name; arg_loc = loc; }

let convert_variable env = function
  | Local({ decl_name = "__func__" }) ->
    CONSTANT(CONST_STRING (Convert_env.get_current_func_name env))
  | Local n ->
    (match Convert_env.closure_var_kind env n.decl_name with
     | None -> VARIABLE n.decl_name
     | Some is_ref -> make_closure_access env n.decl_name is_ref)
  | Global n ->
    let (is_extern_c,_) = Convert_env.get_global_var env n in
    let cname =
      if is_extern_c then n.decl_name else Mangling.mangle n TStandard None
    in
    VARIABLE cname
  | FunctionParameter n ->
    (match Convert_env.closure_var_kind env n with
     | None -> VARIABLE n
     | Some is_ref -> make_closure_access env n is_ref)
  | CodePointer (n,signature,kind,is_extern_c,tm) ->
    let cname =
      if is_extern_c then n.decl_name
      else
        let n, tm = Convert_env.typedef_normalize env n tm in
        let signature = Convert_env.signature_normalize env signature in
        Mangling.mangle n tm (Some (kind,signature))
    in VARIABLE cname

let convert_binary kind assgn e1 e2 =
  match kind,assgn with
    | BOPlus, AKRValue -> BINARY(ADD,e1,e2)
    | BOPlus, AKAssign -> BINARY(ADD_ASSIGN,e1,e2)
    | BOMinus, AKRValue -> BINARY(SUB,e1,e2)
    | BOMinus, AKAssign -> BINARY(SUB_ASSIGN,e1,e2)
    | BOLess, AKRValue -> BINARY(LT,e1,e2)
    | BOLessOrEqual, AKRValue -> BINARY(LE, e1, e2)
    | BOEqual, AKRValue -> BINARY(EQ,e1,e2)
    | BODifferent, AKRValue -> BINARY(NE,e1,e2)
    | BOGreaterOrEqual, AKRValue -> BINARY(GE,e1,e2)
    | BOGreater, AKRValue -> BINARY(GT,e1,e2)
    | BOTimes, AKRValue -> BINARY(MUL,e1,e2)
    | BOTimes, AKAssign -> BINARY(MUL_ASSIGN,e1,e2)
    | BODivide, AKRValue -> BINARY(DIV,e1,e2)
    | BODivide, AKAssign -> BINARY(DIV_ASSIGN,e1,e2)
    | BOModulo, AKRValue -> BINARY(MOD,e1,e2)
    | BOModulo, AKAssign -> BINARY(MOD_ASSIGN,e1,e2)
    | BOBitOr, AKRValue -> BINARY(BOR,e1,e2)
    | BOBitOr, AKAssign -> BINARY(BOR_ASSIGN,e1,e2)
    | BOBitAnd, AKRValue -> BINARY(BAND,e1,e2)
    | BOBitAnd, AKAssign -> BINARY(BAND_ASSIGN,e1,e2)
    | BOBitExclusiveOr, AKRValue -> BINARY(XOR,e1,e2)
    | BOBitExclusiveOr, AKAssign -> BINARY(XOR_ASSIGN,e1,e2)
    | BOLeftShift, AKRValue -> BINARY(SHL,e1,e2)
    | BOLeftShift, AKAssign -> BINARY(SHL_ASSIGN,e1,e2)
    | BORightShift, AKRValue -> BINARY(SHR,e1,e2)
    | BORightShift, AKAssign -> BINARY(SHR_ASSIGN,e1,e2)
    | BOLogicalAnd, AKRValue -> BINARY(AND,e1,e2)
    | BOLogicalOr, AKRValue -> BINARY(OR,e1,e2)
    | BOComma, AKRValue -> COMMA [e1;e2]
    | _, AKAssign ->
        Frama_Clang_option.fatal
          "Binary operator is not supposed to have an assign kind"

let is_bin_assign = function
  | ADD | SUB | MUL | DIV | MOD | AND | OR | BAND | BOR | XOR
  | SHL | SHR | EQ | NE | LT | GT | LE | GE
    -> false
  | ASSIGN | ADD_ASSIGN | SUB_ASSIGN | MUL_ASSIGN | DIV_ASSIGN | MOD_ASSIGN
  | BAND_ASSIGN | BOR_ASSIGN | XOR_ASSIGN | SHL_ASSIGN | SHR_ASSIGN
    -> true

let is_unary_assign = function
  | MINUS | PLUS | NOT | BNOT | MEMOF | ADDROF -> false
  | PREINCR | PREDECR | POSINCR | POSDECR -> true

let rec make_addrof e =
  match e.expr_node with
    | VARIABLE _ | INDEX _ | MEMBEROF _ | MEMBEROFPTR _ ->
       { e with expr_node = UNARY(ADDROF,e) }
    (* I think this is handled well by cabs2cil. *)
    | QUESTION _ -> { e with expr_node = UNARY(ADDROF,e) }
    | CAST(_,SINGLE_INIT e) -> make_addrof e
    | PAREN e -> make_addrof e
    | BINARY(a, e1, _) when is_bin_assign a ->
        { e with expr_node = COMMA [ e; make_addrof e1 ] }
    | UNARY(MEMOF, e) -> e
    | UNARY(a, e1) when is_unary_assign a ->
        { e with expr_node = COMMA [ e; make_addrof e1 ] }
    | COMMA l ->
        (match List.rev l with
           | [] ->
               Frama_Clang_option.fatal
                 "Trying to take the address of an empty expression"
           | a::l ->
               { e with expr_node = COMMA (List.rev ((make_addrof a) :: l))})
    | NOTHING | UNARY _ | LABELADDR _ | BINARY _ | CALL _ | CONSTANT _
    | EXPR_SIZEOF _ | TYPE_SIZEOF _ | EXPR_ALIGNOF _ | TYPE_ALIGNOF _
    | GNU_BODY _ | EXPR_PATTERN _ | CAST _ | GENERIC _ ->
      Frama_Clang_option.fatal
        "Cannot take the address of a non-lval expression"

let is_builtin_va_list = function
  | Named({ decl_name = "__builtin_va_list"}, _) -> true
  | _ -> false

let rec convert_ref env typ expr =
  match typ, expr with
  (* special case for va_list. *)
  | (LVReference (PDataPointer ty)
    | RVReference (PDataPointer ty)), e
    when is_builtin_va_list ty.plain_type -> e
  | (LVReference _ | RVReference _), { expr_node = UNARY(MEMOF,e) } -> e
  | (LVReference _ | RVReference _), { expr_node = CAST(_,SINGLE_INIT e) } ->
      make_addrof e
  | (LVReference _ | RVReference _), _ -> make_addrof expr
  | Named (ty, _), _
      -> if Convert_env.has_typedef env ty
         then convert_ref env (Convert_env.get_typedef env ty).plain_type expr
         else expr
  | _, _ -> expr

let convert_reference_parameters env variadic prms args =
  let convert_ref typ arg = convert_ref env typ.plain_type arg in
  let rec convert = function
    | [], [] -> []
    | [], args when variadic -> args
    | prm::prms, arg::args -> convert_ref prm arg :: convert (prms,args)
    | _ ->
      Convert_env.fatal env
        "Wrong number of arguments in function call (expected %d, got %d)"
        (List.length prms) (List.length args)
  in
  convert (prms, args)

let rec is_constructor_call e =
 match e.econtent with
   | Static_call (_, _, FKConstructor _, _, _,_) -> true
   | Unary_operator(UOCastNoEffect _,e) -> is_constructor_call e
   | _ -> false

let rec extract_constructor_call e =
  match e.econtent with
    | Static_call (name, sigtype, (FKConstructor _ as kind), args, tn, _) ->
      (kind, name, tn, sigtype, args)
    | Unary_operator(UOCastNoEffect _,e) -> extract_constructor_call e
    | _ -> Frama_Clang_option.fatal "Not a constructor"

let add_attr env name args =
  let expr_loc = Convert_env.get_loc env in
  let name = { expr_loc; expr_node = VARIABLE name } in
  let payload =
    match args with
    | [] -> name
    | _ -> { expr_loc; expr_node = CALL (name, args, []) }
  in
  ("__declspec", [ payload ])

let add_fc_destructor_attr env typ attrs =
  let expr_loc = Convert_env.get_loc env in
  match (Convert_env.qual_type_normalize env typ).plain_type with
  | Struct (n,args) when Convert_env.has_destructor env (n,args) ->
    let name =
      Mangling.mangle
        (Cxx_utils.meth_name n args ("~" ^ n.decl_name))
        TStandard
        (Some
           (FKDestructor true,
            { result = Cxx_utils.unqual_type Void;
              parameter = [];
              variadic = false;
            }))
    in
    let arg =
      { expr_loc;
        expr_node =
          UNARY(
            ADDROF,
            { expr_loc; expr_node = CONSTANT (CONST_STRING name)})}
    in
    let attr = add_attr env Cabs2cil.frama_c_destructor [arg] in
    attr :: attrs
  | _ -> attrs

let rm_fc_destructor_attr attrs =
  List.filter
    (fun (name,content) ->
       name <> "__declspec" ||
       (match content with
        | [ { expr_node = CALL ({ expr_node = VARIABLE n }, _, _)}] ->
          n <> Cabs2cil.frama_c_destructor
        | _ -> true))
    attrs

let add_temporary (* env *) e =
  if is_constructor_call e then
    let (kind, cons,tc,signature,args) = extract_constructor_call e in
    let e =
      { e with econtent
            = Static_call(cons,signature,kind,args,tc,false)
      }
    in e
  else e

(* some temporary might be needed. Note that their list is returned reverted.
   convert_full_expr takes care of putting it in the good order. *)
let var_name s =
  let counter = ref (-1) in
  fun () -> incr counter; s ^ "_" ^ string_of_int !counter

let shift_ptr_var_name = var_name "__cast_tmp"
let virtual_var_name = var_name "__virtual_tmp"
let shift_object_name = var_name "__shift_object"

let find_loc_list f l =
  match l with
    | [] -> Lexing.dummy_pos, Lexing.dummy_pos
    | [ s ] -> f s
    | s :: l ->
        let (beg_loc,_) = f s in
        let rec aux = function
          | [] -> assert false
          | [ s ] ->
              let (_,end_loc) = f s in
              (beg_loc, end_loc)
          | _::l -> aux l
        in
        aux l

let find_loc_stmt =
  function
    | Nop l -> l
    | Return (l,_) -> l
    | Expression (l,_) -> l
    | VirtualExpression (l,_) -> l
    | Ghost_block(l,_) -> l
    | Block (l,_) -> l
    | Condition (l,_,_,_) -> l
    | Label(l,_) -> l
    | Goto(l,_) -> l
    | Switch(l,_,_) -> l
    | VarDecl(l,_,_,_) -> l
    | Break l -> l
    | Continue l -> l
    | While(l,_,_,_) -> l
    | DoWhile(l,_,_,_) -> l
    | For(l,_,_,_,_,_) -> l
    | Code_annot(l,_) -> l
    | TryCatch(l,_,_) -> l
    | GccInlineAsm(l,_,_,_) -> l

let find_loc_list_stmt = find_loc_list find_loc_stmt

let find_loc_case_stmt =
  function
    | Case(_,l) | Default l -> find_loc_list_stmt l

let find_loc_case_stmt_list = find_loc_list find_loc_case_stmt

let empty_aux = []

let merge_aux aux1 aux2 = aux1 @ aux2

let add_local_aux_def defs def = (Some def, None) :: defs

let add_local_aux_def_init defs def init = (Some def, Some init) :: defs

let add_local_aux_init defs init = (None, Some init) :: defs

let add_temp env stmts (dec, init) =
  let stmts =
    match init with
      | None -> stmts
      | Some init -> init :: stmts
  in
  match dec with
    | None -> stmts
    | Some dec -> (make_stmt env (DEFINITION dec)) :: stmts

let add_temp_update env acc (dec,inits) =
  (* We have three possibilities:
     - no definition and a statement
     - a single init expression in the definition and no init statement
     - no init expression and an init statement *)
  match dec with
    | None ->
      (match inits with
        | None -> acc
        | Some s -> s :: acc)
    | Some (DECDEF(_,(_,[(name,_,_,_),inite]),_)) ->
      let stmt =
        match inite, inits with
          | SINGLE_INIT e, None ->
            make_stmt env
              (COMPUTATION(
                  mk_expr env (BINARY(ASSIGN, mk_expr env (VARIABLE name), e)),
                  Convert_env.get_loc env))
          | NO_INIT, Some s -> s
          | _ ->
            Convert_env.fatal env "Unexpected initialization for a temporary"
      in
      stmt :: acc
    | _ -> Convert_env.fatal env "Unexpected definition for a temporary"

let mk_compound_init env lv typ init =
  let loc = Convert_env.get_loc env in
  let rec aux acc lv typ init =
    match init with
    | SINGLE_INIT def ->
      COMPUTATION (
        { expr_loc = def.expr_loc; expr_node = BINARY(ASSIGN,lv,def)},
        def.expr_loc)
      :: acc
    | NO_INIT -> NOP loc :: acc
    | COMPOUND_INIT l ->
      (match typ.plain_type with
       | Array { subtype } ->
         let rec aux_array acc i l =
           match l with
           | [] -> acc
           | (what,init) :: l ->
             (* translation scheme uses that for now. *)
             assert (what = NEXT_INIT);
             let lv =
               { expr_loc = lv.expr_loc;
                 expr_node =
                   INDEX(
                     lv,
                     { expr_loc = lv.expr_loc;
                       expr_node = CONSTANT (CONST_INT (string_of_int i))})}
             in
             aux_array (aux acc lv subtype init) (i+1) l
         in
         aux_array acc 0 l
       | Struct (name, tk) ->
         let rec aux_struct acc lfields linit =
           match lfields, linit with
           | _,[] -> acc
           | [],_ ->
             Convert_env.fatal
               env "Too many initializers for class %a"
               Fclang_datatype.Qualified_name.pretty (name,tk)
           | (fname,ftype)::lfields, (what,i)::linit ->
             assert (what = NEXT_INIT);
             let lv = {expr_loc=lv.expr_loc; expr_node=MEMBEROF(lv,fname)} in
             aux_struct (aux acc lv ftype i) lfields linit
         in
         aux_struct acc (Convert_env.get_struct env (name,tk)) l
       | _ -> Convert_env.fatal env "Compound init on a scalar type")
  in
  let init_stmts = aux [] lv typ init in
  match init_stmts with
  | [] -> assert false (* at least one initialization is supposed to occur. *)
  | [ single_init ] -> single_init
  | l -> let l = List.rev_map (make_stmt env) l in make_block env l

let computation_or_nop loc exp =
  match exp.expr_node with
  | NOTHING -> NOP loc
  | _ -> COMPUTATION(exp,loc)

let preserved_returned_object aux e =
  match e.expr_node with
  | VARIABLE n ->
    let transf (d,s as res) =
      match d with
      | Some (DECDEF(spec,(t,l),loc)) ->
        let change_name ((n',decl,attrs,loc),init as res) =
          if n <> n' then res
          else
            ((n,decl,rm_fc_destructor_attr attrs,loc),init)
        in
        let l' = List.map change_name l in
        Some (DECDEF(spec,(t,l'),loc)),s
      | _ -> res
    in
    List.map transf aux
  | _ -> aux

let rec convert_base_type env spec decl typ does_remove_virtual =
  match typ with
  | Void -> spec_type Tvoid :: spec, decl
  | Int IBool -> spec_type Tbool :: spec, decl
  | Int (IChar_u | IChar_s | IChar) -> spec_type Tchar :: spec, decl
  | Int IUChar -> (List.map spec_type [Tunsigned; Tchar]) @ spec, decl
  | Int ISChar -> (List.map spec_type [Tsigned; Tchar ]) @ spec, decl
    (* TODO: intKindForSize returns a type of exactly 16 bits. There is no
       function for providing an ikind of at least 16 bits yet. This should
       be added to Cil. Indeed, it could theoretically be possible that
       intKindForSize 2 fails while there exist types of a strictly
       greater size. *)
  | Int IChar16 -> spec_of_ikind (Cil.intKindForSize 2 true) @ spec, decl
  | Int IChar32 -> spec_of_ikind (Cil.intKindForSize 4 true) @ spec, decl
  | Int (IWChar_u | IWChar_s | IWUChar | IWSChar | IWChar ) ->
      let wchar_name = { prequalification=[];decl_name="fc_wchar_t"} in
      let base =
        if Convert_env.has_typedef env wchar_name then begin
          let rep = (Convert_env.get_typedef env wchar_name).plain_type in
          match rep with
            | Named (_,is_extern_c) ->
                let name =
                  if is_extern_c then wchar_name.decl_name
                  else Mangling.mangle wchar_name TStandard None
                in
                [ SpecType (Tnamed name) ]
            | Int _ ->
              let spec,_ =
                convert_base_type env [] decl rep does_remove_virtual
              in
              spec
            | _ ->
                Frama_Clang_option.fatal
                  "wchar_t should be linked to a named or integral type"
        end else
          spec_of_ikind Cil.theMachine.Cil.wcharKind
      in
      base @ spec, decl
  | Int IInt -> spec_type Tint :: spec, decl
  | Int IShort -> spec_type Tshort :: spec, decl
  | Int IUShort -> (List.map spec_type [Tunsigned; Tshort ]) @ spec, decl
  | Int IUInt -> (List.map spec_type [Tunsigned; Tint]) @ spec, decl
  | Int ILong -> spec_type Tlong :: spec, decl
  | Int IULong -> (List.map spec_type [Tunsigned; Tlong]) @ spec,decl
  | Int ILongLong -> (List.map spec_type [Tlong; Tlong]) @ spec,decl
  | Int IULongLong ->
    (List.map spec_type [Tunsigned; Tlong; Tlong]) @ spec,decl
  | Float FFloat -> spec_type Tfloat :: spec, decl
  | Float FDouble -> spec_type Tdouble :: spec, decl
  | Float FLongDouble -> (List.map spec_type [Tlong; Tdouble]) @ spec, decl
  | Enum e ->
    let body_name, t = Convert_env.typedef_normalize env e.body TStandard in
    let name =
      if e.ekind_is_extern_c then body_name.decl_name
      else Mangling.mangle body_name t None
    in
    spec_type (Tenum(name,None,[]))::spec, decl
  | Struct (s,t) ->
    let name =
      if Convert_env.is_extern_c_aggregate env s t then s.decl_name
      else
        let s, t = Convert_env.typedef_normalize env s t in
        Mangling.mangle s t None
    in
    spec_type (Tstruct (name, None, [])) :: spec, decl
  | Union (s,t) ->
    let name =
      if Convert_env.is_extern_c_aggregate env s t then s.decl_name
      else
        let s, t = Convert_env.typedef_normalize env s t in
        Mangling.mangle s t None
    in
    spec_type (Tunion (name, None, [])) :: spec, decl
  | Pointer (PDataPointer t) ->
    let attrs = List.map cv_to_attr spec in
    let decl d = decl (protect_ptr_type attrs d) in
    convert_type env decl t does_remove_virtual
  | LVReference (PDataPointer t) | RVReference(PDataPointer t)->
    let attrs = List.map cv_to_attr spec in
    convert_type
      env (fun d -> decl (protect_ptr_type attrs d)) t does_remove_virtual
  | Pointer (PFunctionPointer s) ->
    let rt, rt_decl, args, variadic =
      convert_fptr env s does_remove_virtual
    in
    let attrs = List.map cv_to_attr spec in
    rt,
    (fun d ->
      rt_decl
        (PROTO (decl (protect_ptr_type attrs d), args,[],variadic)))
  | LVReference (PFunctionPointer s)
  | RVReference (PFunctionPointer s) ->
    let rt, rt_decl, args, variadic =
      convert_fptr env s does_remove_virtual
    in
    let attrs= List.map cv_to_attr spec in
    rt,
    (fun d ->
       rt_decl (PROTO (decl (protect_ptr_type attrs d),args,[],variadic)))
  | Pointer(PStandardMethodPointer _)
  | LVReference (PStandardMethodPointer _)
  | RVReference (PStandardMethodPointer _) ->
      Frama_Clang_option.not_yet_implemented "pointer to member"
  | Pointer(PVirtualMethodPointer _)
  | LVReference (PVirtualMethodPointer _)
  | RVReference (PVirtualMethodPointer _) ->
      Frama_Clang_option.not_yet_implemented "pointer to member"
  | Array a ->
    let get_array_cv_attribute = function
      | SpecCV _ as cv -> Some (cv_to_attr cv)
      | _ -> None
    in
    let attrs = List.filter_map get_array_cv_attribute spec in
      convert_type
        env
        (fun d ->
          let dim =
            Option.fold
              ~some:(fun e ->
                  let _,_,ce =
                    convert_expr env empty_aux e does_remove_virtual
                  in
                  ce.expr_node)
              ~none:NOTHING
              a.dimension
          in
          let exp =
            { expr_loc = Cil_datatype.Location.unknown; expr_node = dim }
          in
          decl (protect_array_type attrs exp d))
        a.subtype
        does_remove_virtual
  | Named (name, is_extern_c_name) ->
    let cname =
      if Cxx_utils.is_builtin_qual_type name then name.decl_name
      else if is_extern_c_name
      then name.decl_name
      else
        let name, t = Convert_env.typedef_normalize env name TStandard in
        Mangling.mangle name t None
    in
    spec_type (Tnamed cname)::spec, decl
  | Lambda _ ->
    let type_name = Mangling.mangle_cc_type typ in
    (SpecType (Tstruct (type_name, None, []))) :: spec, decl

and convert_type env decl t does_remove_virtual =
  let spec = List.map convert_cv t.qualifier in
  convert_base_type env spec decl t.plain_type does_remove_virtual

and convert_fptr env s does_remove_virtual =
  let args, variadic =
    if s.variadic && s.parameter = [] then [], false
    else
      convert_signature env s.parameter does_remove_virtual, s.variadic
  in
  let rt, rt_decl =
    convert_specifiers env s.result does_remove_virtual
  in
  rt, rt_decl, args, variadic

and convert_signature env l does_remove_virtual =
  match l with
    | [] ->
      (* in C++, an empty list is strictly equivalent to (void), i.e. no
         argument at all. In C, a prototype with no argument means that the
         arguments are not specified, so that a subsequent declaration could
         provides one or more arguments. We thus normalize that to (void) for
         the C translation.
       *)
      [ [SpecType Tvoid],("",JUSTBASE,[],Convert_env.get_loc env) ]
    | _ -> List.map (convert_anonymous_decl env does_remove_virtual) l

and convert_specifiers env t does_remove_virtual =
  let spec = List.map convert_cv t.qualifier in
  convert_base_type env spec (fun d -> d) t.plain_type does_remove_virtual

and convert_anonymous_decl env does_remove_virtual t =
  let typ, decl = convert_specifiers env t does_remove_virtual in
  (typ, ("",decl JUSTBASE,[],Cil_datatype.Location.unknown))

and convert_decl env does_remove_virtual arg =
  let typ,decl = convert_specifiers env arg.arg_type does_remove_virtual in
  (typ,
   (arg.arg_name, decl JUSTBASE, [],
    Cil_datatype.Location.of_lexing_loc arg.arg_loc))

and make_prototype loc env name kind rt args variadic does_remove_virtual =
  let rt, decl = convert_specifiers env rt does_remove_virtual in
  let args =
    match args with
      | [] -> (* empty list in C++ always mean void, not unspecified *)
        [[SpecType Tvoid],("",JUSTBASE,[],loc)]
      | _ -> List.map (convert_decl env does_remove_virtual) args
  in
  let args =
    match kind, args with
    | FKConstructor _, (spec, name) :: args' ->
      (SpecAttr (add_attr env Cil.frama_c_init_obj []) :: spec, name) :: args'
    | _ -> args
  in
  env, (rt, (name,decl (PROTO(JUSTBASE,args,[],variadic)),[],loc))

and convert_constant env c does_remove_virtual = match c with
  | IntCst (kind,_,v) -> mk_int64_cst_n env ~kind v
  | FloatCst(_,v) -> CONSTANT(CONST_FLOAT v)
  | EnumCst(n,e,_) ->
    let n, t = Convert_env.typedef_normalize env n TStandard in
    let name =
      if e.ekind_is_extern_c then n.decl_name else Mangling.mangle n t None
    in
    let body_name, t' = Convert_env.typedef_normalize env e.body TStandard in
    let enum =
      if e.ekind_is_extern_c then body_name.decl_name
      else Mangling.mangle body_name t' None
    in
    (* C++ enum constant are of type Enum, while C treat them as integers.
       This is not an issue for most purposes, except when it comes to
       handle exceptions: catching enum e is not the same as catching int x.
     *)
    mk_cast_n ([SpecType (Tenum (enum,None,[]))], JUSTBASE) (mk_var env name)
  | TypeCst (TCCSizeOf, t) ->
    let bt,decl = convert_base_type env [] id t does_remove_virtual in
    TYPE_SIZEOF (bt,decl JUSTBASE)
  | TypeCst (TCCAlignOf, t) ->
    let bt,decl = convert_base_type env [] id t does_remove_virtual in
    TYPE_ALIGNOF (bt,decl JUSTBASE)

and convert_unary env kind arg does_remove_virtual =
  match kind with
    (* Not a real cast, merely a compilation's artifact *)
    | UOCastNoEffect _ -> arg.expr_node
    (* Marks initialization of a ref field. treated elsewhere. *)
    | UOCastDerefInit -> arg.expr_node
    (* Use the actual rvalue of a reference. *)
    | UOCastDeref -> UNARY(MEMOF,arg)
    | UOCastToVoid -> mk_cast_n ([SpecType Tvoid], JUSTBASE) arg
    | UOCastInteger(t,_)
    | UOCastEnum(t,_) | UOCastFloat(t,_) | UOCastC t ->
      let rt, decl = convert_specifiers env t does_remove_virtual in
      mk_cast_n (rt, decl JUSTBASE) arg
    | UOPostInc -> UNARY(POSINCR,arg)
    | UOPostDec -> UNARY(POSDECR,arg)
    | UOPreInc  -> UNARY(PREINCR,arg)
    | UOPreDec  -> UNARY(PREDECR,arg)
    | UOOpposite -> UNARY(MINUS,arg)
    | UOBitNegate -> UNARY(BNOT,arg)
    | UOLogicalNegate -> UNARY(NOT,arg)

(* drop_temp is true when the resulting value is not considered further,
   i.e. the expression is evaluated only for its side effect. In this setting,
   temporaries will be translated as NOTHING, since computations occur in the
   tmps instructions and not the returned expression.
*)
and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
  let create_this_access e origin_type aux env is_reference noeffect =
    if (noeffect)
    then e, aux, env
    else begin
      let derived_name, td
        = if not is_reference
          then Convert_env.get_class_name_from_pointer env
            origin_type.plain_type
          else let derived_name, td, _ =
            Convert_env.get_class_name_from_reference env
              origin_type.plain_type
          in derived_name, td
      in
      let var_name = shift_ptr_var_name () in
      let env =
        Convert_env.add_local_var env var_name
          Cxx_utils.(
            plain_obj_ptr (unqual_type (Struct (derived_name,td))))
      in
      let derived_name, td =
        Convert_env.typedef_normalize env derived_name td
      in
      let init =
        if not is_reference then e else mk_expr env (UNARY(ADDROF, e))
      in
      let aux =
        add_local_aux_def aux
          (DECDEF(
              None,
              ([SpecType
                  (Tstruct
                     (Mangling.mangle derived_name td None, None, []))],
               [(var_name, PTR([], JUSTBASE),[], e.expr_loc),
                SINGLE_INIT(init)]), e.expr_loc))
      in
        mk_expr env (VARIABLE var_name), aux, env
    end
  in
  let create_table_access access aux env noeffect =
    if (noeffect) then access, aux, env
    else begin
      let table_access = virtual_var_name () in
      let qual_vmt_content_name = Cxx_utils.empty_qual "_frama_c_vmt_content" in
      let env =
        Convert_env.add_local_var env table_access
          Cxx_utils.(
            plain_obj_ptr (
              unqual_type (Struct (qual_vmt_content_name, TStandard))))
      in
      let qual_vmt_content_name, _ =
        Convert_env.typedef_normalize env qual_vmt_content_name TStandard
      in
      let tmp_decl = DECDEF( None,
       ([SpecType (Tstruct (Mangling.mangle
           qual_vmt_content_name TStandard None, None, []))],
         [(table_access,PTR( [], JUSTBASE),[],access.expr_loc),
           SINGLE_INIT (access)]),
       access.expr_loc)
      in
      let aux = add_local_aux_def aux tmp_decl in
      (mk_expr env (VARIABLE table_access)), aux, env
    end
  in
  let create_shift_object aux env loc =
    let var_name = shift_object_name () in
    let env =
      Convert_env.add_local_var
        env var_name Cxx_utils.(plain_obj_ptr(unqual_type (Int IInt)))
      in
      let def =
        DECDEF(
          None,
          ([SpecType Tint],
           [(var_name, JUSTBASE, [], loc),
            SINGLE_INIT (mk_expr env (CONSTANT (CONST_INT "0")))]), loc)
      in
      let aux = add_local_aux_def aux def in
      mk_expr env (VARIABLE var_name), aux, env
  in
  let env, aux, node =
    match e with
      | Constant c ->
        let e = convert_constant env c does_remove_virtual in env, aux, e
      | String s -> env, aux, CONSTANT (CONST_STRING s)
      | Variable v -> env, aux, convert_variable env v
      | Malloc(t) ->
          let bt,decl = convert_base_type env [] id t does_remove_virtual in
          env,
          aux,
          CALL(mk_expr env (VARIABLE "malloc"),
               [mk_expr env (TYPE_SIZEOF (bt,decl JUSTBASE))],[])
      | MallocArray(t,s) ->
          let bt,decl = convert_base_type env [] id t does_remove_virtual in
          let env, aux, size = convert_expr env aux s does_remove_virtual in
          env,
          aux,
          CALL(
            mk_expr env (VARIABLE "malloc"),
            [mk_expr env
               (BINARY
                  (MUL,
                   mk_expr env (TYPE_SIZEOF(bt,decl JUSTBASE)),size))], [])
      | Free e | FreeArray e ->
          let env, aux, arg = convert_expr env aux e does_remove_virtual in
          env, aux, CALL(mk_expr env (VARIABLE "free"),[arg],[])
      | Assign(x,e) when is_constructor_call e ->
        let kind, name, tn, sigtype, args = extract_constructor_call e in
        let e =
          { e with
            econtent =
              Static_call(name, sigtype, kind,
                { x with econtent = Address x}::args, tn, false)}
        in
        let env, aux, e = convert_expr env aux e does_remove_virtual in
        env, aux, e.expr_node
      (* Initialization of a reference with a reference:
         don't apply the derefs. *)
      | Assign({ econtent = Unary_operator (UOCastDerefInit, x) },e) ->
        let env, aux, lv = convert_expr env aux x does_remove_virtual in
        let env, aux, rv = convert_expr env aux e does_remove_virtual in
        let rv = mk_addrof env rv in
        env, aux, BINARY(ASSIGN,lv,rv)
      | Assign(x,e) ->
          let env, aux, lv = convert_expr env aux x does_remove_virtual in
          let env, aux, rv = convert_expr env aux e does_remove_virtual in
          env, aux, BINARY(ASSIGN,lv,rv)
      | Unary_operator(k,e) ->
          let env, aux, e = convert_expr env aux e does_remove_virtual in
          let e = convert_unary env k e does_remove_virtual in
          env, aux, e
      | Binary_operator(k,a,e1,e2) ->
          let env, aux, e1 = convert_expr env aux e1 does_remove_virtual in
          let env, aux, e2 = convert_expr env aux e2 does_remove_virtual in
          env, aux, convert_binary k a e1 e2
      | Dereference e ->
          let env, aux, e = convert_expr env aux e does_remove_virtual in
          env, aux, UNARY(MEMOF,e)
      | Address e ->
          let env, aux, e = convert_expr env aux e does_remove_virtual in
          env, aux, (make_addrof e).expr_node
      | PointerCast(target,base,e) ->
          let env, aux, e = convert_expr env aux e does_remove_virtual in
          let rt, decl = convert_specifiers env target does_remove_virtual in
            (match base with
              | RPKPointer ->
                  env, aux, mk_cast_n (rt,decl JUSTBASE) e
              | RPKReference ->
                  env, aux,
                  UNARY(
                    MEMOF,
                    mk_cast
                      env (rt,decl JUSTBASE) (mk_expr env (UNARY(ADDROF,e))))
              | RPKStaticBasePointer ->
                let (base_class_name, t) =
                  Convert_env.get_class_name_from_pointer env target.plain_type
                in let (base_class_name, t) =