diff --git a/convert.ml b/convert.ml
index 2bbb4b5e8c4e9323c806cad7cb2525bfdeb1ba9f..6497fb4bb997df1ea43ee31e63a0f810096eb30f 100644
--- a/convert.ml
+++ b/convert.ml
@@ -119,23 +119,6 @@ let rec protect_ptr_type 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 =
@@ -589,61 +572,43 @@ let preserved_returned_object aux e =
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
+ | 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 -> spec_of_ikind (Cil.intKindForSize 2 true) @ spec, decl
- | Int IChar32 -> spec_of_ikind (Cil.intKindForSize 4 true) @ spec, decl
+ | 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 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
+ 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 ->
- (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
+ 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
- spec_type (Tenum(name,None,[]))::spec, decl
+ env, (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
@@ -651,7 +616,7 @@ let rec convert_base_type env spec decl typ does_remove_virtual =
let s, t = Convert_env.typedef_normalize env s t in
Mangling.mangle s t None
in
- spec_type (Tstruct (name, None, [])) :: spec, decl
+ 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
@@ -659,7 +624,7 @@ let rec convert_base_type env spec decl typ does_remove_virtual =
let s, t = Convert_env.typedef_normalize env s t in
Mangling.mangle s t None
in
- spec_type (Tunion (name, None, [])) :: spec, decl
+ 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
@@ -669,23 +634,25 @@ let rec convert_base_type env spec decl typ does_remove_virtual =
convert_type
env (fun d -> decl (protect_ptr_type attrs d)) t does_remove_virtual
| Pointer (PFunctionPointer s) ->
- let rt, rt_decl, args, variadic =
+ let env, (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)))
+ env,
+ (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 =
+ let env, (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)))
+ env,
+ (rt,
+ (fun d ->
+ rt_decl (PROTO (decl (protect_ptr_type attrs d),args,[],variadic))))
| Pointer(PStandardMethodPointer _)
| LVReference (PStandardMethodPointer _)
| RVReference (PStandardMethodPointer _) ->
@@ -728,25 +695,26 @@ let rec convert_base_type env spec decl typ does_remove_virtual =
let name, t = Convert_env.typedef_normalize env name TStandard in
Mangling.mangle name t None
in
- spec_type (Tnamed cname)::spec, decl
+ env, (spec_type (Tnamed cname)::spec, decl)
| Lambda _ ->
let type_name = Mangling.mangle_cc_type typ in
- (SpecType (Tstruct (type_name, None, []))) :: spec, decl
+ 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 args, variadic =
- if s.variadic && s.parameter = [] then [], false
+ let env, (args, variadic) =
+ if s.variadic && s.parameter = [] then env, ([], false)
else
- convert_signature env s.parameter does_remove_virtual, s.variadic
+ let env, l = convert_signature env s.parameter does_remove_virtual in
+ env, (l, s.variadic)
in
- let rt, rt_decl =
+ let env, (rt, rt_decl) =
convert_specifiers env s.result does_remove_virtual
in
- rt, rt_decl, args, variadic
+ env, (rt, rt_decl, args, variadic)
and convert_signature env l does_remove_virtual =
match l with
@@ -757,30 +725,37 @@ and convert_signature env l does_remove_virtual =
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
+ 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 typ, decl = convert_specifiers env t does_remove_virtual in
- (typ, ("",decl JUSTBASE,[],Cil_datatype.Location.unknown))
+ 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 typ,decl = convert_specifiers env arg.arg_type does_remove_virtual in
+ 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 rt, decl = convert_specifiers env rt does_remove_virtual in
- let args =
+ 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 *)
- [[SpecType Tvoid],("",JUSTBASE,[],loc)]
- | _ -> List.map (convert_decl env does_remove_virtual) args
+ 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
@@ -791,8 +766,8 @@ and make_prototype loc env name kind rt args variadic does_remove_virtual =
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)
+ | 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 =
@@ -807,34 +782,35 @@ and convert_constant env c does_remove_virtual = match c with
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 bt,decl = convert_base_type env [] id t does_remove_virtual in
- TYPE_SIZEOF (bt,decl JUSTBASE)
+ let env, (bt,decl) = convert_base_type env [] id t does_remove_virtual in
+ env, 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)
+ 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 _ -> arg.expr_node
+ | UOCastNoEffect _ -> env, arg.expr_node
(* Marks initialization of a ref field. treated elsewhere. *)
- | UOCastDerefInit -> arg.expr_node
+ | UOCastDerefInit -> env, arg.expr_node
(* Use the actual rvalue of a reference. *)
- | UOCastDeref -> UNARY(MEMOF,arg)
- | UOCastToVoid -> mk_cast_n ([SpecType Tvoid], JUSTBASE) arg
+ | UOCastDeref -> env, UNARY(MEMOF,arg)
+ | UOCastToVoid -> env, 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)
+ 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,
@@ -924,17 +900,21 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
let env, aux, node =
match e with
| Constant c ->
- let e = convert_constant env c does_remove_virtual in env, aux, e
+ 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 bt,decl = convert_base_type env [] id t does_remove_virtual in
+ 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 bt,decl = convert_base_type env [] id t does_remove_virtual in
+ 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,
@@ -970,7 +950,7 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
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
+ 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
@@ -984,7 +964,9 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
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
+ 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
@@ -1229,7 +1211,9 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
expr_node = UNARY(ADDROF,e)}))}))
| ShiftPointerCast(target,base,kind,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
+ let env, (rt, decl) =
+ convert_specifiers env target does_remove_virtual
+ in
let derived_aux e derived_name td base_name tb =
let var_name = shift_ptr_var_name () in
let env =
@@ -1459,13 +1443,13 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
Convert_env.class_type_from_qualifications
env name.prequalification
in
- let proto_args =
+ let env, proto_args =
convert_signature
env
(Cxx_utils.(obj_ptr (unqual_type class_type))::signature.parameter)
does_remove_virtual
in
- let proto_rt, proto_rt_decl =
+ let env, (proto_rt, proto_rt_decl) =
convert_specifiers env signature.result does_remove_virtual
in
let proto_spec = List.map convert_cv signature.result.qualifier in
@@ -1530,7 +1514,9 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
env, aux, CALL(f,args,[])
| Temporary(name, ctyp, init_exp, force) ->
let env = Convert_env.add_local_var env name ctyp.plain_type in
- let typ, decl = convert_specifiers env ctyp does_remove_virtual in
+ let env, (typ, decl) =
+ convert_specifiers env ctyp does_remove_virtual
+ in
let attrs = add_fc_destructor_attr env ctyp [] in
let res = if drop_temp then NOTHING else VARIABLE name in
let is_const = Cxx_utils.is_const_type ctyp in
@@ -1600,7 +1586,7 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
env, add_local_aux_def aux tmp_decl, res)
| VAArg(e,t) ->
let env, aux', e = convert_expr env aux e does_remove_virtual in
- let typ, decl = convert_specifiers env t does_remove_virtual in
+ let env, (typ, decl) = convert_specifiers env t does_remove_virtual in
(* implement the ugly comment in cabs.ml *)
let builtin = mk_expr env (VARIABLE "__builtin_va_arg") in
let typ_expr = mk_expr env (TYPE_SIZEOF (typ, decl JUSTBASE)) in
@@ -1636,7 +1622,9 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
let subtype = Cxx_utils.const_qual_type elt_typ in
let array_type = Array { subtype; dimension } in
let qarray_type = Cxx_utils.unqual_type array_type in
- let carr_type, carr_decl = convert_specifiers env qarray_type false in
+ let env, (carr_type, carr_decl) =
+ convert_specifiers env qarray_type false
+ in
let array_name = Convert_env.temp_name env "init_array" in
let old_env = env in
let env = Convert_env.add_local_var env array_name array_type in
@@ -1693,7 +1681,7 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
(CONSTANT (CONST_INT (string_of_int il_size)))
],[])),loc))
in
- let cil_type, cil_decl =
+ let env, (cil_type, cil_decl) =
convert_specifiers env (Cxx_utils.unqual_type il_type) false
in
let il_dec =
@@ -1743,19 +1731,22 @@ and create_lambda env aux lam_name lam_type overloads closures =
(* Create the definition of the struct that represents the lambda *)
let define_struct env name =
let loc = Convert_env.get_loc env in
- let field_of_capture cap =
+ let field_of_capture env cap =
let s, t = capture_name_type env cap in
- let rt, decl = convert_specifiers env t false in
- FIELD (rt, [ (s, decl JUSTBASE, [], loc), None ])
+ let env, (rt, decl) = convert_specifiers env t false in
+ env, FIELD (rt, [ (s, decl JUSTBASE, [], loc), None ])
in
- let field_of_functions ovl =
+ let field_of_functions env ovl =
let fptr = mk_lambda_fptr_type lam_type ovl in
let name = lambda_unique_overload_name ovl.id in
- let rt, decl = convert_specifiers env fptr false in
- FIELD (rt, [(name, decl JUSTBASE, [], loc), None])
+ let env, (rt, decl) = convert_specifiers env fptr false in
+ env, FIELD (rt, [(name, decl JUSTBASE, [], loc), None])
in
- let cap_fields = List.map field_of_capture closures in
- let fptr_fields = List.map field_of_functions overloads in
+ let env,cap_fields = Convert_env.env_map field_of_capture env closures in
+ let env,fptr_fields =
+ Convert_env.env_map field_of_functions env overloads
+ in
+ env,
ONLYTYPEDEF (
[SpecType (Tstruct(name, Some (fptr_fields @ cap_fields),[]))],loc)
in
@@ -1796,7 +1787,7 @@ and create_lambda env aux lam_name lam_type overloads closures =
in
let struct_name = Mangling.mangle_cc_type lam_type in
- let struct_def = define_struct env struct_name in
+ let env, struct_def = define_struct env struct_name in
let env = Convert_env.add_c_global env struct_def in
let struct_inst = instantiate_struct env struct_name in
let aux = add_local_aux_def aux struct_inst in
@@ -2116,7 +2107,7 @@ and convert_initializer env typ var init_exp does_remove_virtual =
| _, None -> env, aux, (what,def)::acc
| Single_init e, Some _ ->
incr init_var_counter;
- let spec, decl = convert_specifiers env ty does_remove_virtual in
+ let env, (spec, decl) = convert_specifiers env ty does_remove_virtual in
let attrs = add_fc_destructor_attr env ty [] in
let cloc = Cil_datatype.Location.of_lexing_loc e.eloc in
let decl =
@@ -2149,7 +2140,9 @@ and convert_init_statement env init does_remove_virtual =
let env, aux, l, def, base =
List.fold_right
(fun {id_name; init_type=typ; init_val} (env,aux,l,def, base) ->
- let base', decl = convert_specifiers env typ does_remove_virtual in
+ let env, (base', decl) =
+ convert_specifiers env typ does_remove_virtual
+ in
let base =
match base with
| None -> Some base'
@@ -2163,21 +2156,21 @@ and convert_init_statement env init does_remove_virtual =
let env = Convert_env.add_local_var env id_name typ.plain_type in
match init_val with
| None ->
- let init = (id_name, decl JUSTBASE,[],loc),NO_INIT in
- (env, aux, init::l, def, base)
+ let init = (id_name, decl JUSTBASE,[],loc),NO_INIT in
+ (env, aux, init::l, def, base)
| Some init ->
let var = Local { prequalification = []; decl_name = id_name } in
let env,aux',init, def' =
convert_initializer env typ var init does_remove_virtual
in
- let def = match def' with
- | None -> def
- | Some stmt -> stmt::def
- in
- let init = (id_name, decl JUSTBASE,attrs,loc),init in
- env, merge_aux aux' aux, init::l, def, base)
- init_declarator_list
- (env, empty_aux, [], [], None)
+ let def = match def' with
+ | None -> def
+ | Some stmt -> stmt::def
+ in
+ let init = (id_name, decl JUSTBASE,attrs,loc),init in
+ env, merge_aux aux' aux, init::l, def, base)
+ init_declarator_list
+ (env, empty_aux, [], [], None)
in
let l = List.rev l in
if l = [] then
@@ -2201,7 +2194,7 @@ and convert_condition env cond does_remove_virtual =
| CondVarDecl(name, typ, init) ->
let attrs = add_fc_destructor_attr env typ [] in
let env = Convert_env.add_local_var env name typ.plain_type in
- let base, decl = convert_specifiers env typ does_remove_virtual in
+ let env, (base, decl) = convert_specifiers env typ does_remove_virtual in
let res = { expr_loc = loc; expr_node = VARIABLE name } in
let var = Local { prequalification = []; decl_name = name } in
let env, aux, init, e =
@@ -2340,7 +2333,7 @@ and convert_statement env st does_remove_virtual =
| VarDecl (loc, name, typ, init) ->
let env = Convert_env.set_loc env loc in
let cloc = Cil_datatype.Location.of_lexing_loc loc in
- let base, decl = convert_specifiers env typ does_remove_virtual in
+ let env, (base, decl) = convert_specifiers env typ does_remove_virtual in
let qual_name = { prequalification = []; decl_name = name } in
let attrs = add_fc_destructor_attr env typ [] in
let env =
@@ -2467,7 +2460,7 @@ and convert_catch_clause does_remove_virtual (acc,env) { typed_arg; cbody } =
| None -> None, env
| Some v ->
let qtype = Convert_env.qual_type_normalize env v.arg_type in
- let decl = convert_decl env does_remove_virtual v in
+ let env, decl = convert_decl env does_remove_virtual v in
Some decl,
Convert_env.add_local_var env v.arg_name qtype.plain_type
in
@@ -2482,7 +2475,7 @@ and convert_case_statement does_remove_virtual (acc, env) case =
| Case(value,action) ->
let loc = find_loc_list_stmt action in
let cloc = Cil_datatype.Location.of_lexing_loc loc in
- let value = convert_constant env value does_remove_virtual in
+ let env, value = convert_constant env value does_remove_virtual in
let value = mk_expr_l cloc value in
let action, env =
convert_stmt_block env action does_remove_virtual
@@ -2552,7 +2545,7 @@ let convert_static_const env loc name ikind kind value does_remove_virtual =
Mangling.mangle qualified_name t None
in
let plain = Int ikind in
- let spec, _ =
+ let env, (spec, _) =
convert_base_type env [SpecCV CV_CONST] id plain does_remove_virtual
in
let spec =
@@ -2844,7 +2837,7 @@ let create_stmt_set_vmt env qualification_class inherits =
Cxx_utils.
(obj_ptr (class_ptr (Cxx_utils.empty_qual "_frama_c_vmt", TStandard)))
in
- let rt, decl = convert_specifiers env vmt_type true in
+ let env, (rt, decl) = convert_specifiers env vmt_type true in
let cvmt_type = rt, decl JUSTBASE in
let create_stmt_set_shift_vmt (l, previous_index)
{ base = base_class_name;
@@ -3080,9 +3073,13 @@ and create_generic_op op env most_derived class_name =
| _ :: _ :: _ ->
Frama_Clang_option.fatal "unexpected signature for implicit operator"
in
- let bt1,dt1 = convert_specifiers env bare_this_ptr (not most_derived) in
+ let env, (bt1,dt1) =
+ convert_specifiers env bare_this_ptr (not most_derived)
+ in
let t1 = bt1, dt1 JUSTBASE in
- let bt2,dt2 = convert_specifiers env bare_prm (not most_derived) in
+ let env, (bt2,dt2) =
+ convert_specifiers env bare_prm (not most_derived)
+ in
let t2 = bt2, dt2 JUSTBASE in
let mk_cast t e = mk_expr env (CAST (t, SINGLE_INIT e)) in
let mk_mem e = mk_expr env (UNARY(MEMOF,e)) in
@@ -3666,7 +3663,7 @@ and convert_class_component (env, implicits, types, fields, others) meth =
| CFieldDecl(loc, name, typ, bf_info, is_mutable) ->
let env = Convert_env.set_loc env loc in
let cloc = Cil_datatype.Location.of_lexing_loc loc in
- let base,decl = convert_specifiers env typ false in
+ let env, (base,decl) = convert_specifiers env typ false in
(* We remove static qualifier to avoid confusion with the C's static. *)
let base =
List.filter (function SpecStorage(STATIC)-> false | _ -> true) base
@@ -3707,7 +3704,7 @@ and convert_class_component (env, implicits, types, fields, others) meth =
let env = Convert_env.add_typedef env qual_name typ in
let name,_= Convert_env.typedef_normalize env qual_name TStandard in
let name = Mangling.mangle name TStandard None in
- let base,decl = convert_specifiers env typ false in
+ let env, (base,decl) = convert_specifiers env typ false in
(env,implicits,
TYPEDEF((SpecTypedef::base,[(name,decl JUSTBASE,[],cloc)]),cloc)
::types,
@@ -3776,7 +3773,7 @@ let rec convert_pod_field (cfields, typs, env) field =
| CFieldDecl(loc, name, typ, bf_info,is_mutable) ->
let env = Convert_env.set_loc env loc in
let cloc = Cil_datatype.Location.of_lexing_loc loc in
- let base,decl = convert_specifiers env typ false in
+ let env, (base,decl) = convert_specifiers env typ false in
let base =
if is_mutable then
SpecAttr (add_attr env Cil.frama_c_mutable []) :: base
@@ -4031,7 +4028,7 @@ let rec convert_global env glob =
qualified_name TStandard in
Mangling.mangle n' t' None
in
- let rt, decl = convert_specifiers env typ false in
+ let env, (rt, decl) = convert_specifiers env typ false in
let attrs = add_fc_destructor_attr env typ [] in
let env = Convert_env.add_global_var env qualified_name typ.plain_type in
let old_ghost = Convert_env.is_ghost env in
@@ -4102,7 +4099,7 @@ let rec convert_global env glob =
qual_name TStandard in
Mangling.mangle qual_name t None
in
- let base,decl = convert_specifiers env typ false in
+ let env, (base,decl) = convert_specifiers env typ false in
let env = Convert_env.set_ghost env old_ghost in
Convert_env.add_c_global
env (TYPEDEF((SpecTypedef::base,[(name,decl JUSTBASE,[],cloc)]), cloc))
@@ -4150,7 +4147,7 @@ let convert_ast file =
pos_lnum = 0; pos_bol = 0; pos_cnum = 0; }
in
let basic_loc = basic_pos, basic_pos in
- let sizeof_t = spec_of_ikind Cil.theMachine.kindOfSizeOf in
+ let sizeof_t = Cxx_utils.spec_of_ikind Cil.theMachine.kindOfSizeOf in
let res =
(Datatype.Filepath.of_string file.filename,
(false,
diff --git a/convert_env.ml b/convert_env.ml
index e3466772f26ca65eaff72d1ef1f7028c8b58b521..f076bd323ae0b043a4932131c465ea0fbc28a6a3 100644
--- a/convert_env.ml
+++ b/convert_env.ml
@@ -258,6 +258,24 @@ let get_typedef env name =
let has_typedef env name =
Fclang_datatype.Qualified_name.Map.mem (name, TStandard) env.typedefs
+let memo_wchar env =
+ let wchar_name = { prequalification=[];decl_name="wchar_t"} in
+ if has_typedef env wchar_name then env
+ else begin
+ let kind = Cil.theMachine.wcharKind in
+ let repr = Cxx_utils.(unqual_type (int_type kind)) in
+ let env = add_typedef env wchar_name repr in
+ let ghost = is_ghost env in
+ let env = set_ghost env false in
+ let loc = get_loc env in
+ let spec = Cxx_utils.spec_of_ikind kind in
+ let name = ["wchar_t", Cabs.JUSTBASE, [], loc] in
+ let def = Cabs.TYPEDEF((spec,name),loc) in
+ let env = add_c_global env def in
+ let env = set_ghost env ghost in
+ env
+ end
+
let rec template_parameter_normalize env tparam = match tparam with
| TPStructOrClass name -> TPStructOrClass
{ name with prequalification
@@ -790,3 +808,8 @@ let reset_closure env =
match env.captured_vars with
| [] -> env
| _::captured_vars -> { env with captured_vars }
+
+let env_map f env l =
+ let do_one (env, acc) x = let env, y = f env x in env,y::acc in
+ let env, res = List.fold_left do_one (env,[]) l in
+ env, List.rev res
diff --git a/convert_env.mli b/convert_env.mli
index b5d3c8bb4da058253821bb9570ced546ace6715b..9a45ebf1d7461b5517bfba95a17f17b223f5b717 100644
--- a/convert_env.mli
+++ b/convert_env.mli
@@ -128,6 +128,11 @@ val get_typedef: env -> qualified_name -> qual_type
val has_typedef: env -> qualified_name -> bool
+val memo_wchar: env -> env
+(** adds a definition of wchar_t if not already present. Used when encountering
+ [wchar_t] on the C++ side.
+*)
+
val add_struct: env -> (qualified_name * tkind) -> (string * qual_type) list
-> env
@@ -315,3 +320,8 @@ val reset_closure: env -> env
val add_closure_info: env -> capture list -> env
(** Associates the given identifiers to the appropriate closure kind. *)
+
+(** iterates a function that might change the environment over a list,
+ and returns the final environment together with the list of results
+*)
+val env_map: (env -> 'a -> (env * 'b)) -> env -> 'a list -> (env * 'b list)
diff --git a/cxx_utils.ml b/cxx_utils.ml
index a4c74979e904f1c2f515492504456dd521a640ca..c4ed3ab1edf599adcf9396042304d084d91ff289 100644
--- a/cxx_utils.ml
+++ b/cxx_utils.ml
@@ -393,6 +393,23 @@ let meth_name class_name tkind decl_name =
let prequalification= List.append class_name.prequalification [last_elt] in
{ prequalification; decl_name }
+let int_kind = function
+ | Cil_types.IBool -> IBool
+ | IChar ->
+ if Cil.theMachine.theMachine.char_is_unsigned then IChar_u else IChar_s
+ | IUChar -> IUChar
+ | ISChar -> ISChar
+ | IInt -> IInt
+ | IUInt -> IUInt
+ | IShort -> IShort
+ | IUShort -> IUShort
+ | ILong -> ILong
+ | IULong -> IULong
+ | ILongLong -> ILongLong
+ | IULongLong -> IULongLong
+
+let int_type ikind = Intermediate_format.Int (int_kind ikind)
+
let unqual_type t = { qualifier = []; plain_type = t }
let const_type t = { qualifier = [ Const ]; plain_type = t }
@@ -431,3 +448,20 @@ let class_ptr (n,t) = unqual_type (plain_class_ptr (n,t))
let class_lvref (n,t) = unqual_type (plain_class_lvref (n,t))
let class_rvref (n,t) = unqual_type (plain_class_rvref (n,t))
+
+let spec_of_ikind s =
+ let open Cabs in
+ let open Cil_types in
+ 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 ]
diff --git a/cxx_utils.mli b/cxx_utils.mli
index f5d77c22e7a0647cf68ddb7fcb48e5c585b07a86..a5990517ad3a16e9d96585370cf04e5ac9c55442 100644
--- a/cxx_utils.mli
+++ b/cxx_utils.mli
@@ -59,6 +59,9 @@ val meth_name: qualified_name -> tkind -> string -> qualified_name
(** {3 Types}. *)
+(** returns an IR typ corresponding to the Cil's kind *)
+val int_type: Cil_types.ikind -> typ
+
(** returns the unqualified version of the given typ. *)
val unqual_type: typ -> qual_type
@@ -99,3 +102,5 @@ val class_ptr: Fclang_datatype.Qualified_name.t -> qual_type
val class_lvref: Fclang_datatype.Qualified_name.t -> qual_type
val class_rvref: Fclang_datatype.Qualified_name.t -> qual_type
+
+val spec_of_ikind: Cil_types.ikind -> Cabs.specifier
diff --git a/tests/basic/oracle/placement_new.res.oracle b/tests/basic/oracle/placement_new.res.oracle
index 7404de4d8ea2e13942a395ef7afe0e23289f221b..bd686d917ffc2377d51e19504eead59e959b28e1 100644
--- a/tests/basic/oracle/placement_new.res.oracle
+++ b/tests/basic/oracle/placement_new.res.oracle
@@ -39,6 +39,7 @@ struct __fc_lldiv_t {
long long rem ;
};
typedef struct __fc_lldiv_t lldiv_t;
+typedef long wchar_t;
typedef size_t size_t;
struct T;
struct T {
@@ -1075,7 +1076,7 @@ int mblen(char const *s, size_t n);
\from (indirect: s), *(s + (0 .. n - 1)), (indirect: n),
__fc_mbtowc_state;
*/
-int mbtowc(long * restrict pwc, char const * restrict s, size_t n);
+int mbtowc(wchar_t * restrict pwc, char const * restrict s, size_t n);
/*@ ghost int __fc_wctomb_state; */
/*@ assigns \result, *(s + (0 ..)), __fc_wctomb_state;
@@ -1083,7 +1084,7 @@ int mbtowc(long * restrict pwc, char const * restrict s, size_t n);
assigns *(s + (0 ..)) \from wc, __fc_wctomb_state;
assigns __fc_wctomb_state \from wc, __fc_wctomb_state;
*/
-int wctomb(char *s, long wc);
+int wctomb(char *s, wchar_t wc);
/*@ requires separation: \separated(pwcs, s);
assigns \result, *(pwcs + (0 .. n - 1));
@@ -1092,7 +1093,7 @@ int wctomb(char *s, long wc);
assigns *(pwcs + (0 .. n - 1))
\from (indirect: s), *(s + (0 .. n - 1)), (indirect: n);
*/
-size_t mbstowcs(long * restrict pwcs, char const * restrict s, size_t n);
+size_t mbstowcs(wchar_t * restrict pwcs, char const * restrict s, size_t n);
/*@ requires separation: \separated(s, pwcs);
assigns \result, *(s + (0 .. n - 1));
@@ -1102,7 +1103,7 @@ size_t mbstowcs(long * restrict pwcs, char const * restrict s, size_t n);
assigns *(s + (0 .. n - 1))
\from (indirect: pwcs), *(pwcs + (0 .. n - 1)), (indirect: n);
*/
-size_t wcstombs(char * restrict s, long const * restrict pwcs, size_t n);
+size_t wcstombs(char * restrict s, wchar_t const * restrict pwcs, size_t n);
/*@ requires valid_memptr: \valid(memptr);
requires
diff --git a/tests/basic/oracle/placement_newb.res.oracle b/tests/basic/oracle/placement_newb.res.oracle
index a12fa44c50c296a6e43f0884f0f45048e14df710..8b2058baa39ac3767c9065984c5cb8e5c3005e90 100644
--- a/tests/basic/oracle/placement_newb.res.oracle
+++ b/tests/basic/oracle/placement_newb.res.oracle
@@ -17,6 +17,7 @@ struct __fc_lldiv_t {
long long rem ;
};
typedef struct __fc_lldiv_t lldiv_t;
+typedef long wchar_t;
void *malloc(size_t size);
void free(void *p);
@@ -1044,7 +1045,7 @@ int mblen(char const *s, size_t n);
\from (indirect: s), *(s + (0 .. n - 1)), (indirect: n),
__fc_mbtowc_state;
*/
-int mbtowc(long * restrict pwc, char const * restrict s, size_t n);
+int mbtowc(wchar_t * restrict pwc, char const * restrict s, size_t n);
/*@ ghost int __fc_wctomb_state; */
/*@ assigns \result, *(s + (0 ..)), __fc_wctomb_state;
@@ -1052,7 +1053,7 @@ int mbtowc(long * restrict pwc, char const * restrict s, size_t n);
assigns *(s + (0 ..)) \from wc, __fc_wctomb_state;
assigns __fc_wctomb_state \from wc, __fc_wctomb_state;
*/
-int wctomb(char *s, long wc);
+int wctomb(char *s, wchar_t wc);
/*@ requires separation: \separated(pwcs, s);
assigns \result, *(pwcs + (0 .. n - 1));
@@ -1061,7 +1062,7 @@ int wctomb(char *s, long wc);
assigns *(pwcs + (0 .. n - 1))
\from (indirect: s), *(s + (0 .. n - 1)), (indirect: n);
*/
-size_t mbstowcs(long * restrict pwcs, char const * restrict s, size_t n);
+size_t mbstowcs(wchar_t * restrict pwcs, char const * restrict s, size_t n);
/*@ requires separation: \separated(s, pwcs);
assigns \result, *(s + (0 .. n - 1));
@@ -1071,7 +1072,7 @@ size_t mbstowcs(long * restrict pwcs, char const * restrict s, size_t n);
assigns *(s + (0 .. n - 1))
\from (indirect: pwcs), *(pwcs + (0 .. n - 1)), (indirect: n);
*/
-size_t wcstombs(char * restrict s, long const * restrict pwcs, size_t n);
+size_t wcstombs(char * restrict s, wchar_t const * restrict pwcs, size_t n);
/*@ requires valid_memptr: \valid(memptr);
requires
diff --git a/tests/specs/oracle/wchar_t.res.oracle b/tests/specs/oracle/wchar_t.res.oracle
index 351afe930821eef0911613a67ddd4a86301b653e..130fd3148ea1772077349e0f70e5eb40da8610f4 100644
--- a/tests/specs/oracle/wchar_t.res.oracle
+++ b/tests/specs/oracle/wchar_t.res.oracle
@@ -1,13 +1,14 @@
[kernel] Parsing wchar_t.cpp (external front-end)
Now output intermediate result
/* Generated by Frama-C */
+typedef long wchar_t;
/*@ predicate is_normal_char(long c) = 0 ≤ c ≤ 255;
*/
/*@ predicate wchar_buff{L}(long *p, ℤ l) = \at(*(p + l) ≡ (long)0,L);
*/
int freq[256];
/*@ requires is_normal_char(c); */
-void count(long c)
+void count(wchar_t c)
{
(freq[c]) ++;
return;
diff --git a/tests/stl/oracle/limits.res.oracle b/tests/stl/oracle/limits.res.oracle
index d32240c5d192920a22376af29057eaa289f4be22..1d54ee54127ab740700d723a3ae986d5b7834a5e 100644
--- a/tests/stl/oracle/limits.res.oracle
+++ b/tests/stl/oracle/limits.res.oracle
@@ -31,6 +31,7 @@ struct _frama_c_rtti_name_info_node {
int number_of_base_classes ;
struct _frama_c_vmt *pvmt ;
};
+typedef long wchar_t;
float __builtin_huge_valf(void);
float __builtin_nanf(char const *__frama_c_arg_0);
@@ -569,23 +570,23 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
_Bool const is_specialized = (_Bool)1;
_Bool const is_signed = (_Bool)1;
-long min(void)
+wchar_t min(void)
{
- long __retres;
+ wchar_t __retres;
__retres = -2147483647L - 1L;
return __retres;
}
-long max(void)
+wchar_t max(void)
{
- long __retres;
+ wchar_t __retres;
__retres = 2147483647L;
return __retres;
}
-long lowest(void)
+wchar_t lowest(void)
{
- long tmp;
+ wchar_t tmp;
tmp = min();
return tmp;
}
@@ -596,17 +597,17 @@ int const max_digits10 = 0;
_Bool const is_integer = (_Bool)1;
_Bool const is_exact = (_Bool)1;
int const radix = 2;
-long epsilon(void)
+wchar_t epsilon(void)
{
- long __retres;
- __retres = (long)0;
+ wchar_t __retres;
+ __retres = (wchar_t)0;
return __retres;
}
-long round_error(void)
+wchar_t round_error(void)
{
- long __retres;
- __retres = (long)0;
+ wchar_t __retres;
+ __retres = (wchar_t)0;
return __retres;
}
@@ -618,31 +619,31 @@ _Bool const has_infinity = (_Bool)0;
_Bool const has_quiet_NaN = (_Bool)0;
_Bool const has_signaling_NaN = (_Bool)0;
_Bool const has_denorm_loss = (_Bool)0;
-long infinity(void)
+wchar_t infinity(void)
{
- long __retres;
- __retres = (long)0;
+ wchar_t __retres;
+ __retres = (wchar_t)0;
return __retres;
}
-long quiet_NaN(void)
+wchar_t quiet_NaN(void)
{
- long __retres;
- __retres = (long)0;
+ wchar_t __retres;
+ __retres = (wchar_t)0;
return __retres;
}
-long signaling_NaN(void)
+wchar_t signaling_NaN(void)
{
- long __retres;
- __retres = (long)0;
+ wchar_t __retres;
+ __retres = (wchar_t)0;
return __retres;
}
-long denorm_min(void)
+wchar_t denorm_min(void)
{
- long __retres;
- __retres = (long)0;
+ wchar_t __retres;
+ __retres = (wchar_t)0;
return __retres;
}
diff --git a/tests/stl/oracle/stl_atomic.res.oracle b/tests/stl/oracle/stl_atomic.res.oracle
index fc10dce3d1da3ab9cd30fcd808aed257793d0106..2da7908d106cc4a1d27f9a13e2a4214e0be57821 100644
--- a/tests/stl/oracle/stl_atomic.res.oracle
+++ b/tests/stl/oracle/stl_atomic.res.oracle
@@ -113,8 +113,9 @@ struct __atomic<char16_t> {
struct __atomic<char32_t> {
unsigned int __val ;
};
+typedef long wchar_t;
struct __atomic<wchar_t> {
- long __val ;
+ wchar_t __val ;
};
struct atomic<bool> {
struct __atomic<bool> _frama_c__ZN3stdE8__atomicIbE ;
@@ -3502,187 +3503,204 @@ _Bool is_lock_free(struct __atomic<wchar_t> const volatile *this);
_Bool is_lock_free(struct __atomic<wchar_t> const *this);
/*@ requires \valid(this); */
-void store(struct __atomic<wchar_t> volatile *this, long c, memory_order o);
+void store(struct __atomic<wchar_t> volatile *this, wchar_t c, memory_order o);
/*@ requires \valid(this); */
-void store(struct __atomic<wchar_t> *this, long c, memory_order o);
+void store(struct __atomic<wchar_t> *this, wchar_t c, memory_order o);
/*@ requires \valid_read(this); */
-long load(struct __atomic<wchar_t> const volatile *this,
- memory_order __frama_c_arg_0);
+wchar_t load(struct __atomic<wchar_t> const volatile *this,
+ memory_order __frama_c_arg_0);
/*@ requires \valid_read(this); */
-long load(struct __atomic<wchar_t> const *this, memory_order __frama_c_arg_0);
+wchar_t load(struct __atomic<wchar_t> const *this,
+ memory_order __frama_c_arg_0);
/*@ requires \valid_read(this); */
-long conversion(wchar_t)(struct __atomic<wchar_t> const volatile *this);
+wchar_t conversion(wchar_t)(struct __atomic<wchar_t> const volatile *this);
/*@ requires \valid_read(this); */
-long conversion(wchar_t)(struct __atomic<wchar_t> const *this);
+wchar_t conversion(wchar_t)(struct __atomic<wchar_t> const *this);
/*@ requires \valid(this); */
-long exchange(struct __atomic<wchar_t> volatile *this, long __frama_c_arg_0,
- memory_order __frama_c_arg_1);
+wchar_t exchange(struct __atomic<wchar_t> volatile *this,
+ wchar_t __frama_c_arg_0, memory_order __frama_c_arg_1);
/*@ requires \valid(this); */
-long exchange(struct __atomic<wchar_t> *this, long __frama_c_arg_0,
- memory_order __frama_c_arg_1);
+wchar_t exchange(struct __atomic<wchar_t> *this, wchar_t __frama_c_arg_0,
+ memory_order __frama_c_arg_1);
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0); */
_Bool compare_exchange_weak(struct __atomic<wchar_t> volatile *this,
- long *__frama_c_arg_0, long __frama_c_arg_1,
+ wchar_t *__frama_c_arg_0,
+ wchar_t __frama_c_arg_1,
memory_order __frama_c_arg_2,
memory_order __frama_c_arg_3);
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0); */
_Bool compare_exchange_weak(struct __atomic<wchar_t> *this,
- long *__frama_c_arg_0, long __frama_c_arg_1,
+ wchar_t *__frama_c_arg_0,
+ wchar_t __frama_c_arg_1,
memory_order __frama_c_arg_2,
memory_order __frama_c_arg_3);
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0); */
_Bool compare_exchange_strong(struct __atomic<wchar_t> volatile *this,
- long *__frama_c_arg_0, long __frama_c_arg_1,
+ wchar_t *__frama_c_arg_0,
+ wchar_t __frama_c_arg_1,
memory_order __frama_c_arg_2,
memory_order __frama_c_arg_3);
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0); */
_Bool compare_exchange_strong(struct __atomic<wchar_t> *this,
- long *__frama_c_arg_0, long __frama_c_arg_1,
+ wchar_t *__frama_c_arg_0,
+ wchar_t __frama_c_arg_1,
memory_order __frama_c_arg_2,
memory_order __frama_c_arg_3);
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0); */
_Bool compare_exchange_weak(struct __atomic<wchar_t> volatile *this,
- long *__frama_c_arg_0, long __frama_c_arg_1,
+ wchar_t *__frama_c_arg_0,
+ wchar_t __frama_c_arg_1,
memory_order __frama_c_arg_2);
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0); */
_Bool compare_exchange_weak(struct __atomic<wchar_t> *this,
- long *__frama_c_arg_0, long __frama_c_arg_1,
+ wchar_t *__frama_c_arg_0,
+ wchar_t __frama_c_arg_1,
memory_order __frama_c_arg_2);
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0); */
_Bool compare_exchange_strong(struct __atomic<wchar_t> volatile *this,
- long *__frama_c_arg_0, long __frama_c_arg_1,
+ wchar_t *__frama_c_arg_0,
+ wchar_t __frama_c_arg_1,
memory_order __frama_c_arg_2);
/*@ requires \valid(this);
requires \valid(__frama_c_arg_0); */
_Bool compare_exchange_strong(struct __atomic<wchar_t> *this,
- long *__frama_c_arg_0, long __frama_c_arg_1,
+ wchar_t *__frama_c_arg_0,
+ wchar_t __frama_c_arg_1,
memory_order __frama_c_arg_2);
/*@ requires \valid(this); */
-long fetch_add(struct __atomic<wchar_t> volatile *this, long __frama_c_arg_0,
- memory_order __frama_c_arg_1);
+wchar_t fetch_add(struct __atomic<wchar_t> volatile *this,
+ wchar_t __frama_c_arg_0, memory_order __frama_c_arg_1);
/*@ requires \valid(this); */
-long fetch_add(struct __atomic<wchar_t> *this, long __frama_c_arg_0,
- memory_order __frama_c_arg_1);
+wchar_t fetch_add(struct __atomic<wchar_t> *this, wchar_t __frama_c_arg_0,
+ memory_order __frama_c_arg_1);
/*@ requires \valid(this); */
-long fetch_sub(struct __atomic<wchar_t> volatile *this, long __frama_c_arg_0,
- memory_order __frama_c_arg_1);
+wchar_t fetch_sub(struct __atomic<wchar_t> volatile *this,
+ wchar_t __frama_c_arg_0, memory_order __frama_c_arg_1);
/*@ requires \valid(this); */
-long fetch_sub(struct __atomic<wchar_t> *this, long __frama_c_arg_0,
- memory_order __frama_c_arg_1);
+wchar_t fetch_sub(struct __atomic<wchar_t> *this, wchar_t __frama_c_arg_0,
+ memory_order __frama_c_arg_1);
/*@ requires \valid(this); */
-long fetch_and(struct __atomic<wchar_t> volatile *this, long __frama_c_arg_0,
- memory_order __frama_c_arg_1);
+wchar_t fetch_and(struct __atomic<wchar_t> volatile *this,
+ wchar_t __frama_c_arg_0, memory_order __frama_c_arg_1);
/*@ requires \valid(this); */
-long fetch_and(struct __atomic<wchar_t> *this, long __frama_c_arg_0,
- memory_order __frama_c_arg_1);
+wchar_t fetch_and(struct __atomic<wchar_t> *this, wchar_t __frama_c_arg_0,
+ memory_order __frama_c_arg_1);
/*@ requires \valid(this); */
-long fetch_or(struct __atomic<wchar_t> volatile *this, long __frama_c_arg_0,
- memory_order __frama_c_arg_1);
+wchar_t fetch_or(struct __atomic<wchar_t> volatile *this,
+ wchar_t __frama_c_arg_0, memory_order __frama_c_arg_1);
/*@ requires \valid(this); */
-long fetch_or(struct __atomic<wchar_t> *this, long __frama_c_arg_0,
- memory_order __frama_c_arg_1);
+wchar_t fetch_or(struct __atomic<wchar_t> *this, wchar_t __frama_c_arg_0,
+ memory_order __frama_c_arg_1);
/*@ requires \valid(this); */
-long fetch_xor(struct __atomic<wchar_t> volatile *this, long __frama_c_arg_0,
- memory_order __frama_c_arg_1);
+wchar_t fetch_xor(struct __atomic<wchar_t> volatile *this,
+ wchar_t __frama_c_arg_0, memory_order __frama_c_arg_1);
/*@ requires \valid(this); */
-long fetch_xor(struct __atomic<wchar_t> *this, long __frama_c_arg_0,
- memory_order __frama_c_arg_1);
+wchar_t fetch_xor(struct __atomic<wchar_t> *this, wchar_t __frama_c_arg_0,
+ memory_order __frama_c_arg_1);
/*@ requires \valid_read(this); */
void __atomic<wchar_t>::Ctor(struct __atomic<wchar_t> const *this,
- long __frama_c_arg_0);
+ wchar_t __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator=(struct __atomic<wchar_t> volatile *this, long __frama_c_arg_0);
+wchar_t operator=(struct __atomic<wchar_t> volatile *this,
+ wchar_t __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator=(struct __atomic<wchar_t> *this, long __frama_c_arg_0);
+wchar_t operator=(struct __atomic<wchar_t> *this, wchar_t __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator++(struct __atomic<wchar_t> volatile *this, int __frama_c_arg_0);
+wchar_t operator++(struct __atomic<wchar_t> volatile *this,
+ int __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator++(struct __atomic<wchar_t> *this, int __frama_c_arg_0);
+wchar_t operator++(struct __atomic<wchar_t> *this, int __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator--(struct __atomic<wchar_t> volatile *this, int __frama_c_arg_0);
+wchar_t operator--(struct __atomic<wchar_t> volatile *this,
+ int __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator--(struct __atomic<wchar_t> *this, int __frama_c_arg_0);
+wchar_t operator--(struct __atomic<wchar_t> *this, int __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator++(struct __atomic<wchar_t> volatile *this);
+wchar_t operator++(struct __atomic<wchar_t> volatile *this);
/*@ requires \valid(this); */
-long operator++(struct __atomic<wchar_t> *this);
+wchar_t operator++(struct __atomic<wchar_t> *this);
/*@ requires \valid(this); */
-long operator--(struct __atomic<wchar_t> volatile *this);
+wchar_t operator--(struct __atomic<wchar_t> volatile *this);
/*@ requires \valid(this); */
-long operator--(struct __atomic<wchar_t> *this);
+wchar_t operator--(struct __atomic<wchar_t> *this);
/*@ requires \valid(this); */
-long operator+=(struct __atomic<wchar_t> volatile *this, long __frama_c_arg_0);
+wchar_t operator+=(struct __atomic<wchar_t> volatile *this,
+ wchar_t __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator+=(struct __atomic<wchar_t> *this, long __frama_c_arg_0);
+wchar_t operator+=(struct __atomic<wchar_t> *this, wchar_t __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator-=(struct __atomic<wchar_t> volatile *this, long __frama_c_arg_0);
+wchar_t operator-=(struct __atomic<wchar_t> volatile *this,
+ wchar_t __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator-=(struct __atomic<wchar_t> *this, long __frama_c_arg_0);
+wchar_t operator-=(struct __atomic<wchar_t> *this, wchar_t __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator&=(struct __atomic<wchar_t> volatile *this, long __frama_c_arg_0);
+wchar_t operator&=(struct __atomic<wchar_t> volatile *this,
+ wchar_t __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator&=(struct __atomic<wchar_t> *this, long __frama_c_arg_0);
+wchar_t operator&=(struct __atomic<wchar_t> *this, wchar_t __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator|=(struct __atomic<wchar_t> volatile *this, long __frama_c_arg_0);
+wchar_t operator|=(struct __atomic<wchar_t> volatile *this,
+ wchar_t __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator|=(struct __atomic<wchar_t> *this, long __frama_c_arg_0);
+wchar_t operator|=(struct __atomic<wchar_t> *this, wchar_t __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator^=(struct __atomic<wchar_t> volatile *this, long __frama_c_arg_0);
+wchar_t operator^=(struct __atomic<wchar_t> volatile *this,
+ wchar_t __frama_c_arg_0);
/*@ requires \valid(this); */
-long operator^=(struct __atomic<wchar_t> *this, long __frama_c_arg_0);
+wchar_t operator^=(struct __atomic<wchar_t> *this, wchar_t __frama_c_arg_0);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "__atomic",
@@ -3836,7 +3854,7 @@ void atomic<char32_t>::Ctor(struct atomic<char32_t> const *this,
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
/*@ requires \valid_read(this); */
-void atomic<wchar_t>::Ctor(struct atomic<wchar_t> const *this, long x)
+void atomic<wchar_t>::Ctor(struct atomic<wchar_t> const *this, wchar_t x)
{
__atomic<wchar_t>::Ctor(& this->_frama_c__ZN3stdE8__atomicIwE,x);
return;
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index 3aed66ca369e67ddf9554386637eb9d445456280..e03d5d8e5d00e07cf2aec3598e315a4beea078aa 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -115,6 +115,7 @@ struct __fc_lldiv_t {
long long rem ;
};
typedef struct __fc_lldiv_t lldiv_t;
+typedef long wchar_t;
struct Aircraft {
int m_id ;
int m_flyCount ;
@@ -3171,7 +3172,7 @@ int mblen(char const *s, size_t n);
\from (indirect: s), *(s + (0 .. n - 1)), (indirect: n),
__fc_mbtowc_state;
*/
-int mbtowc(long * restrict pwc, char const * restrict s, size_t n);
+int mbtowc(wchar_t * restrict pwc, char const * restrict s, size_t n);
/*@ ghost int __fc_wctomb_state; */
/*@ assigns \result, *(s + (0 ..)), __fc_wctomb_state;
@@ -3179,7 +3180,7 @@ int mbtowc(long * restrict pwc, char const * restrict s, size_t n);
assigns *(s + (0 ..)) \from wc, __fc_wctomb_state;
assigns __fc_wctomb_state \from wc, __fc_wctomb_state;
*/
-int wctomb(char *s, long wc);
+int wctomb(char *s, wchar_t wc);
/*@ requires separation: \separated(pwcs, s);
assigns \result, *(pwcs + (0 .. n - 1));
@@ -3188,7 +3189,7 @@ int wctomb(char *s, long wc);
assigns *(pwcs + (0 .. n - 1))
\from (indirect: s), *(s + (0 .. n - 1)), (indirect: n);
*/
-size_t mbstowcs(long * restrict pwcs, char const * restrict s, size_t n);
+size_t mbstowcs(wchar_t * restrict pwcs, char const * restrict s, size_t n);
/*@ requires separation: \separated(s, pwcs);
assigns \result, *(s + (0 .. n - 1));
@@ -3198,7 +3199,7 @@ size_t mbstowcs(long * restrict pwcs, char const * restrict s, size_t n);
assigns *(s + (0 .. n - 1))
\from (indirect: pwcs), *(pwcs + (0 .. n - 1)), (indirect: n);
*/
-size_t wcstombs(char * restrict s, long const * restrict pwcs, size_t n);
+size_t wcstombs(char * restrict s, wchar_t const * restrict pwcs, size_t n);
/*@ requires valid_memptr: \valid(memptr);
requires
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index 93272875fe11dee726682a4633df56775edb13b3..a46d588217d4921a93749653bd2029a34e6f0f19 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -112,6 +112,7 @@ struct __fc_lldiv_t {
long long rem ;
};
typedef struct __fc_lldiv_t lldiv_t;
+typedef long wchar_t;
struct Aircraft {
int m_id ;
int m_flyCount ;
@@ -2950,7 +2951,7 @@ int mblen(char const *s, size_t n);
\from (indirect: s), *(s + (0 .. n - 1)), (indirect: n),
__fc_mbtowc_state;
*/
-int mbtowc(long * restrict pwc, char const * restrict s, size_t n);
+int mbtowc(wchar_t * restrict pwc, char const * restrict s, size_t n);
/*@ ghost int __fc_wctomb_state; */
/*@ assigns \result, *(s + (0 ..)), __fc_wctomb_state;
@@ -2958,7 +2959,7 @@ int mbtowc(long * restrict pwc, char const * restrict s, size_t n);
assigns *(s + (0 ..)) \from wc, __fc_wctomb_state;
assigns __fc_wctomb_state \from wc, __fc_wctomb_state;
*/
-int wctomb(char *s, long wc);
+int wctomb(char *s, wchar_t wc);
/*@ requires separation: \separated(pwcs, s);
assigns \result, *(pwcs + (0 .. n - 1));
@@ -2967,7 +2968,7 @@ int wctomb(char *s, long wc);
assigns *(pwcs + (0 .. n - 1))
\from (indirect: s), *(s + (0 .. n - 1)), (indirect: n);
*/
-size_t mbstowcs(long * restrict pwcs, char const * restrict s, size_t n);
+size_t mbstowcs(wchar_t * restrict pwcs, char const * restrict s, size_t n);
/*@ requires separation: \separated(s, pwcs);
assigns \result, *(s + (0 .. n - 1));
@@ -2977,7 +2978,7 @@ size_t mbstowcs(long * restrict pwcs, char const * restrict s, size_t n);
assigns *(s + (0 .. n - 1))
\from (indirect: pwcs), *(pwcs + (0 .. n - 1)), (indirect: n);
*/
-size_t wcstombs(char * restrict s, long const * restrict pwcs, size_t n);
+size_t wcstombs(char * restrict s, wchar_t const * restrict pwcs, size_t n);
/*@ requires valid_memptr: \valid(memptr);
requires
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index 31e6f7e6cf06a2c6eda81e4715b264cadf34ece8..37ece5b303d3a0f03e26700b2a7aba6e4b530cb3 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -113,6 +113,7 @@ struct __fc_lldiv_t {
long long rem ;
};
typedef struct __fc_lldiv_t lldiv_t;
+typedef long wchar_t;
struct Aircraft {
int m_id ;
int m_flyCount ;
@@ -2956,7 +2957,7 @@ int mblen(char const *s, size_t n);
\from (indirect: s), *(s + (0 .. n - 1)), (indirect: n),
__fc_mbtowc_state;
*/
-int mbtowc(long * restrict pwc, char const * restrict s, size_t n);
+int mbtowc(wchar_t * restrict pwc, char const * restrict s, size_t n);
/*@ ghost int __fc_wctomb_state; */
/*@ assigns \result, *(s + (0 ..)), __fc_wctomb_state;
@@ -2964,7 +2965,7 @@ int mbtowc(long * restrict pwc, char const * restrict s, size_t n);
assigns *(s + (0 ..)) \from wc, __fc_wctomb_state;
assigns __fc_wctomb_state \from wc, __fc_wctomb_state;
*/
-int wctomb(char *s, long wc);
+int wctomb(char *s, wchar_t wc);
/*@ requires separation: \separated(pwcs, s);
assigns \result, *(pwcs + (0 .. n - 1));
@@ -2973,7 +2974,7 @@ int wctomb(char *s, long wc);
assigns *(pwcs + (0 .. n - 1))
\from (indirect: s), *(s + (0 .. n - 1)), (indirect: n);
*/
-size_t mbstowcs(long * restrict pwcs, char const * restrict s, size_t n);
+size_t mbstowcs(wchar_t * restrict pwcs, char const * restrict s, size_t n);
/*@ requires separation: \separated(s, pwcs);
assigns \result, *(s + (0 .. n - 1));
@@ -2983,7 +2984,7 @@ size_t mbstowcs(long * restrict pwcs, char const * restrict s, size_t n);
assigns *(s + (0 .. n - 1))
\from (indirect: pwcs), *(pwcs + (0 .. n - 1)), (indirect: n);
*/
-size_t wcstombs(char * restrict s, long const * restrict pwcs, size_t n);
+size_t wcstombs(char * restrict s, wchar_t const * restrict pwcs, size_t n);
/*@ requires valid_memptr: \valid(memptr);
requires
diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index 0edccd4ed5e3fa45d6746965895d992e839f8f08..f47a3978400b2b09fa04f35a6693615cf4fc6725 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -103,8 +103,9 @@ struct tm {
int tm_yday ;
int tm_isdst ;
};
+typedef long wchar_t;
typedef char char_type;
-typedef long char_type;
+typedef wchar_t char_type;
struct __shared_ref_base;
struct piecewise_construct_t;
struct piecewise_construct_t {
@@ -2005,7 +2006,7 @@ void tzset(void);
\from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
assigns \result \from dest;
*/
-long *wmemmove(long *dest, long const *src, size_t n);
+wchar_t *wmemmove(wchar_t *dest, wchar_t const *src, size_t n);
/*@ requires valid_wcs: \valid(wcs + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(wcs);
@@ -2017,7 +2018,7 @@ long *wmemmove(long *dest, long const *src, size_t n);
assigns *(wcs + (0 .. n - 1)) \from wc, (indirect: n);
assigns \result \from wcs;
*/
-long *wmemset(long *wcs, long wc, size_t n);
+wchar_t *wmemset(wchar_t *wcs, wchar_t wc, size_t n);
/*@ requires valid_wstring_src: valid_read_wstring(src);
requires valid_wstring_dest: valid_wstring(dest);
@@ -2036,7 +2037,7 @@ long *wmemset(long *wcs, long wc, size_t n);
(indirect: src);
assigns \result \from dest;
*/
-long *wcscat(long * restrict dest, long const * restrict src);
+wchar_t *wcscat(wchar_t * restrict dest, wchar_t const * restrict src);
/*@ requires valid_wstring_src: valid_read_wstring(wcs);
ensures
@@ -2045,7 +2046,7 @@ long *wcscat(long * restrict dest, long const * restrict src);
assigns \result;
assigns \result \from wcs, (indirect: *(wcs + (0 ..))), (indirect: wc);
*/
-long *wcschr(long const *wcs, long wc);
+wchar_t *wcschr(wchar_t const *wcs, wchar_t wc);
/*@ requires valid_wstring_s1: valid_read_wstring(s1);
requires valid_wstring_s2: valid_read_wstring(s2);
@@ -2053,7 +2054,7 @@ long *wcschr(long const *wcs, long wc);
assigns \result
\from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
*/
-int wcscmp(long const *s1, long const *s2);
+int wcscmp(wchar_t const *s1, wchar_t const *s2);
/*@ requires valid_wstring_src: valid_read_wstring(src);
requires room_wstring: \valid(dest + (0 .. wcslen(src)));
@@ -2066,7 +2067,7 @@ int wcscmp(long const *s1, long const *s2);
\from *(src + (0 .. wcslen{Old}(src))), (indirect: src);
assigns \result \from dest;
*/
-long *wcscpy(long * restrict dest, long const * restrict src);
+wchar_t *wcscpy(wchar_t * restrict dest, wchar_t const * restrict src);
/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
requires valid_wstring_accept: valid_read_wstring(accept);
@@ -2074,7 +2075,7 @@ long *wcscpy(long * restrict dest, long const * restrict src);
assigns \result
\from (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
*/
-size_t wcscspn(long const *wcs, long const *accept);
+size_t wcscspn(wchar_t const *wcs, wchar_t const *accept);
/*@ requires valid_nwstring_src: valid_read_nwstring(src, n);
requires valid_wstring_dest: valid_wstring(dest);
@@ -2094,7 +2095,8 @@ size_t wcscspn(long const *wcs, long const *accept);
\from (indirect: *(dest + (0 ..))), (indirect: *(src + (0 .. n - 1))),
(indirect: n);
*/
-size_t wcslcat(long * restrict dest, long const * restrict src, size_t n);
+size_t wcslcat(wchar_t * restrict dest, wchar_t const * restrict src,
+ size_t n);
/*@ requires valid_wstring_src: valid_read_wstring(src);
requires room_nwstring: \valid(dest + (0 .. n));
@@ -2108,14 +2110,14 @@ size_t wcslcat(long * restrict dest, long const * restrict src, size_t n);
\from (indirect: *(dest + (0 .. n - 1))), (indirect: dest),
(indirect: *(src + (0 .. n - 1))), (indirect: src), (indirect: n);
*/
-size_t wcslcpy(long *dest, long const *src, size_t n);
+size_t wcslcpy(wchar_t *dest, wchar_t const *src, size_t n);
/*@ requires valid_string_s: valid_read_wstring(s);
ensures result_is_length: \result ≡ wcslen(\old(s));
assigns \result;
assigns \result \from (indirect: *(s + (0 .. wcslen{Old}(s))));
*/
-size_t wcslen(long const *s);
+size_t wcslen(wchar_t const *s);
/*@ requires valid_nwstring_src: valid_read_nwstring(src, n);
requires valid_wstring_dest: valid_wstring(dest);
@@ -2134,7 +2136,8 @@ size_t wcslen(long const *s);
(indirect: src), (indirect: n);
assigns \result \from dest;
*/
-long *wcsncat(long * restrict dest, long const * restrict src, size_t n);
+wchar_t *wcsncat(wchar_t * restrict dest, wchar_t const * restrict src,
+ size_t n);
/*@ requires valid_wstring_s1: valid_read_wstring(s1);
requires valid_wstring_s2: valid_read_wstring(s2);
@@ -2143,7 +2146,7 @@ long *wcsncat(long * restrict dest, long const * restrict src, size_t n);
\from (indirect: *(s1 + (0 .. n - 1))),
(indirect: *(s2 + (0 .. n - 1))), (indirect: n);
*/
-int wcsncmp(long const *s1, long const *s2, size_t n);
+int wcsncmp(wchar_t const *s1, wchar_t const *s2, size_t n);
/*@ requires valid_wstring_src: valid_read_wstring(src);
requires room_nwstring: \valid(dest + (0 .. n - 1));
@@ -2157,7 +2160,8 @@ int wcsncmp(long const *s1, long const *s2, size_t n);
\from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
assigns \result \from dest;
*/
-long *wcsncpy(long * restrict dest, long const * restrict src, size_t n);
+wchar_t *wcsncpy(wchar_t * restrict dest, wchar_t const * restrict src,
+ size_t n);
/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
requires valid_wstring_accept: valid_read_wstring(accept);
@@ -2168,7 +2172,7 @@ long *wcsncpy(long * restrict dest, long const * restrict src, size_t n);
assigns \result
\from wcs, (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
*/
-long *wcspbrk(long const *wcs, long const *accept);
+wchar_t *wcspbrk(wchar_t const *wcs, wchar_t const *accept);
/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
ensures
@@ -2178,7 +2182,7 @@ long *wcspbrk(long const *wcs, long const *accept);
assigns \result
\from wcs, (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))), (indirect: wc);
*/
-long *wcsrchr(long const *wcs, long wc);
+wchar_t *wcsrchr(wchar_t const *wcs, wchar_t wc);
/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
requires valid_wstring_accept: valid_read_wstring(accept);
@@ -2187,7 +2191,7 @@ long *wcsrchr(long const *wcs, long wc);
\from (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))),
(indirect: *(accept + (0 .. wcslen{Old}(accept))));
*/
-size_t wcsspn(long const *wcs, long const *accept);
+size_t wcsspn(wchar_t const *wcs, wchar_t const *accept);
/*@ requires valid_wstring_haystack: valid_read_wstring(haystack);
requires valid_wstring_needle: valid_read_wstring(needle);
@@ -2199,7 +2203,7 @@ size_t wcsspn(long const *wcs, long const *accept);
\from haystack, (indirect: *(haystack + (0 ..))),
(indirect: *(needle + (0 ..)));
*/
-long *wcsstr(long const *haystack, long const *needle);
+wchar_t *wcsstr(wchar_t const *haystack, wchar_t const *needle);
/*@ requires room_nwstring: \valid(ws + (0 .. n - 1));
requires valid_stream: \valid(stream);
@@ -2211,7 +2215,7 @@ long *wcsstr(long const *haystack, long const *needle);
assigns *(ws + (0 .. n - 1)) \from (indirect: n), (indirect: *stream);
assigns \result \from ws, (indirect: n), (indirect: *stream);
*/
-long *fgetws(long * restrict ws, int n, FILE * restrict stream);
+wchar_t *fgetws(wchar_t * restrict ws, int n, FILE * restrict stream);
/*@ axiomatic wformat_length {
logic ℤ wformat_length{L}(long *format) ;
@@ -2225,7 +2229,7 @@ long *fgetws(long * restrict ws, int n, FILE * restrict stream);
assigns \result
\from (indirect: *(ws1 + (0 ..))), (indirect: *(ws2 + (0 ..)));
*/
-int wcscasecmp(long const *ws1, long const *ws2);
+int wcscasecmp(wchar_t const *ws1, wchar_t const *ws2);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;