convert.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-Clang                                      *)
(*                                                                        *)
(*  Copyright (C) 2012-2025                                               *)
(*    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

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 () =
  Ast_attributes.(register (AttrName false) fc_implicit_attr);
  Ast_attributes.(register (AttrName false) fc_pure_template_decl_attr)

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 make_integral_constant_kind k v =
  let v = Integer.to_string v in
  let s =
    match k with
    | IBool
    | IChar_s | ISChar | IWChar_s
    | IChar | IWChar | IShort | IInt -> ""
    | IChar_u | IUChar | IChar16 | IChar32 | IWChar_u
    | 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 -> false
  | IChar | IWChar -> Machine.char_is_unsigned ()
  | IShort | IInt -> false
  | IChar_u | IUChar | IChar16 | IChar32 | IWChar_u
  | 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 _ | 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_class_decl_loc = function
  | CMethod (loc,_,_,_,_,_,_,_,_,_,_,_)
  | CCompound (loc,_,_,_,_,_,_)
  | CFieldDecl (loc,_,_,_,_)
  | CTypedef (loc,_,_)
  | CStaticConst (loc,_,_,_,_)
  | CEnum (loc,_,_,_)
  | Class_annot (loc,_) -> loc

let find_loc_translation_unit_decl = function
  | Function (_,_,loc,_,_,_,_,_,_,_,_,_,_)
  | Compound(loc,_,_,_,_,_,_,_,_)
  | GlobalVarDecl(loc,_,_,_,_,_)
  | Typedef(loc,_,_,_,_)
  | Namespace (loc,_,_)
  | StaticConst (loc,_,_,_,_,_,_)
  | EnumDecl(loc,_,_,_,_,_)
  | GlobalAnnotation(loc,_) -> loc

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 (None, 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 (None, 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 convert_class_name env name tc =
  if Convert_env.is_extern_c_aggregate env name tc then name.decl_name
  else
    let s, t = Convert_env.typedef_normalize env name tc in
    Mangling.mangle s t None

let qual_vmt_content_name = Cxx_utils.empty_qual "_frama_c_vmt_content"
let qual_vmt_name = Cxx_utils.empty_qual "_frama_c_vmt"

let mk_vmt_content_type env =
  let name, tc =
    Convert_env.typedef_normalize env qual_vmt_content_name TStandard
  in
  Tstruct (convert_class_name env name tc, None, [])

let mk_vmt_type env =
  let name, tc = Convert_env.typedef_normalize env qual_vmt_name TStandard in
  Tstruct (convert_class_name env name tc, None, [])

let rec convert_base_type env spec decl typ does_remove_virtual =
  match typ with
  | Void -> env, (spec_type Tvoid :: spec, decl)
  | Int IBool -> env, (spec_type Tbool :: spec, decl)
  | Int (IChar_u | IChar_s | IChar) -> env, (spec_type Tchar :: spec, decl)
  | Int IUChar -> env, ((List.map spec_type [Tunsigned; Tchar]) @ spec, decl)
  | Int ISChar -> env, ((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 ->
    env, (Cxx_utils.spec_of_ikind (Cil.intKindForSize 2 true) @ spec, decl)
  | Int IChar32 ->
    env, (Cxx_utils.spec_of_ikind (Cil.intKindForSize 4 true) @ spec, decl)
  | Int (IWChar_u | IWChar_s | IWChar ) ->
    let env = Convert_env.memo_wchar env in
    env, (SpecType (Tnamed "wchar_t") :: spec, decl)
  | Int IInt -> env, (spec_type Tint :: spec, decl)
  | Int IShort -> env, (spec_type Tshort :: spec, decl)
  | Int IUShort -> env, ((List.map spec_type [Tunsigned; Tshort ]) @ spec, decl)
  | Int IUInt -> env, ((List.map spec_type [Tunsigned; Tint]) @ spec, decl)
  | Int ILong -> env, (spec_type Tlong :: spec, decl)
  | Int IULong -> env, ((List.map spec_type [Tunsigned; Tlong]) @ spec,decl)
  | Int ILongLong -> env, ((List.map spec_type [Tlong; Tlong]) @ spec,decl)
  | Int IULongLong ->
    env, ((List.map spec_type [Tunsigned; Tlong; Tlong]) @ spec,decl)
  | Float FFloat -> env, (spec_type Tfloat :: spec, decl)
  | Float FDouble -> env, (spec_type Tdouble :: spec, decl)
  | Float FLongDouble ->
    env, ((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
    env, (spec_type (Tenum(name,None,[]))::spec, decl)
  | Struct (s,t) ->
    let name = convert_class_name env s t in
    env, (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
    env, (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 env, (rt, rt_decl, args, variadic) =
      convert_fptr env s does_remove_virtual
    in
    let attrs = List.map cv_to_attr spec in
    env,
    (rt,
     (fun d ->
        rt_decl
          (PROTO (decl (protect_ptr_type attrs d), args,[],variadic))))
  | LVReference (PFunctionPointer s)
  | RVReference (PFunctionPointer s) ->
    let env, (rt, rt_decl, args, variadic) =
      convert_fptr env s does_remove_virtual
    in
    let attrs= List.map cv_to_attr spec in
    env,
    (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
    env, (spec_type (Tnamed cname)::spec, decl)
  | Lambda _ ->
    let type_name = Mangling.mangle_cc_type typ in
    env, ((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 env, (args, variadic) =
    if s.variadic && s.parameter = [] then env, ([], false)
    else
      let env, l = convert_signature env s.parameter does_remove_virtual in
      env, (l, s.variadic)
  in
  let env, (rt, rt_decl) =
    convert_specifiers env s.result does_remove_virtual
  in
  env, (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.
    *)
    env, [ [SpecType Tvoid],("",JUSTBASE,[],Convert_env.get_loc env) ]
  | _ ->
    let do_one env d = convert_anonymous_decl env does_remove_virtual d in
    Convert_env.env_map do_one env 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 env, (typ, decl) = convert_specifiers env t does_remove_virtual in
  env, (typ, ("",decl JUSTBASE,[],Cil_datatype.Location.unknown))

and convert_decl env does_remove_virtual arg =
  let env, (typ,decl) =
    convert_specifiers env arg.arg_type does_remove_virtual
  in
  env,
  (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 env, (rt, decl) = convert_specifiers env rt does_remove_virtual in
  let env, args =
    match args with
    | [] -> (* empty list in C++ always mean void, not unspecified *)
      env, [[SpecType Tvoid],("",JUSTBASE,[],loc)]
    | _ ->
      let do_one env arg = convert_decl env does_remove_virtual arg in
      Convert_env.env_map do_one env args
  in
  let args =
    match kind, args with
    | FKConstructor _, (spec, name) :: args' ->
      (SpecAttr (add_attr env Ast_attributes.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) -> env, mk_int64_cst_n env ~kind v
  | FloatCst(_,v) -> env, 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.
    *)
    env,
    mk_cast_n ([SpecType (Tenum (enum,None,[]))], JUSTBASE) (mk_var env name)
  | TypeCst (TCCSizeOf, t) ->
    let env, (bt,decl) = convert_base_type env [] id t does_remove_virtual in
    env, TYPE_SIZEOF (bt,decl JUSTBASE)
  | TypeCst (TCCAlignOf, t) ->
    let env, (bt,decl) = convert_base_type env [] id t does_remove_virtual in
    env, 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 _ -> env, arg.expr_node
  (* Marks initialization of a ref field. treated elsewhere. *)
  | UOCastDerefInit -> env, arg.expr_node
  (* Use the actual rvalue of a reference. *)
  | UOCastDeref -> env, UNARY(MEMOF,arg)
  | UOCastToVoid -> env, mk_cast_n ([SpecType Tvoid], JUSTBASE) arg
  | UOCastInteger(t,_)
  | UOCastEnum(t,_) | UOCastFloat(t,_) | UOCastC t ->
    let env, (rt, decl) = convert_specifiers env t does_remove_virtual in
    env, mk_cast_n (rt, decl JUSTBASE) arg
  | UOPostInc -> env, UNARY(POSINCR,arg)
  | UOPostDec -> env, UNARY(POSDECR,arg)
  | UOPreInc  -> env, UNARY(PREINCR,arg)
  | UOPreDec  -> env, UNARY(PREDECR,arg)
  | UOOpposite -> env, UNARY(MINUS,arg)
  | UOBitNegate -> env, UNARY(BNOT,arg)
  | UOLogicalNegate -> env, 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 name = convert_class_name 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 (name,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 env =
        Convert_env.add_local_var env table_access
          Cxx_utils.(
            plain_obj_ptr (
              unqual_type (Struct (qual_vmt_content_name, TStandard))))
      in
      let tmp_decl = DECDEF( None,
                             ([SpecType (mk_vmt_content_type env)],
                              [(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 env, 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 env, (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 env, (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 env, 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 env, (rt, decl) =
        convert_specifiers env target does_remove_virtual
      in
      (match base with
       | RPKPointer ->
         env, aux, mk_cast_n (rt,decl JUSTBASE) e
       | RPKReference ->