diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index d5fabe311..62eb74878 100644 --- a/charon-ml/src/CharonVersion.ml +++ b/charon-ml/src/CharonVersion.ml @@ -1,3 +1,3 @@ (* This is an automatically generated file, generated from `charon/Cargo.toml`. *) (* To re-generate this file, rune `make` in the root directory *) -let supported_charon_version = "0.1.159" +let supported_charon_version = "0.1.160" diff --git a/charon-ml/src/GAst.ml b/charon-ml/src/GAst.ml index f1aae0bf6..1c9a9f9d0 100644 --- a/charon-ml/src/GAst.ml +++ b/charon-ml/src/GAst.ml @@ -30,6 +30,7 @@ type mixed_declaration_group = item_id g_declaration_group [@@deriving show] type 'body gfun_decl = { def_id : FunDeclId.id; item_meta : item_meta; + generics : generic_params; signature : fun_sig; src : item_source; is_global_initializer : GlobalDeclId.id option; diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml index 54b8e51e0..8993a0404 100644 --- a/charon-ml/src/GAstOfJson.ml +++ b/charon-ml/src/GAstOfJson.ml @@ -29,6 +29,7 @@ let rec gfun_decl_of_json [ ("def_id", def_id); ("item_meta", item_meta); + ("generics", generics); ("signature", signature); ("src", src); ("is_global_initializer", is_global_initializer); @@ -36,13 +37,23 @@ let rec gfun_decl_of_json ] -> let* def_id = FunDeclId.id_of_json ctx def_id in let* item_meta = item_meta_of_json ctx item_meta in + let* generics = generic_params_of_json ctx generics in let* signature = fun_sig_of_json ctx signature in let* src = item_source_of_json ctx src in let* is_global_initializer = option_of_json global_decl_id_of_json ctx is_global_initializer in let* body = body_of_json ctx body in - Ok { def_id; item_meta; signature; src; is_global_initializer; body } + Ok + { + def_id; + item_meta; + generics; + signature; + src; + is_global_initializer; + body; + } | _ -> Error "") (** Deserialize a map from file id to file name. diff --git a/charon-ml/src/GAstUtils.ml b/charon-ml/src/GAstUtils.ml index 9a149825c..9e56ca1b0 100644 --- a/charon-ml/src/GAstUtils.ml +++ b/charon-ml/src/GAstUtils.ml @@ -1,4 +1,5 @@ open Types +open TypesUtils open GAst (** Small utility: list the transitive parents of a region var group. We don't @@ -41,15 +42,10 @@ let locals_get_input_vars (locals : locals) : local list = let fun_body_get_input_vars (fbody : 'body gexpr_body) : local list = locals_get_input_vars fbody.locals -(** Like `binder` but for the free variables bound by the generics of an item. - This is not present in the charon ast but returned by helpers so we don't - forget to substitute. Use `Substitute.apply_args_to_item_binder` to get the - correctly-substituted inner value. *) -type 'a item_binder = { - item_binder_params : generic_params; - item_binder_value : 'a; -} -[@@deriving show, ord] +(** Get the signature of this function as a bound value, i.e. including its + generics parameters. *) +let bound_fun_sig_of_decl (def : 'a gfun_decl) : bound_fun_sig = + { item_binder_params = def.generics; item_binder_value = def.signature } (** Lookup a method in this trait decl. The two levels of binders in the output reflect that there are two binding levels: the trait generics and the method diff --git a/charon-ml/src/LlbcAstUtils.ml b/charon-ml/src/LlbcAstUtils.ml index 31d45c9ce..4cc90b24c 100644 --- a/charon-ml/src/LlbcAstUtils.ml +++ b/charon-ml/src/LlbcAstUtils.ml @@ -106,12 +106,21 @@ class ['self] map_crate_with_span = method visit_fun_decl (_ : (item_id * span) option) (decl : fun_decl) : fun_decl = - let { def_id; item_meta; signature; src; is_global_initializer; body } = + let { + def_id; + item_meta; + generics; + signature; + src; + is_global_initializer; + body; + } = decl in let decl_span_info = Some (IdFun def_id, item_meta.span) in let def_id = self#visit_fun_decl_id decl_span_info def_id in let item_meta = self#visit_item_meta decl_span_info item_meta in + let generics = self#visit_generic_params decl_span_info generics in let signature = self#visit_fun_sig decl_span_info signature in let src = self#visit_item_source decl_span_info src in let is_global_initializer = @@ -119,7 +128,15 @@ class ['self] map_crate_with_span = is_global_initializer in let body = self#visit_option self#visit_expr_body decl_span_info body in - { def_id; item_meta; signature; src; is_global_initializer; body } + { + def_id; + item_meta; + generics; + signature; + src; + is_global_initializer; + body; + } method! visit_global_decl (_ : (item_id * span) option) (decl : global_decl) = @@ -293,12 +310,21 @@ class ['self] iter_crate_with_span = method visit_fun_decl (_ : (item_id * span) option) (decl : fun_decl) : unit = - let { def_id; item_meta; signature; src; is_global_initializer; body } = + let { + def_id; + item_meta; + generics; + signature; + src; + is_global_initializer; + body; + } = decl in let decl_span_info = Some (IdFun def_id, item_meta.span) in self#visit_fun_decl_id decl_span_info def_id; self#visit_item_meta decl_span_info item_meta; + self#visit_generic_params decl_span_info generics; self#visit_fun_sig decl_span_info signature; self#visit_item_source decl_span_info src; self#visit_option self#visit_global_decl_id decl_span_info diff --git a/charon-ml/src/NameMatcher.ml b/charon-ml/src/NameMatcher.ml index 6ede3e80a..a0a0f4ff7 100644 --- a/charon-ml/src/NameMatcher.ml +++ b/charon-ml/src/NameMatcher.ml @@ -580,7 +580,7 @@ and match_expr_with_ty (ctx : 'fun_body ctx) (c : match_config) (m : maps) let m = maps_push_bound_regions_group_if_nonempty m binder.binder_regions in - let inputs, output = binder.binder_value in + let { T.inputs; output; _ } = binder.binder_value in (* Match *) List.for_all2 (match_expr_with_ty ctx c m) pinputs inputs && @@ -770,8 +770,7 @@ let match_fn_ptr (ctx : 'fun_body ctx) (c : match_config) (p : pattern) | TraitImplItem (_, trait_ref, method_name, _) when c.match_with_trait_decl_refs -> let subst = - Substitute.make_subst_from_generics d.signature.generics - func.generics + Substitute.make_subst_from_generics d.generics func.generics in let trait_ref = Substitute.trait_decl_ref_substitute subst trait_ref @@ -1023,7 +1022,7 @@ and ty_to_pattern_aux (ctx : 'fun_body ctx) (c : to_pat_config) let m = constraints_map_push_regions_map_if_nonempty m binder.binder_regions in - let inputs, output = binder.binder_value in + let { T.inputs; output; _ } = binder.binder_value in let inputs = List.map (ty_to_pattern_aux ctx c m) inputs in let output = if output = TypesUtils.mk_unit_ty then None diff --git a/charon-ml/src/PrintGAst.ml b/charon-ml/src/PrintGAst.ml index 647a09770..bf645e34b 100644 --- a/charon-ml/src/PrintGAst.ml +++ b/charon-ml/src/PrintGAst.ml @@ -3,6 +3,7 @@ open Types open TypesUtils open GAst +open GAstUtils open PrintUtils open PrintTypes open PrintExpressions @@ -36,7 +37,8 @@ let assertion_to_string (env : 'a fmt_env) (indent : string) (a : assertion) : (** Small helper *) let fun_sig_with_name_to_string (env : 'a fmt_env) (indent : string) (indent_incr : string) (attribute : string option) (name : string option) - (args : local list option) (sg : fun_sig) : string = + (args : local list option) (sg : bound_fun_sig) : string = + let { item_binder_params = generics; item_binder_value = sg; _ } = sg in let ty_to_string = ty_to_string env in (* Unsafe keyword *) @@ -44,7 +46,7 @@ let fun_sig_with_name_to_string (env : 'a fmt_env) (indent : string) (* Generics and predicates *) let params, clauses = - predicates_and_trait_clauses_to_string env indent indent_incr sg.generics + predicates_and_trait_clauses_to_string env indent indent_incr generics in let params = if params = [] then "" else "<" ^ String.concat ", " params ^ ">" @@ -85,7 +87,7 @@ let fun_sig_with_name_to_string (env : 'a fmt_env) (indent : string) ^ clauses let fun_sig_to_string (env : 'a fmt_env) (indent : string) - (indent_incr : string) (sg : fun_sig) : string = + (indent_incr : string) (sg : fun_sig item_binder) : string = fun_sig_with_name_to_string env indent indent_incr None None None sg let gfun_decl_to_string (env : 'a fmt_env) (indent : string) @@ -93,7 +95,7 @@ let gfun_decl_to_string (env : 'a fmt_env) (indent : string) (body_to_string : 'a fmt_env -> string -> string -> 'body -> string) (def : 'body gfun_decl) : string = (* Locally update the environment *) - let env = fmt_env_update_generics_and_preds env def.signature.generics in + let env = fmt_env_update_generics_and_preds env def.generics in let sg = def.signature in @@ -102,6 +104,7 @@ let gfun_decl_to_string (env : 'a fmt_env) (indent : string) (* We print the declaration differently if it is opaque (no body) or transparent * (we have access to a body) *) + let sg = bound_fun_sig_of_decl def in match def.body with | None -> fun_sig_with_name_to_string env indent indent_incr (Some "opaque") diff --git a/charon-ml/src/PrintLlbcAst.ml b/charon-ml/src/PrintLlbcAst.ml index 4cd572565..f40036aef 100644 --- a/charon-ml/src/PrintLlbcAst.ml +++ b/charon-ml/src/PrintLlbcAst.ml @@ -117,9 +117,7 @@ module Ast = struct String.concat ";\n" (List.map (statement_to_string env indent indent_incr) b.statements) - let fun_sig_to_string (env : fmt_env) (indent : string) (indent_incr : string) - (sg : fun_sig) : string = - fun_sig_to_string env indent indent_incr sg + let fun_sig_to_string = fun_sig_to_string let fun_decl_to_string (env : fmt_env) (indent : string) (indent_incr : string) (def : fun_decl) : string = diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index a14047c00..1abc36f4e 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -286,7 +286,7 @@ and ty_to_string (env : 'a fmt_env) (ty : ty) : string = | RShared -> "*const " ^ ty_to_string env rty) | TFnPtr binder -> let env = fmt_env_push_regions env binder.binder_regions in - let inputs, output = binder.binder_value in + let { inputs; output; _ } = binder.binder_value in let inputs = "(" ^ String.concat ", " (List.map (ty_to_string env) inputs) ^ ") -> " in diff --git a/charon-ml/src/Substitute.ml b/charon-ml/src/Substitute.ml index bcae914c4..57fbe0bd0 100644 --- a/charon-ml/src/Substitute.ml +++ b/charon-ml/src/Substitute.ml @@ -615,7 +615,7 @@ let lookup_method_sig (crate : 'a gcrate) (trait_id : trait_decl_id) (* Substitute the signature to be valid under the binder. *) let signature = st_substitute_visitor#visit_fun_sig - (make_subst_from_generics method_decl.signature.generics + (make_subst_from_generics method_decl.generics bound_method.binder_value.generics) method_decl.signature in @@ -625,22 +625,18 @@ let lookup_method_sig (crate : 'a gcrate) (trait_id : trait_decl_id) in Some { item_binder_params = trait_params; item_binder_value = bound_sig } -(* Like [lookup_method_sig], but with no binder shenanigans: the returns - fun_sig takes as parameters the concatenation of trait generics and method - generics. *) +(* Like [lookup_method_sig], but with no binder shenanigans: the returned + binder binds the concatenation of trait generics and method generics. *) let lookup_flat_method_sig (crate : 'a gcrate) (trait_id : trait_decl_id) - (name : trait_item_name) : fun_sig option = + (name : trait_item_name) : bound_fun_sig option = let* bound_sig = lookup_method_sig crate trait_id name in let bound_sig = fuse_binders st_substitute_visitor#visit_fun_sig bound_sig in - let s = - { bound_sig.item_binder_value with generics = bound_sig.item_binder_params } - in - Some s + Some bound_sig (* Lookup the signature of a `Ty::FnDef`. *) -let lookup_fndef_sig (crate : 'a gcrate) (fn_def : fn_ptr region_binder) : - (ty list * ty) region_binder option = - match fn_def.binder_value.kind with +let lookup_fndef_sig (crate : 'a gcrate) (fn_ptr : fn_ptr region_binder) : + fun_sig region_binder option = + match fn_ptr.binder_value.kind with | FunId (FRegular fun_decl_id) -> let* fun_decl = LlbcAst.FunDeclId.Map.find_opt fun_decl_id crate.fun_decls @@ -648,16 +644,12 @@ let lookup_fndef_sig (crate : 'a gcrate) (fn_def : fn_ptr region_binder) : (* Substitute the signature to be valid under the binder. *) let fn_sig = st_substitute_visitor#visit_fun_sig - (make_subst_from_generics fun_decl.signature.generics - fn_def.binder_value.generics) + (make_subst_from_generics fun_decl.generics + fn_ptr.binder_value.generics) fun_decl.signature in (* Rebind everything *) - Some - { - binder_regions = fn_def.binder_regions; - binder_value = (fn_sig.inputs, fn_sig.output); - } + Some { binder_regions = fn_ptr.binder_regions; binder_value = fn_sig } | _ -> None (* Construct a set of generic arguments in the scope of `params` that matches diff --git a/charon-ml/src/TypesUtils.ml b/charon-ml/src/TypesUtils.ml index eda271342..22cf1b21b 100644 --- a/charon-ml/src/TypesUtils.ml +++ b/charon-ml/src/TypesUtils.ml @@ -15,6 +15,18 @@ end module RegionMap = Collections.MakeMap (RegionOrderedType) module RegionSet = Collections.MakeSet (RegionOrderedType) +(** Like `binder` but for the free variables bound by the generics of an item. + This is not present in the charon ast but returned by helpers so we don't + forget to substitute. Use `Substitute.apply_args_to_item_binder` to get the + correctly-substituted inner value. *) +type 'a item_binder = { + item_binder_params : generic_params; + item_binder_value : 'a; +} +[@@deriving show, ord] + +type bound_fun_sig = fun_sig item_binder + let to_name (ls : string list) : name = List.map (fun s -> PeIdent (s, Disambiguator.zero)) ls diff --git a/charon-ml/src/generated/Generated_GAst.ml b/charon-ml/src/generated/Generated_GAst.ml index c60a378ba..2c5a7bf53 100644 --- a/charon-ml/src/generated/Generated_GAst.ml +++ b/charon-ml/src/generated/Generated_GAst.ml @@ -95,14 +95,6 @@ and fn_operand = (** Regular case: call to a top-level function, trait method, etc. *) | FnOpDynamic of operand (** Use of a function pointer. *) -(** A function signature. *) -and fun_sig = { - is_unsafe : bool; (** Is the function unsafe or not *) - generics : generic_params; - inputs : ty list; - output : ty; -} - (** A variable *) and local = { index : local_id; (** Unique index identifying the variable *) diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml index aa1ab3563..78f17a017 100644 --- a/charon-ml/src/generated/Generated_GAstOfJson.ml +++ b/charon-ml/src/generated/Generated_GAstOfJson.ml @@ -529,11 +529,7 @@ and closure_info_of_json (ctx : of_json_ctx) (js : json) : (region_binder_of_json trait_impl_ref_of_json) ctx fn_impl in - let* signature = - region_binder_of_json - (pair_of_json (list_of_json ty_of_json) ty_of_json) - ctx signature - in + let* signature = region_binder_of_json fun_sig_of_json ctx signature in Ok ({ kind; fn_once_impl; fn_mut_impl; fn_impl; signature } : closure_info) @@ -911,17 +907,11 @@ and fun_sig_of_json (ctx : of_json_ctx) (js : json) : (fun_sig, string) result = combine_error_msgs js __FUNCTION__ (match js with | `Assoc - [ - ("is_unsafe", is_unsafe); - ("generics", generics); - ("inputs", inputs); - ("output", output); - ] -> + [ ("is_unsafe", is_unsafe); ("inputs", inputs); ("output", output) ] -> let* is_unsafe = bool_of_json ctx is_unsafe in - let* generics = generic_params_of_json ctx generics in let* inputs = list_of_json ty_of_json ctx inputs in let* output = ty_of_json ctx output in - Ok ({ is_unsafe; generics; inputs; output } : fun_sig) + Ok ({ is_unsafe; inputs; output } : fun_sig) | _ -> Error "") and g_declaration_group_of_json : @@ -2148,11 +2138,7 @@ and ty_kind_of_json (ctx : of_json_ctx) (js : json) : (ty_kind, string) result = let* dyn_trait = dyn_predicate_of_json ctx dyn_trait in Ok (TDynTrait dyn_trait) | `Assoc [ ("FnPtr", fn_ptr) ] -> - let* fn_ptr = - region_binder_of_json - (pair_of_json (list_of_json ty_of_json) ty_of_json) - ctx fn_ptr - in + let* fn_ptr = region_binder_of_json fun_sig_of_json ctx fn_ptr in Ok (TFnPtr fn_ptr) | `Assoc [ ("FnDef", fn_def) ] -> let* fn_def = region_binder_of_json fn_ptr_of_json ctx fn_def in diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml index 5d342cad0..e9fefa0c4 100644 --- a/charon-ml/src/generated/Generated_Types.ml +++ b/charon-ml/src/generated/Generated_Types.ml @@ -353,6 +353,13 @@ and fun_id = (** A primitive function, coming from a standard library (for instance: [alloc::boxed::Box::new]). TODO: rename to "Primitive" *) +(** A function signature. *) +and fun_sig = { + is_unsafe : bool; (** Is the function unsafe or not *) + inputs : ty list; + output : ty; +} + (** A set of generic arguments. *) and generic_args = { regions : region list; @@ -600,7 +607,7 @@ and ty_kind = } ]} *) | TDynTrait of dyn_predicate (** [dyn Trait] *) - | TFnPtr of (ty list * ty) region_binder + | TFnPtr of fun_sig region_binder (** Function pointer type. This is a literal pointer to a region of memory that contains a callable function. This is a function signature with limited generics: it only supports lifetime generics, not other kinds @@ -691,7 +698,7 @@ and closure_info = { (** The [FnMut] implementation of this closure, if any. *) fn_impl : trait_impl_ref region_binder option; (** The [Fn] implementation of this closure, if any. *) - signature : (ty list * ty) region_binder; + signature : fun_sig region_binder; (** The signature of the function that this closure represents. *) } diff --git a/charon-ml/tests/Test_NameMatcher.ml b/charon-ml/tests/Test_NameMatcher.ml index f2e34493d..89462452c 100644 --- a/charon-ml/tests/Test_NameMatcher.ml +++ b/charon-ml/tests/Test_NameMatcher.ml @@ -121,8 +121,7 @@ module PatternTest = struct match test.call_idx with | None -> let generics = - TypesUtils.generic_args_of_params decl.item_meta.span - decl.signature.generics + TypesUtils.generic_args_of_params decl.item_meta.span decl.generics in Types.{ kind = FunId (FRegular decl.def_id); generics } | Some idx -> @@ -161,8 +160,7 @@ module PatternTest = struct log#error "Pattern %s failed to match function %s (in `%s`)\n" (pattern_to_string env.print_config test.pattern) (pattern_to_string env.print_config - (fn_ptr_to_pattern env.ctx env.to_pat_config decl.signature.generics - fn_ptr)) + (fn_ptr_to_pattern env.ctx env.to_pat_config decl.generics fn_ptr)) env.file_name; false) else if (not test.success) && match_success then ( diff --git a/charon/Cargo.lock b/charon/Cargo.lock index cd4ffa99b..8a85d9dcc 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -219,7 +219,7 @@ checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268" [[package]] name = "charon" -version = "0.1.159" +version = "0.1.160" dependencies = [ "annotate-snippets", "anstream", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index f3f830b86..86d3ce7da 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "charon" -version = "0.1.159" +version = "0.1.160" authors = [ "Son Ho ", "Guillaume Boisseau ", diff --git a/charon/src/ast/gast.rs b/charon/src/ast/gast.rs index 847d46375..0d5e8ed48 100644 --- a/charon/src/ast/gast.rs +++ b/charon/src/ast/gast.rs @@ -189,6 +189,7 @@ pub struct FunDecl { pub def_id: FunDeclId, /// The meta data associated with the declaration. pub item_meta: ItemMeta, + pub generics: GenericParams, /// The signature contains the inputs/output types *with* non-erased regions. /// It also contains the list of region and type parameters. pub signature: FunSig, diff --git a/charon/src/ast/gast_utils.rs b/charon/src/ast/gast_utils.rs index d506a8680..89ea44c19 100644 --- a/charon/src/ast/gast_utils.rs +++ b/charon/src/ast/gast_utils.rs @@ -88,22 +88,19 @@ impl FunDecl { let FunDecl { def_id, item_meta, + generics: _, signature, - src: kind, + src, is_global_initializer, body, } = self; - let signature = FunSig { - generics: subst.params, - inputs: signature.inputs.substitute(&subst.skip_binder), - output: signature.output.substitute(&subst.skip_binder), - ..signature - }; - let src = kind.substitute(&subst.skip_binder); + let signature = signature.substitute(&subst.skip_binder); + let src = src.substitute(&subst.skip_binder); let body = body.substitute(&subst.skip_binder); FunDecl { def_id, item_meta, + generics: subst.params, signature, src, is_global_initializer, diff --git a/charon/src/ast/krate.rs b/charon/src/ast/krate.rs index f956b9cc1..b8305d9fb 100644 --- a/charon/src/ast/krate.rs +++ b/charon/src/ast/krate.rs @@ -355,7 +355,7 @@ impl<'ctx> ItemRef<'ctx> { pub fn generic_params(&self) -> &'ctx GenericParams { match self { ItemRef::Type(d) => &d.generics, - ItemRef::Fun(d) => &d.signature.generics, + ItemRef::Fun(d) => &d.generics, ItemRef::Global(d) => &d.generics, ItemRef::TraitDecl(d) => &d.generics, ItemRef::TraitImpl(d) => &d.generics, @@ -446,7 +446,7 @@ impl<'ctx> ItemRefMut<'ctx> { pub fn generic_params(&mut self) -> &mut GenericParams { match self { ItemRefMut::Type(d) => &mut d.generics, - ItemRefMut::Fun(d) => &mut d.signature.generics, + ItemRefMut::Fun(d) => &mut d.generics, ItemRefMut::Global(d) => &mut d.generics, ItemRefMut::TraitDecl(d) => &mut d.generics, ItemRefMut::TraitImpl(d) => &mut d.generics, diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 392dcf9b0..1e8092140 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -877,7 +877,7 @@ pub enum TyKind { /// contains a callable function. /// This is a function signature with limited generics: it only supports lifetime generics, not /// other kinds of generics. - FnPtr(RegionBinder<(Vec, Ty)>), + FnPtr(RegionBinder), /// The unique type associated with each function item. Each function item is given /// a unique generic type that takes as input the function's early-bound generics. This type /// is not generally nameable in Rust; it's a ZST (there's a unique value), and a value of that type @@ -977,16 +977,15 @@ pub struct ClosureInfo { /// The `Fn` implementation of this closure, if any. pub fn_impl: Option>, /// The signature of the function that this closure represents. - pub signature: RegionBinder<(Vec, Ty)>, + pub signature: RegionBinder, } /// A function signature. -#[derive(Debug, Clone, PartialEq, Eq, SerializeState, DeserializeState, Drive, DriveMut)] +#[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)] pub struct FunSig { /// Is the function unsafe or not #[drive(skip)] pub is_unsafe: bool, - pub generics: GenericParams, pub inputs: Vec, pub output: Ty, } diff --git a/charon/src/bin/charon-driver/translate/translate_closures.rs b/charon/src/bin/charon-driver/translate/translate_closures.rs index 700e195f7..4aa64c056 100644 --- a/charon/src/bin/charon-driver/translate/translate_closures.rs +++ b/charon/src/bin/charon-driver/translate/translate_closures.rs @@ -76,7 +76,7 @@ impl ItemTransCtx<'_, '_> { } else { None }; - let signature = self.translate_fun_sig(span, &args.fn_sig)?; + let signature = self.translate_poly_fun_sig(span, &args.fn_sig)?; Ok(ClosureInfo { kind, fn_once_impl, @@ -283,10 +283,7 @@ impl ItemTransCtx<'_, '_> { signature.value, ); - let is_unsafe = match signature.value.safety { - hax::Safety::Unsafe => true, - hax::Safety::Safe => false, - }; + let mut fun_sig = self.translate_fun_sig(span, signature.hax_skip_binder_ref())?; let state_ty = self.get_closure_state_ty(span, args)?; @@ -309,26 +306,15 @@ impl ItemTransCtx<'_, '_> { }; // The types that the closure takes as input. - let input_tys: Vec = signature - .value - .inputs - .iter() - .map(|ty| self.translate_ty(span, ty)) - .try_collect()?; + let input_tys: Vec = mem::take(&mut fun_sig.inputs); // The method takes `self` and the closure inputs as a tuple. - let inputs = vec![state_ty, Ty::mk_tuple(input_tys)]; - let output = self.translate_ty(span, &signature.value.output)?; - - Ok(FunSig { - generics: self.the_only_binder().params.clone(), - is_unsafe, - inputs, - output, - }) + fun_sig.inputs = vec![state_ty, Ty::mk_tuple(input_tys)]; + + Ok(fun_sig) } fn translate_closure_method_body( - mut self, + &mut self, span: Span, def: &hax::FullDef, target_kind: ClosureKind, @@ -536,6 +522,7 @@ impl ItemTransCtx<'_, '_> { Ok(FunDecl { def_id, item_meta, + generics: self.into_generics(), signature, src, is_global_initializer: None, @@ -642,11 +629,8 @@ impl ItemTransCtx<'_, '_> { .push_params_from_binder(closure.fn_sig.rebind(()))?; // Translate the function signature - let mut signature = - self.translate_closure_method_sig(def, span, closure, ClosureKind::FnOnce)?; - let state_ty = signature.inputs.remove(0); - let args_tuple_ty = signature.inputs.remove(0); - signature.inputs = args_tuple_ty.as_tuple().unwrap().iter().cloned().collect(); + let signature = self.translate_fun_sig(span, closure.fn_sig.hax_skip_binder_ref())?; + let state_ty = self.get_closure_state_ty(span, closure)?; let body = if item_meta.opacity.with_private_contents().is_opaque() { Body::Opaque @@ -675,13 +659,14 @@ impl ItemTransCtx<'_, '_> { .enumerate() .map(|(i, ty)| builder.new_var(Some(format!("arg{}", i + 1)), ty.clone())) .collect(); - let args_tupled = builder.new_var(Some("args".to_string()), args_tuple_ty.clone()); + let args_tupled_ty = Ty::mk_tuple(signature.inputs.clone()); + let args_tupled = builder.new_var(Some("args".to_string()), args_tupled_ty.clone()); let state = builder.new_var(Some("state".to_string()), state_ty.clone()); builder.push_statement(StatementKind::Assign( args_tupled.clone(), Rvalue::Aggregate( - AggregateKind::Adt(args_tuple_ty.as_adt().unwrap().clone(), None, None), + AggregateKind::Adt(args_tupled_ty.as_adt().unwrap().clone(), None, None), args.into_iter().map(Operand::Move).collect(), ), )); @@ -704,6 +689,7 @@ impl ItemTransCtx<'_, '_> { Ok(FunDecl { def_id, item_meta, + generics: self.into_generics(), signature, src: ItemSource::TopLevel, is_global_initializer: None, diff --git a/charon/src/bin/charon-driver/translate/translate_drops.rs b/charon/src/bin/charon-driver/translate/translate_drops.rs index 2b3ae6e45..eebb99d77 100644 --- a/charon/src/bin/charon-driver/translate/translate_drops.rs +++ b/charon/src/bin/charon-driver/translate/translate_drops.rs @@ -119,8 +119,7 @@ impl ItemTransCtx<'_, '_> { let input = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty(); let signature = FunSig { - generics: self.into_generics(), - is_unsafe: false, + is_unsafe: true, inputs: vec![input], output: Ty::mk_unit(), }; @@ -128,6 +127,7 @@ impl ItemTransCtx<'_, '_> { Ok(FunDecl { def_id, item_meta, + generics: self.into_generics(), signature, src, is_global_initializer: None, diff --git a/charon/src/bin/charon-driver/translate/translate_functions.rs b/charon/src/bin/charon-driver/translate/translate_functions.rs index 1fa85f2b5..9d897b980 100644 --- a/charon/src/bin/charon-driver/translate/translate_functions.rs +++ b/charon/src/bin/charon-driver/translate/translate_functions.rs @@ -3,107 +3,29 @@ //! us to handle, and easier to maintain - rustc's representation can evolve //! independently. -use std::panic; - use super::translate_ctx::*; use charon_lib::ast::ullbc_ast_utils::BodyBuilder; use charon_lib::ast::*; -use charon_lib::common::*; -use charon_lib::formatter::IntoFormatter; -use charon_lib::pretty::FmtWithCtx; use charon_lib::ullbc_ast::*; use itertools::Itertools; impl ItemTransCtx<'_, '_> { - /// Translate a function's signature, and initialize a body translation context - /// at the same time - the function signature gives us the list of region and - /// type parameters, that we put in the translation context. - pub(crate) fn translate_function_signature( - &mut self, - def: &hax::FullDef, - item_meta: &ItemMeta, - ) -> Result { - let span = item_meta.span; - - self.translate_def_generics(span, def)?; - - let signature = match &def.kind { - hax::FullDefKind::Fn { sig, .. } => sig, - hax::FullDefKind::AssocFn { sig, .. } => sig, - hax::FullDefKind::Ctor { - fields, output_ty, .. - } => { - let sig = hax::TyFnSig { - inputs: fields.iter().map(|field| field.ty.clone()).collect(), - output: output_ty.clone(), - c_variadic: false, - safety: hax::Safety::Safe, - abi: hax::ExternAbi::Rust, - }; - &hax::Binder { - value: sig, - bound_vars: Default::default(), - } - } - hax::FullDefKind::Const { ty, .. } - | hax::FullDefKind::AssocConst { ty, .. } - | hax::FullDefKind::Static { ty, .. } => { - let sig = hax::TyFnSig { - inputs: vec![], - output: ty.clone(), - c_variadic: false, - safety: hax::Safety::Safe, - abi: hax::ExternAbi::Rust, - }; - &hax::Binder { - value: sig, - bound_vars: Default::default(), - } - } - _ => panic!("Unexpected definition for function: {def:?}"), - }; - - // Translate the signature - trace!("signature of {:?}:\n{:?}", def.def_id(), signature.value); - let inputs: Vec = signature - .value - .inputs - .iter() - .map(|ty| self.translate_ty(span, ty)) - .try_collect()?; - let output = self.translate_ty(span, &signature.value.output)?; - - let fmt_ctx = &self.into_fmt(); - trace!( - "# Input variables types:\n{}", - pretty_display_list(|x| x.to_string_with_ctx(fmt_ctx), &inputs) - ); - trace!("# Output variable type:\n{}", output.with_ctx(fmt_ctx)); - - let is_unsafe = match signature.value.safety { - hax::Safety::Unsafe => true, - hax::Safety::Safe => false, - }; - - Ok(FunSig { - generics: self.the_only_binder().params.clone(), - is_unsafe, - inputs, - output, - }) - } - /// Generate a fake function body for ADT constructors. pub(crate) fn build_ctor_body( &mut self, span: Span, def: &hax::FullDef, - adt_def_id: &hax::DefId, - ctor_of: &hax::CtorOf, - variant_id: usize, - fields: &hax::IndexVec, - output_ty: &hax::Ty, ) -> Result { + let hax::FullDefKind::Ctor { + adt_def_id, + ctor_of, + variant_id, + fields, + output_ty, + } = def.kind() + else { + unreachable!() + }; let tref = self .translate_type_decl_ref(span, &def.this().with_def_id(self.hax_state(), adt_def_id))?; let output_ty = self.translate_ty(span, output_ty)?; @@ -120,7 +42,7 @@ impl ItemTransCtx<'_, '_> { .try_collect()?; let variant = match ctor_of { hax::CtorOf::Struct => None, - hax::CtorOf::Variant => Some(VariantId::from(variant_id)), + hax::CtorOf::Variant => Some(VariantId::from(*variant_id)), }; builder.push_statement(StatementKind::Assign( return_place, diff --git a/charon/src/bin/charon-driver/translate/translate_items.rs b/charon/src/bin/charon-driver/translate/translate_items.rs index 44560a57d..52ff9bdf1 100644 --- a/charon/src/bin/charon-driver/translate/translate_items.rs +++ b/charon/src/bin/charon-driver/translate/translate_items.rs @@ -255,9 +255,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { item_meta: item_meta.clone(), src: ItemSource::TopLevel, is_global_initializer: Some(global_id), + generics: Default::default(), signature: FunSig { is_unsafe: false, - generics: Default::default(), inputs: vec![], output: Ty::mk_unit(), }, @@ -481,13 +481,56 @@ impl ItemTransCtx<'_, '_> { ) -> Result { let span = item_meta.span; + self.translate_def_generics(span, def)?; + let src = self.get_item_source(span, def)?; + + if let hax::FullDefKind::Ctor { + fields, output_ty, .. + } = def.kind() + { + let signature = FunSig { + inputs: fields + .iter() + .map(|field| self.translate_ty(span, &field.ty)) + .try_collect()?, + output: self.translate_ty(span, output_ty)?, + is_unsafe: false, + }; + + let body = if item_meta.opacity.with_private_contents().is_opaque() { + Body::Opaque + } else { + self.build_ctor_body(span, def)? + }; + return Ok(FunDecl { + def_id, + item_meta, + generics: self.into_generics(), + signature, + src, + is_global_initializer: None, + body, + }); + } + // Translate the function signature trace!("Translating function signature"); - let signature = self.translate_function_signature(def, &item_meta)?; + let signature = match &def.kind { + hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } => { + self.translate_fun_sig(span, &sig.value)? + } + hax::FullDefKind::Const { ty, .. } + | hax::FullDefKind::AssocConst { ty, .. } + | hax::FullDefKind::Static { ty, .. } => FunSig { + inputs: vec![], + output: self.translate_ty(span, ty)?, + is_unsafe: false, + }, + _ => panic!("Unexpected definition for function: {def:?}"), + }; // Check whether this function is a method declaration for a trait definition. // If this is the case, it shouldn't contain a body. - let src = self.get_item_source(span, def)?; let is_trait_method_decl_without_default = match &src { ItemSource::TraitDecl { has_default, .. } => !has_default, _ => false, @@ -506,24 +549,6 @@ impl ItemTransCtx<'_, '_> { Body::Opaque } else if is_trait_method_decl_without_default { Body::TraitMethodWithoutDefault - } else if let hax::FullDefKind::Ctor { - adt_def_id, - ctor_of, - variant_id, - fields, - output_ty, - .. - } = def.kind() - { - self.build_ctor_body( - span, - def, - adt_def_id, - ctor_of, - *variant_id, - fields, - output_ty, - )? } else { // Translate the MIR body for this definition. self.translate_def_body(item_meta.span, def) @@ -531,6 +556,7 @@ impl ItemTransCtx<'_, '_> { Ok(FunDecl { def_id, item_meta, + generics: self.into_generics(), signature, src, is_global_initializer, diff --git a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs index b7fd17d99..bc8147f6a 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -306,16 +306,17 @@ impl ItemTransCtx<'_, '_> { let self_ty = TyKind::TypeVar(DeBruijnVar::new_at_zero(TypeVarId::ZERO)).into_ty(); let self_ptr = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty(); - let drop_ty = Ty::new(TyKind::FnPtr(RegionBinder::empty(( - [self_ptr].into(), - Ty::mk_unit(), - )))); + let drop_ty = Ty::new(TyKind::FnPtr(RegionBinder::empty(FunSig { + is_unsafe: true, + inputs: [self_ptr].into(), + output: Ty::mk_unit(), + }))); ("drop".into(), drop_ty) } TrVTableField::Method(item_name, sig) => { // It's ok to translate the method signature in the context of the trait because // `vtable_sig: Some(_)` ensures the method has no generics of its own. - let sig = self.translate_fun_sig(span, &sig)?; + let sig = self.translate_poly_fun_sig(span, &sig)?; let ty = TyKind::FnPtr(sig).into_ty(); let field_name = format!("method_{}", item_name.0); (field_name, ty) @@ -839,7 +840,6 @@ impl ItemTransCtx<'_, '_> { // Signature: `() -> VTable`. let sig = FunSig { is_unsafe: false, - generics: self.the_only_binder().params.clone(), inputs: vec![], output: Ty::new(TyKind::Adt(vtable_struct_ref.clone())), }; @@ -861,6 +861,7 @@ impl ItemTransCtx<'_, '_> { Ok(FunDecl { def_id: init_func_id, item_meta: item_meta, + generics: self.into_generics(), signature: sig, src: ItemSource::VTableInstance { impl_ref }, is_global_initializer: Some(init_for), @@ -1020,8 +1021,7 @@ impl ItemTransCtx<'_, '_> { // `*mut dyn Trait -> ()` let signature = FunSig { - is_unsafe: false, - generics: self.the_only_binder().params.clone(), + is_unsafe: true, inputs: vec![ref_dyn_self.clone()], output: Ty::mk_unit(), }; @@ -1036,6 +1036,7 @@ impl ItemTransCtx<'_, '_> { Ok(FunDecl { def_id: fun_id, item_meta, + generics: self.into_generics(), signature, src: ItemSource::VTableMethodShim, is_global_initializer: None, @@ -1065,21 +1066,11 @@ impl ItemTransCtx<'_, '_> { ); }; - // Replace to get the true signature of the shim function. - // As `translate_function_signature` will use the `sig` field of the `hax::FullDef` - // TODO: this is a hack. - let shim_func_def = { - let mut def = impl_func_def.clone(); - let hax::FullDefKind::AssocFn { sig, .. } = &mut def.kind else { - unreachable!() - }; - *sig = vtable_sig.clone(); - def - }; - - // Compute the correct signature for the shim - let signature = self.translate_function_signature(&shim_func_def, &item_meta)?; + self.translate_def_generics(span, &impl_func_def)?; + // The signature of the shim function. + let signature = self.translate_fun_sig(span, &vtable_sig.value)?; + // The concrete receiver we will cast to. let target_receiver = self.translate_ty(span, &target_signature.value.inputs[0])?; trace!( @@ -1096,6 +1087,7 @@ impl ItemTransCtx<'_, '_> { Ok(FunDecl { def_id: fun_id, item_meta, + generics: self.into_generics(), signature, src: ItemSource::VTableMethodShim, is_global_initializer: None, diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index aef3d2fe7..14e6f47a9 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -198,7 +198,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { hax::TyKind::Arrow(sig) => { trace!("Arrow"); trace!("bound vars: {:?}", sig.bound_vars); - let sig = self.translate_fun_sig(span, sig)?; + let sig = self.translate_poly_fun_sig(span, sig)?; TyKind::FnPtr(sig) } hax::TyKind::FnDef { item, .. } => { @@ -268,19 +268,24 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { Ok(kind.into_ty()) } - pub fn translate_fun_sig( + pub fn translate_poly_fun_sig( &mut self, span: Span, sig: &hax::Binder, - ) -> Result, Ty)>, Error> { - self.translate_region_binder(span, sig, |ctx, sig| { - let inputs = sig - .inputs - .iter() - .map(|x| ctx.translate_ty(span, x)) - .try_collect()?; - let output = ctx.translate_ty(span, &sig.output)?; - Ok((inputs, output)) + ) -> Result, Error> { + self.translate_region_binder(span, sig, |ctx, sig| ctx.translate_fun_sig(span, sig)) + } + pub fn translate_fun_sig(&mut self, span: Span, sig: &hax::TyFnSig) -> Result { + let inputs = sig + .inputs + .iter() + .map(|x| self.translate_ty(span, x)) + .try_collect()?; + let output = self.translate_ty(span, &sig.output)?; + Ok(FunSig { + is_unsafe: sig.safety == hax::Safety::Unsafe, + inputs, + output, }) } diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 40cb9c277..183968051 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -542,10 +542,10 @@ impl FmtWithCtx for FunDecl { .fmt_item_intro(f, ctx, keyword, self.def_id)?; // Update the context - let ctx = &ctx.set_generics(&self.signature.generics); + let ctx = &ctx.set_generics(&self.generics); // Generic parameters - let (params, preds) = self.signature.generics.fmt_with_ctx_with_trait_clauses(ctx); + let (params, preds) = self.generics.fmt_with_ctx_with_trait_clauses(ctx); write!(f, "{params}")?; // Arguments @@ -584,33 +584,34 @@ impl FmtWithCtx for FunDeclRef { } } -impl FmtWithCtx for FunSig { +impl FmtWithCtx for RegionBinder { fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { - let ctx = &ctx.set_generics(&self.generics); + // Update the bound regions + let ctx = &ctx.push_bound_regions(&self.regions); + let FunSig { + is_unsafe, + inputs, + output, + } = &self.skip_binder; - // Unsafe keyword - if self.is_unsafe { + if *is_unsafe { write!(f, "unsafe ")?; } - // Generic parameters - let (params, clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx); - write!(f, "fn{params}")?; - - // Arguments - let args = self - .inputs - .iter() - .map(|ty| ty.with_ctx(ctx).to_string()) - .format(", "); - write!(f, "({args})")?; - - // Return type - if !self.output.is_unit() { - write!(f, " -> {}", self.output.with_ctx(ctx))?; + write!(f, "fn")?; + if !self.regions.is_empty() { + write!( + f, + "<{}>", + self.regions.iter().map(|r| r.with_ctx(ctx)).format(", ") + )?; + } + let inputs = inputs.iter().map(|x| x.with_ctx(ctx)).format(", "); + write!(f, "({inputs})")?; + if !output.is_unit() { + let output = output.with_ctx(ctx); + write!(f, " -> {output}")?; } - - write!(f, "{clauses}")?; Ok(()) } } @@ -1978,30 +1979,6 @@ impl FmtWithCtx for TraitTypeConstraint { } } -impl FmtWithCtx for RegionBinder<(Vec, Ty)> { - fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { - // Update the bound regions - let ctx = &ctx.push_bound_regions(&self.regions); - - write!(f, "fn")?; - if !self.regions.is_empty() { - write!( - f, - "<{}>", - self.regions.iter().map(|r| r.with_ctx(ctx)).format(", ") - )?; - } - let (inputs, output) = &self.skip_binder; - let inputs = inputs.iter().map(|x| x.with_ctx(ctx)).format(", "); - write!(f, "({inputs})")?; - if !output.is_unit() { - let output = output.with_ctx(ctx); - write!(f, " -> {output}")?; - } - Ok(()) - } -} - impl FmtWithCtx for Ty { fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self.kind() { diff --git a/charon/src/transform/add_missing_info/reorder_decls.rs b/charon/src/transform/add_missing_info/reorder_decls.rs index 74a9afbae..bebdd7a50 100644 --- a/charon/src/transform/add_missing_info/reorder_decls.rs +++ b/charon/src/transform/add_missing_info/reorder_decls.rs @@ -337,14 +337,24 @@ fn compute_declarations_graph<'tcx>(ctx: &'tcx TransformCtx) -> Deps { let _ = item.drive(&mut graph); } ItemRef::Fun(d) => { + let FunDecl { + def_id: _, + item_meta: _, + generics, + signature, + src, + is_global_initializer: _, + body, + } = d; // Skip `d.is_global_initializer` to avoid incorrect mutual dependencies. // TODO: add `is_global_initializer` to `ItemKind`. - let _ = d.signature.drive(&mut graph); - let _ = d.body.drive(&mut graph); + let _ = generics.drive(&mut graph); + let _ = signature.drive(&mut graph); + let _ = body.drive(&mut graph); // FIXME(#514): A method declaration depends on its declaring trait because of its // `Self` clause. While the clause is implicit, we make sure to record the // dependency manually. - if let ItemSource::TraitDecl { trait_ref, .. } = &d.src { + if let ItemSource::TraitDecl { trait_ref, .. } = src { graph.insert_edge(trait_ref.id.into()); } } diff --git a/charon/src/transform/control_flow/ullbc_to_llbc.rs b/charon/src/transform/control_flow/ullbc_to_llbc.rs index dc8403795..661bb4ecb 100644 --- a/charon/src/transform/control_flow/ullbc_to_llbc.rs +++ b/charon/src/transform/control_flow/ullbc_to_llbc.rs @@ -30,11 +30,9 @@ use std::mem; use crate::common::ensure_sufficient_stack; use crate::errors::sanity_check; -use crate::formatter::IntoFormatter; use crate::ids::IndexVec; use crate::llbc_ast as tgt; use crate::meta::{Span, combine_span}; -use crate::pretty::FmtWithCtx; use crate::transform::TransformCtx; use crate::transform::ctx::TransformPass; use crate::ullbc_ast::{self as src, BlockId}; @@ -1555,18 +1553,10 @@ impl TransformPass for Transform { translate_body(ctx, body); }); - // Print the functions - let fmt_ctx = &ctx.into_fmt(); - for fun in &ctx.translated.fun_decls { - trace!( - "# Signature:\n{}\n\n# Function definition:\n{}\n", - fun.signature.with_ctx(fmt_ctx), - fun.with_ctx(fmt_ctx), - ); - } - if ctx.options.print_built_llbc { eprintln!("# LLBC resulting from control-flow reconstruction:\n\n{ctx}\n",); + } else { + trace!("# LLBC resulting from control-flow reconstruction:\n\n{ctx}\n",); } } } diff --git a/charon/src/transform/ctx.rs b/charon/src/transform/ctx.rs index b04eb3688..3300b8066 100644 --- a/charon/src/transform/ctx.rs +++ b/charon/src/transform/ctx.rs @@ -547,7 +547,7 @@ impl FunDecl { if let Some(body) = self.body.as_unstructured_mut() { let mut ctx = UllbcStatementTransformCtx { ctx, - params: &self.signature.generics, + params: &self.generics, locals: &mut body.locals, span: self.item_meta.span, statements: Vec::new(), @@ -572,7 +572,7 @@ impl FunDecl { if let Some(body) = self.body.as_unstructured_mut() { let mut ctx = UllbcStatementTransformCtx { ctx, - params: &self.signature.generics, + params: &self.generics, locals: &mut body.locals, span: self.item_meta.span, statements: Vec::new(), @@ -610,7 +610,7 @@ impl FunDecl { locals: &mut body.locals, statements: Vec::new(), span: self.item_meta.span, - params: &self.signature.generics, + params: &self.generics, }; body.body.visit_blocks_bwd(|block: &mut llbc_ast::Block| { ctx.statements = Vec::with_capacity(block.statements.len()); diff --git a/charon/tests/ui/arrays.out b/charon/tests/ui/arrays.out index 4790b8e05..00c066748 100644 --- a/charon/tests/ui/arrays.out +++ b/charon/tests/ui/arrays.out @@ -86,7 +86,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = pub fn core::ops::index::Index::index<'_0, Self, Idx, Clause0_Output>(@1: &'_0 (Self), @2: Idx) -> &'_0 (Clause0_Output) @@ -295,7 +295,7 @@ fn UNIT_METADATA() const UNIT_METADATA: () = @Fun0() // Full name: test_crate::::{impl Destruct for Array}::drop_in_place -fn {impl Destruct for Array}::drop_in_place(@1: *mut Array) +unsafe fn {impl Destruct for Array}::drop_in_place(@1: *mut Array) where [@TraitClause0]: Sized, { diff --git a/charon/tests/ui/associated-types.out b/charon/tests/ui/associated-types.out index f193b9233..588262977 100644 --- a/charon/tests/ui/associated-types.out +++ b/charon/tests/ui/associated-types.out @@ -80,7 +80,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::option::Option diff --git a/charon/tests/ui/call-to-known-trait-method.out b/charon/tests/ui/call-to-known-trait-method.out index be62a4d27..a5f67be7f 100644 --- a/charon/tests/ui/call-to-known-trait-method.out +++ b/charon/tests/ui/call-to-known-trait-method.out @@ -97,7 +97,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: alloc::string::String diff --git a/charon/tests/ui/closure-as-fn.out b/charon/tests/ui/closure-as-fn.out index 6da7fea8b..a7f971648 100644 --- a/charon/tests/ui/closure-as-fn.out +++ b/charon/tests/ui/closure-as-fn.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -128,7 +128,7 @@ fn {impl FnMut<()> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: ()) } // Full name: test_crate::main::closure::{impl Destruct for closure}::drop_in_place -fn {impl Destruct for closure}::drop_in_place(@1: *mut closure) +unsafe fn {impl Destruct for closure}::drop_in_place(@1: *mut closure) = // Full name: test_crate::main::closure::{impl Destruct for closure} diff --git a/charon/tests/ui/closures.out b/charon/tests/ui/closures.out index 0c870d83c..efbe8021b 100644 --- a/charon/tests/ui/closures.out +++ b/charon/tests/ui/closures.out @@ -87,7 +87,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::ops::function::Fn @@ -128,7 +128,7 @@ where } // Full name: core::option::Option::{impl Destruct for Option[@TraitClause0]}::drop_in_place -fn {impl Destruct for Option[@TraitClause0]}::drop_in_place(@1: *mut Option[@TraitClause0]) +unsafe fn {impl Destruct for Option[@TraitClause0]}::drop_in_place(@1: *mut Option[@TraitClause0]) where [@TraitClause0]: Sized, = @@ -153,7 +153,7 @@ fn UNIT_METADATA() const UNIT_METADATA: () = @Fun0() // Full name: test_crate::::{impl Destruct for (A)}::drop_in_place -fn {impl Destruct for (A)}::drop_in_place(@1: *mut (A)) +unsafe fn {impl Destruct for (A)}::drop_in_place(@1: *mut (A)) { let @0: (); // return let @1: *mut (A); // arg #1 @@ -320,7 +320,7 @@ fn {impl FnMut<(u32), u32> for test_crate::test_closure_u32::closure}::call_mut< } // Full name: test_crate::test_closure_u32::closure::{impl Destruct for test_crate::test_closure_u32::closure}::drop_in_place -fn {impl Destruct for test_crate::test_closure_u32::closure}::drop_in_place(@1: *mut test_crate::test_closure_u32::closure) +unsafe fn {impl Destruct for test_crate::test_closure_u32::closure}::drop_in_place(@1: *mut test_crate::test_closure_u32::closure) = // Full name: test_crate::test_closure_u32::closure::{impl Destruct for test_crate::test_closure_u32::closure} @@ -460,7 +460,7 @@ fn {impl FnMut<(u32, u32), u32> for test_crate::test_closure_u32s::closure}::cal } // Full name: test_crate::test_closure_u32s::closure::{impl Destruct for test_crate::test_closure_u32s::closure}::drop_in_place -fn {impl Destruct for test_crate::test_closure_u32s::closure}::drop_in_place(@1: *mut test_crate::test_closure_u32s::closure) +unsafe fn {impl Destruct for test_crate::test_closure_u32s::closure}::drop_in_place(@1: *mut test_crate::test_closure_u32s::closure) = // Full name: test_crate::test_closure_u32s::closure::{impl Destruct for test_crate::test_closure_u32s::closure} @@ -591,7 +591,7 @@ fn {impl FnMut<(&'_ (u32)), &'_ (u32)> for test_crate::test_closure_ref_u32::clo } // Full name: test_crate::test_closure_ref_u32::closure::{impl Destruct for test_crate::test_closure_ref_u32::closure}::drop_in_place -fn {impl Destruct for test_crate::test_closure_ref_u32::closure}::drop_in_place(@1: *mut test_crate::test_closure_ref_u32::closure) +unsafe fn {impl Destruct for test_crate::test_closure_ref_u32::closure}::drop_in_place(@1: *mut test_crate::test_closure_ref_u32::closure) = // Full name: test_crate::test_closure_ref_u32::closure::{impl Destruct for test_crate::test_closure_ref_u32::closure} @@ -728,7 +728,7 @@ where } // Full name: test_crate::test_closure_ref_param::closure::{impl Destruct for test_crate::test_closure_ref_param::closure[@TraitClause0]}::drop_in_place -fn {impl Destruct for test_crate::test_closure_ref_param::closure[@TraitClause0]}::drop_in_place(@1: *mut test_crate::test_closure_ref_param::closure[@TraitClause0]) +unsafe fn {impl Destruct for test_crate::test_closure_ref_param::closure[@TraitClause0]}::drop_in_place(@1: *mut test_crate::test_closure_ref_param::closure[@TraitClause0]) where [@TraitClause0]: Sized, = @@ -895,7 +895,7 @@ where } // Full name: test_crate::test_closure_ref_early_bound::closure::{impl Destruct for test_crate::test_closure_ref_early_bound::closure<'_, T>[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for test_crate::test_closure_ref_early_bound::closure<'_, T>[@TraitClause0, @TraitClause1]}::drop_in_place<'a, T>(@1: *mut test_crate::test_closure_ref_early_bound::closure<'_, T>[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for test_crate::test_closure_ref_early_bound::closure<'_, T>[@TraitClause0, @TraitClause1]}::drop_in_place<'a, T>(@1: *mut test_crate::test_closure_ref_early_bound::closure<'_, T>[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Trait<'a, T>, @@ -1060,7 +1060,7 @@ fn {impl FnMut<(u32), u32> for test_crate::test_map_option2::closure}::call_mut< } // Full name: test_crate::test_map_option2::closure::{impl Destruct for test_crate::test_map_option2::closure}::drop_in_place -fn {impl Destruct for test_crate::test_map_option2::closure}::drop_in_place(@1: *mut test_crate::test_map_option2::closure) +unsafe fn {impl Destruct for test_crate::test_map_option2::closure}::drop_in_place(@1: *mut test_crate::test_map_option2::closure) = // Full name: test_crate::test_map_option2::closure::{impl Destruct for test_crate::test_map_option2::closure} @@ -1322,7 +1322,7 @@ fn {impl FnMut<(u32), u32> for test_crate::test_map_option3::closure}::call_mut< } // Full name: test_crate::test_map_option3::closure::{impl Destruct for test_crate::test_map_option3::closure}::drop_in_place -fn {impl Destruct for test_crate::test_map_option3::closure}::drop_in_place(@1: *mut test_crate::test_map_option3::closure) +unsafe fn {impl Destruct for test_crate::test_map_option3::closure}::drop_in_place(@1: *mut test_crate::test_map_option3::closure) = // Full name: test_crate::test_map_option3::closure::{impl Destruct for test_crate::test_map_option3::closure} @@ -1455,7 +1455,7 @@ fn {impl FnMut<(&'_ (&'_ (u32))), u32> for test_crate::test_regions::closure}::c } // Full name: test_crate::test_regions::closure::{impl Destruct for test_crate::test_regions::closure}::drop_in_place -fn {impl Destruct for test_crate::test_regions::closure}::drop_in_place(@1: *mut test_crate::test_regions::closure) +unsafe fn {impl Destruct for test_crate::test_regions::closure}::drop_in_place(@1: *mut test_crate::test_regions::closure) = // Full name: test_crate::test_regions::closure::{impl Destruct for test_crate::test_regions::closure} @@ -1540,7 +1540,7 @@ fn {impl FnMut<(&'_ (&'_ (u32))), u32> for test_crate::test_regions_casted::clos } // Full name: test_crate::test_regions_casted::closure::{impl Destruct for test_crate::test_regions_casted::closure}::drop_in_place -fn {impl Destruct for test_crate::test_regions_casted::closure}::drop_in_place(@1: *mut test_crate::test_regions_casted::closure) +unsafe fn {impl Destruct for test_crate::test_regions_casted::closure}::drop_in_place(@1: *mut test_crate::test_regions_casted::closure) = // Full name: test_crate::test_regions_casted::closure::{impl Destruct for test_crate::test_regions_casted::closure} @@ -1730,7 +1730,7 @@ fn {impl FnMut<(u32), u32> for test_crate::test_closure_capture::closure<'_0, '_ } // Full name: test_crate::test_closure_capture::closure::{impl Destruct for test_crate::test_closure_capture::closure<'_0, '_1>}::drop_in_place -fn {impl Destruct for test_crate::test_closure_capture::closure<'_0, '_1>}::drop_in_place<'_0, '_1>(@1: *mut test_crate::test_closure_capture::closure<'_0, '_1>) +unsafe fn {impl Destruct for test_crate::test_closure_capture::closure<'_0, '_1>}::drop_in_place<'_0, '_1>(@1: *mut test_crate::test_closure_capture::closure<'_0, '_1>) = // Full name: test_crate::test_closure_capture::closure::{impl Destruct for test_crate::test_closure_capture::closure<'_0, '_1>} @@ -1865,7 +1865,7 @@ where } // Full name: test_crate::test_closure_clone::closure::{impl Destruct for test_crate::test_closure_clone::closure[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for test_crate::test_closure_clone::closure[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut test_crate::test_closure_clone::closure[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for test_crate::test_closure_clone::closure[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut test_crate::test_closure_clone::closure[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Clone, @@ -1958,7 +1958,7 @@ fn {impl FnMut<(i32), i32> for test_crate::test_array_map::closure}::call_mut<'_ } // Full name: test_crate::test_array_map::closure::{impl Destruct for test_crate::test_array_map::closure}::drop_in_place -fn {impl Destruct for test_crate::test_array_map::closure}::drop_in_place(@1: *mut test_crate::test_array_map::closure) +unsafe fn {impl Destruct for test_crate::test_array_map::closure}::drop_in_place(@1: *mut test_crate::test_array_map::closure) = // Full name: test_crate::test_array_map::closure::{impl Destruct for test_crate::test_array_map::closure} @@ -2099,7 +2099,7 @@ fn test_fnmut_with_ref() } // Full name: test_crate::test_fnmut_with_ref::closure::{impl Destruct for test_crate::test_fnmut_with_ref::closure<'_0>}::drop_in_place -fn {impl Destruct for test_crate::test_fnmut_with_ref::closure<'_0>}::drop_in_place<'_0>(@1: *mut test_crate::test_fnmut_with_ref::closure<'_0>) +unsafe fn {impl Destruct for test_crate::test_fnmut_with_ref::closure<'_0>}::drop_in_place<'_0>(@1: *mut test_crate::test_fnmut_with_ref::closure<'_0>) = // Full name: test_crate::test_fnmut_with_ref::closure::{impl Destruct for test_crate::test_fnmut_with_ref::closure<'_0>} diff --git a/charon/tests/ui/closures_with_where.out b/charon/tests/ui/closures_with_where.out index 0b3304dbc..6eeaf4e6f 100644 --- a/charon/tests/ui/closures_with_where.out +++ b/charon/tests/ui/closures_with_where.out @@ -62,7 +62,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output @@ -128,7 +128,7 @@ where } // Full name: test_crate::test::closure::{impl Destruct for closure[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for closure[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut closure[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for closure[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut closure[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Ops, diff --git a/charon/tests/ui/comments.out b/charon/tests/ui/comments.out index e9891c340..323d2866e 100644 --- a/charon/tests/ui/comments.out +++ b/charon/tests/ui/comments.out @@ -51,7 +51,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::option::Option diff --git a/charon/tests/ui/control-flow/issue-297-cfg.out b/charon/tests/ui/control-flow/issue-297-cfg.out index 56a99e145..8709ad49e 100644 --- a/charon/tests/ui/control-flow/issue-297-cfg.out +++ b/charon/tests/ui/control-flow/issue-297-cfg.out @@ -299,7 +299,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple diff --git a/charon/tests/ui/desugar_drops_to_calls.out b/charon/tests/ui/desugar_drops_to_calls.out index a6d24b399..498f120be 100644 --- a/charon/tests/ui/desugar_drops_to_calls.out +++ b/charon/tests/ui/desugar_drops_to_calls.out @@ -28,7 +28,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::ops::drop::Drop @@ -55,7 +55,7 @@ pub fn _print<'_0>(@1: Arguments<'_0>) pub struct Global {} // Full name: alloc::alloc::Global::{impl Destruct for Global}::drop_in_place -fn {impl Destruct for Global}::drop_in_place(@1: *mut Global) +unsafe fn {impl Destruct for Global}::drop_in_place(@1: *mut Global) = // Full name: alloc::alloc::Global::{impl Destruct for Global} @@ -65,7 +65,7 @@ impl Destruct for Global { } // Full name: alloc::boxed::Box::{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place -fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]) +unsafe fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]) where [@TraitClause0]: MetaSized, [@TraitClause1]: Sized, @@ -90,7 +90,7 @@ where pub opaque type String // Full name: alloc::string::String::{impl Destruct for String}::drop_in_place -fn {impl Destruct for String}::drop_in_place(@1: *mut String) +unsafe fn {impl Destruct for String}::drop_in_place(@1: *mut String) = // Full name: alloc::string::String::{impl Destruct for String} @@ -109,7 +109,7 @@ where [@TraitClause4]: Destruct, // Full name: alloc::vec::Vec::{impl Destruct for Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place -fn {impl Destruct for Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place(@1: *mut Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]) +unsafe fn {impl Destruct for Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place(@1: *mut Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]) where [@TraitClause0]: Sized, [@TraitClause1]: Sized, @@ -230,7 +230,7 @@ pub fn {impl Drop for Point}::drop<'_0>(@1: &'_0 mut (Point)) } // Full name: test_crate::Point::{impl Destruct for Point}::drop_in_place -fn {impl Destruct for Point}::drop_in_place(@1: *mut Point) +unsafe fn {impl Destruct for Point}::drop_in_place(@1: *mut Point) { let @0: (); // return let @1: *mut Point; // arg #1 diff --git a/charon/tests/ui/dictionary_passing_style_woes.out b/charon/tests/ui/dictionary_passing_style_woes.out index de8d7c47c..d35ad1a1a 100644 --- a/charon/tests/ui/dictionary_passing_style_woes.out +++ b/charon/tests/ui/dictionary_passing_style_woes.out @@ -46,7 +46,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/dyn-with-diamond-supertraits.out b/charon/tests/ui/dyn-with-diamond-supertraits.out index 9badcb73d..6585531ca 100644 --- a/charon/tests/ui/dyn-with-diamond-supertraits.out +++ b/charon/tests/ui/dyn-with-diamond-supertraits.out @@ -49,7 +49,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = #[lang_item("add")] @@ -71,7 +71,7 @@ const UNIT_METADATA: () = @Fun0() struct test_crate::Super::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Super)), + drop: unsafe fn(*mut (dyn Super)), method_super_method: fn<'_0_1>(&'_0_1 ((dyn Super)), T) -> i32, super_trait_0: &'static (core::marker::MetaSized::{vtable}), } @@ -93,7 +93,7 @@ where struct test_crate::Internal::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Internal)), + drop: unsafe fn(*mut (dyn Internal)), method_internal_method: fn<'_0_1>(&'_0_1 ((dyn Internal))) -> Ty0, super_trait_0: &'static (core::marker::MetaSized::{vtable}), } @@ -116,7 +116,7 @@ where struct test_crate::Left::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Left)), + drop: unsafe fn(*mut (dyn Left)), method_left_method: fn<'_0_1>(&'_0_1 ((dyn Left))) -> Ty1, super_trait_0: &'static (core::marker::MetaSized::{vtable}), super_trait_1: &'static (test_crate::Internal::{vtable}), @@ -141,7 +141,7 @@ where struct test_crate::Right::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Right)), + drop: unsafe fn(*mut (dyn Right)), method_right_method: fn<'_0_1>(&'_0_1 ((dyn Right))) -> Ty1, super_trait_0: &'static (core::marker::MetaSized::{vtable}), super_trait_1: &'static (test_crate::Internal::{vtable}), @@ -169,7 +169,7 @@ where struct test_crate::Join::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Join)), + drop: unsafe fn(*mut (dyn Join)), method_join_method: fn<'_0_1>(&'_0_1 ((dyn Join))) -> (Ty3, Ty2), super_trait_0: &'static (core::marker::MetaSized::{vtable}), super_trait_1: &'static (test_crate::Left::{vtable}), @@ -212,7 +212,7 @@ fn {impl Super for i32}::super_method<'_0>(@1: &'_0 (i32), @2: i32) -> i32 } // Full name: test_crate::{impl Super for i32}::{vtable_drop_shim} -fn {impl Super for i32}::{vtable_drop_shim}(@1: *mut (dyn Super)) +unsafe fn {impl Super for i32}::{vtable_drop_shim}(@1: *mut (dyn Super)) { let ret@0: (); // return let dyn_self@1: *mut (dyn Super + '0); // arg #1 @@ -282,7 +282,7 @@ fn {impl Internal for i32}::internal_method<'_0>(@1: &'_0 (i32)) -> i32 } // Full name: test_crate::{impl Internal for i32}::{vtable_drop_shim} -fn {impl Internal for i32}::{vtable_drop_shim}(@1: *mut (dyn Internal)) +unsafe fn {impl Internal for i32}::{vtable_drop_shim}(@1: *mut (dyn Internal)) { let ret@0: (); // return let dyn_self@1: *mut (dyn Internal + '0); // arg #1 @@ -352,7 +352,7 @@ fn {impl Left for i32}::left_method<'_0>(@1: &'_0 (i32)) -> i32 } // Full name: test_crate::{impl Left for i32}::{vtable_drop_shim} -fn {impl Left for i32}::{vtable_drop_shim}(@1: *mut (dyn Left)) +unsafe fn {impl Left for i32}::{vtable_drop_shim}(@1: *mut (dyn Left)) { let ret@0: (); // return let dyn_self@1: *mut (dyn Left + '0); // arg #1 @@ -456,7 +456,7 @@ fn {impl Right for i32}::right_method<'_0>(@1: &'_0 (i32)) -> i32 } // Full name: test_crate::{impl Right for i32}::{vtable_drop_shim} -fn {impl Right for i32}::{vtable_drop_shim}(@1: *mut (dyn Right)) +unsafe fn {impl Right for i32}::{vtable_drop_shim}(@1: *mut (dyn Right)) { let ret@0: (); // return let dyn_self@1: *mut (dyn Right + '0); // arg #1 @@ -544,7 +544,7 @@ fn {impl Join for i32}::join_method<'_0>(@1: &'_0 (i32)) -> (i32, i32) } // Full name: test_crate::{impl Join for i32}::{vtable_drop_shim} -fn {impl Join for i32}::{vtable_drop_shim}(@1: *mut (dyn Join)) +unsafe fn {impl Join for i32}::{vtable_drop_shim}(@1: *mut (dyn Join)) { let ret@0: (); // return let dyn_self@1: *mut (dyn Join + '0); // arg #1 diff --git a/charon/tests/ui/explicit-drop-bounds.out b/charon/tests/ui/explicit-drop-bounds.out index 1ef27a943..3a7663b2f 100644 --- a/charon/tests/ui/explicit-drop-bounds.out +++ b/charon/tests/ui/explicit-drop-bounds.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: alloc::string::String @@ -28,7 +28,7 @@ fn core::marker::Destruct::drop_in_place(@1: *mut Self) pub opaque type String // Full name: alloc::string::String::{impl Destruct for String}::drop_in_place -fn {impl Destruct for String}::drop_in_place(@1: *mut String) +unsafe fn {impl Destruct for String}::drop_in_place(@1: *mut String) = // Full name: alloc::string::String::{impl Destruct for String} diff --git a/charon/tests/ui/external.out b/charon/tests/ui/external.out index 9646bb558..7acf81df0 100644 --- a/charon/tests/ui/external.out +++ b/charon/tests/ui/external.out @@ -81,7 +81,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = #[lang_item("mem_swap")] @@ -189,7 +189,7 @@ where [@TraitClause1]: Sized, // Full name: alloc::vec::Vec::{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut Vec[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut Vec[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Sized, diff --git a/charon/tests/ui/foreign-type-alias.out b/charon/tests/ui/foreign-type-alias.out index 4768b4b17..bf38a308c 100644 --- a/charon/tests/ui/foreign-type-alias.out +++ b/charon/tests/ui/foreign-type-alias.out @@ -52,7 +52,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: alloc::alloc::Global diff --git a/charon/tests/ui/gosim-demo.out b/charon/tests/ui/gosim-demo.out index 633794ea3..261473898 100644 --- a/charon/tests/ui/gosim-demo.out +++ b/charon/tests/ui/gosim-demo.out @@ -347,7 +347,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple diff --git a/charon/tests/ui/impl-trait.out b/charon/tests/ui/impl-trait.out index dfbf44884..3f7388518 100644 --- a/charon/tests/ui/impl-trait.out +++ b/charon/tests/ui/impl-trait.out @@ -58,7 +58,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -324,7 +324,7 @@ where } // Full name: test_crate::wrap::closure::{impl Destruct for closure[@TraitClause0]}::drop_in_place -fn {impl Destruct for closure[@TraitClause0]}::drop_in_place(@1: *mut closure[@TraitClause0]) +unsafe fn {impl Destruct for closure[@TraitClause0]}::drop_in_place(@1: *mut closure[@TraitClause0]) where [@TraitClause0]: Sized, = diff --git a/charon/tests/ui/issue-114-opaque-bodies.out b/charon/tests/ui/issue-114-opaque-bodies.out index 9eab6a76f..8db0e3af7 100644 --- a/charon/tests/ui/issue-114-opaque-bodies.out +++ b/charon/tests/ui/issue-114-opaque-bodies.out @@ -125,7 +125,7 @@ impl From for i64 { #[lang_item("phantom_data")] pub struct PhantomData {} -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::num::niche_types::UsizeNoHighBit @@ -193,7 +193,7 @@ where } // Full name: alloc::vec::Vec::{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut Vec[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut Vec[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Sized, diff --git a/charon/tests/ui/issue-118-generic-copy.out b/charon/tests/ui/issue-118-generic-copy.out index 13ad16010..bb28031bc 100644 --- a/charon/tests/ui/issue-118-generic-copy.out +++ b/charon/tests/ui/issue-118-generic-copy.out @@ -54,7 +54,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/issue-120-bare-discriminant-read.out b/charon/tests/ui/issue-120-bare-discriminant-read.out index b08c0ed44..9716209ec 100644 --- a/charon/tests/ui/issue-120-bare-discriminant-read.out +++ b/charon/tests/ui/issue-120-bare-discriminant-read.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::option::Option @@ -34,7 +34,7 @@ where } // Full name: core::option::Option::{impl Destruct for Option[@TraitClause0]}::drop_in_place -fn {impl Destruct for Option[@TraitClause0]}::drop_in_place(@1: *mut Option[@TraitClause0]) +unsafe fn {impl Destruct for Option[@TraitClause0]}::drop_in_place(@1: *mut Option[@TraitClause0]) where [@TraitClause0]: Sized, = diff --git a/charon/tests/ui/issue-165-vec-macro.out b/charon/tests/ui/issue-165-vec-macro.out index 9d0da8a77..c9e314bb1 100644 --- a/charon/tests/ui/issue-165-vec-macro.out +++ b/charon/tests/ui/issue-165-vec-macro.out @@ -50,7 +50,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::mem::SizedTypeProperties @@ -153,7 +153,7 @@ unsafe fn exchange_malloc(@1: usize, @2: usize) -> *mut u8 = // Full name: alloc::boxed::Box::{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1]) where [@TraitClause0]: MetaSized, [@TraitClause1]: Sized, @@ -185,7 +185,7 @@ where = // Full name: alloc::vec::Vec::{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut Vec[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut Vec[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Sized, diff --git a/charon/tests/ui/issue-323-closure-borrow.out b/charon/tests/ui/issue-323-closure-borrow.out index 5eb73eb46..7aa06d093 100644 --- a/charon/tests/ui/issue-323-closure-borrow.out +++ b/charon/tests/ui/issue-323-closure-borrow.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -135,7 +135,7 @@ fn {impl FnMut<()> for closure<'_0>}::call_mut<'_0, '_1>(@1: &'_1 mut (closure<' } // Full name: test_crate::new::closure::{impl Destruct for closure<'_0>}::drop_in_place -fn {impl Destruct for closure<'_0>}::drop_in_place<'_0>(@1: *mut closure<'_0>) +unsafe fn {impl Destruct for closure<'_0>}::drop_in_place<'_0>(@1: *mut closure<'_0>) = // Full name: test_crate::new::closure::{impl Destruct for closure<'_0>} diff --git a/charon/tests/ui/issue-378-ctor-as-fn.out b/charon/tests/ui/issue-378-ctor-as-fn.out index a67221455..a458b607a 100644 --- a/charon/tests/ui/issue-378-ctor-as-fn.out +++ b/charon/tests/ui/issue-378-ctor-as-fn.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::option::Option @@ -44,7 +44,7 @@ where pub opaque type String // Full name: alloc::string::String::{impl Destruct for String}::drop_in_place -fn {impl Destruct for String}::drop_in_place(@1: *mut String) +unsafe fn {impl Destruct for String}::drop_in_place(@1: *mut String) = // Full name: alloc::string::String::{impl Destruct for String} @@ -87,7 +87,7 @@ struct Foo { } // Full name: test_crate::Foo::{impl Destruct for Foo}::drop_in_place -fn {impl Destruct for Foo}::drop_in_place(@1: *mut Foo) +unsafe fn {impl Destruct for Foo}::drop_in_place(@1: *mut Foo) { let @0: (); // return let @1: *mut Foo; // arg #1 diff --git a/charon/tests/ui/issue-394-rpit-with-lifetime.out b/charon/tests/ui/issue-394-rpit-with-lifetime.out index 3945b3540..3e24fc2ae 100644 --- a/charon/tests/ui/issue-394-rpit-with-lifetime.out +++ b/charon/tests/ui/issue-394-rpit-with-lifetime.out @@ -77,7 +77,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output @@ -115,7 +115,7 @@ fn {impl FnMut<()> for closure<'_>}::call_mut<'a, '_1>(@1: &'_1 mut (closure<'_> } // Full name: test_crate::sparse_transitions::closure::{impl Destruct for closure<'_>}::drop_in_place -fn {impl Destruct for closure<'_>}::drop_in_place<'a>(@1: *mut closure<'_>) +unsafe fn {impl Destruct for closure<'_>}::drop_in_place<'a>(@1: *mut closure<'_>) = // Full name: test_crate::sparse_transitions::closure::{impl Destruct for closure<'_>} diff --git a/charon/tests/ui/issue-395-failed-to-normalize.out b/charon/tests/ui/issue-395-failed-to-normalize.out index 5fccd0ad4..499a361f9 100644 --- a/charon/tests/ui/issue-395-failed-to-normalize.out +++ b/charon/tests/ui/issue-395-failed-to-normalize.out @@ -278,7 +278,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple diff --git a/charon/tests/ui/issue-4-slice-try-into-array.out b/charon/tests/ui/issue-4-slice-try-into-array.out index e46658a11..8d9c04455 100644 --- a/charon/tests/ui/issue-4-slice-try-into-array.out +++ b/charon/tests/ui/issue-4-slice-try-into-array.out @@ -182,7 +182,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::result::{Result[@TraitClause0, @TraitClause1]}::unwrap diff --git a/charon/tests/ui/issue-4-traits.out b/charon/tests/ui/issue-4-traits.out index 5c041e7a0..417059cb0 100644 --- a/charon/tests/ui/issue-4-traits.out +++ b/charon/tests/ui/issue-4-traits.out @@ -182,7 +182,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::result::{Result[@TraitClause0, @TraitClause1]}::unwrap diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out index 94c22c8bf..d2b487581 100644 --- a/charon/tests/ui/issue-45-misc.out +++ b/charon/tests/ui/issue-45-misc.out @@ -456,7 +456,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::ops::control_flow::ControlFlow @@ -581,7 +581,7 @@ fn {impl FnMut<(i32)> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: (i } // Full name: test_crate::map::closure::{impl Destruct for closure}::drop_in_place -fn {impl Destruct for closure}::drop_in_place(@1: *mut closure) +unsafe fn {impl Destruct for closure}::drop_in_place(@1: *mut closure) = // Full name: test_crate::map::closure::{impl Destruct for closure} diff --git a/charon/tests/ui/issue-70-override-provided-method.3.out b/charon/tests/ui/issue-70-override-provided-method.3.out index 82ce54256..428000473 100644 --- a/charon/tests/ui/issue-70-override-provided-method.3.out +++ b/charon/tests/ui/issue-70-override-provided-method.3.out @@ -60,7 +60,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::option::Option diff --git a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out index 8e3828b64..31dfc6eea 100644 --- a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out +++ b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out @@ -54,7 +54,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/iterator.out b/charon/tests/ui/iterator.out index e5d8b8aee..5532e9509 100644 --- a/charon/tests/ui/iterator.out +++ b/charon/tests/ui/iterator.out @@ -27,7 +27,7 @@ pub trait Destruct } // Full name: core::array::iter::IntoIter::{impl Destruct for IntoIter[@TraitClause0]}::drop_in_place -fn {impl Destruct for IntoIter[@TraitClause0]}::drop_in_place(@1: *mut IntoIter[@TraitClause0]) +unsafe fn {impl Destruct for IntoIter[@TraitClause0]}::drop_in_place(@1: *mut IntoIter[@TraitClause0]) where [@TraitClause0]: Sized, = @@ -2517,7 +2517,7 @@ where [@TraitClause1]: TrustedRandomAccessNoCoerce, = -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = pub fn core::ops::arith::AddAssign::add_assign<'_0, Self, Rhs>(@1: &'_0 mut (Self), @2: Rhs) diff --git a/charon/tests/ui/loops.out b/charon/tests/ui/loops.out index 23c6af79d..a61934375 100644 --- a/charon/tests/ui/loops.out +++ b/charon/tests/ui/loops.out @@ -521,7 +521,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple diff --git a/charon/tests/ui/matches.out b/charon/tests/ui/matches.out index ad5707d55..a39c1b2b4 100644 --- a/charon/tests/ui/matches.out +++ b/charon/tests/ui/matches.out @@ -21,7 +21,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/method-impl-generalization.out b/charon/tests/ui/method-impl-generalization.out index 90bc8c37e..046f8f6f6 100644 --- a/charon/tests/ui/method-impl-generalization.out +++ b/charon/tests/ui/method-impl-generalization.out @@ -46,7 +46,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/ml-mono-name-matcher-tests.out b/charon/tests/ui/ml-mono-name-matcher-tests.out index b0a62f0da..f856b10a8 100644 --- a/charon/tests/ui/ml-mono-name-matcher-tests.out +++ b/charon/tests/ui/ml-mono-name-matcher-tests.out @@ -105,11 +105,11 @@ pub trait Destruct::<&'_ (Str)> } // Full name: core::marker::Destruct::drop_in_place:: -fn drop_in_place::(@1: *mut i32) +unsafe fn drop_in_place::(@1: *mut i32) = // Full name: core::marker::Destruct::drop_in_place::<&'_ (Str)> -fn drop_in_place::<&'_ (Str)>(@1: *mut &'_ (Str)) +unsafe fn drop_in_place::<&'_ (Str)>(@1: *mut &'_ (Str)) = // Full name: core::ops::range::RangeFrom:: diff --git a/charon/tests/ui/ml-name-matcher-tests.out b/charon/tests/ui/ml-name-matcher-tests.out index 5e05cb771..139b4a7e3 100644 --- a/charon/tests/ui/ml-name-matcher-tests.out +++ b/charon/tests/ui/ml-name-matcher-tests.out @@ -21,7 +21,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::ops::index::Index diff --git a/charon/tests/ui/monomorphization/closure-fn.out b/charon/tests/ui/monomorphization/closure-fn.out index 962fbae67..dff61131e 100644 --- a/charon/tests/ui/monomorphization/closure-fn.out +++ b/charon/tests/ui/monomorphization/closure-fn.out @@ -38,7 +38,7 @@ pub trait Destruct::> vtable: core::marker::Destruct::{vtable}::> } -fn core::marker::Destruct::drop_in_place::>(@1: *mut closure<'_, '_>) +unsafe fn core::marker::Destruct::drop_in_place::>(@1: *mut closure<'_, '_>) = // Full name: core::marker::Tuple::<(u8, u8)> @@ -213,7 +213,7 @@ fn apply_to_mut::><'_0>(@1: &'_0 mut (closure<'_, '_>)) -> u8 } // Full name: test_crate::main::closure::{impl Destruct::>}::drop_in_place -fn {impl Destruct::>}::drop_in_place<'_0, '_1>(@1: *mut closure<'_, '_>) +unsafe fn {impl Destruct::>}::drop_in_place<'_0, '_1>(@1: *mut closure<'_, '_>) { let @0: (); // return let @1: *mut closure<'_0, '_1>; // arg #1 diff --git a/charon/tests/ui/monomorphization/closure-fnonce.out b/charon/tests/ui/monomorphization/closure-fnonce.out index 42e4e1efc..19a8e9e63 100644 --- a/charon/tests/ui/monomorphization/closure-fnonce.out +++ b/charon/tests/ui/monomorphization/closure-fnonce.out @@ -60,10 +60,10 @@ pub trait Destruct:: vtable: core::marker::Destruct::{vtable}:: } -fn core::marker::Destruct::drop_in_place::(@1: *mut closure) +unsafe fn core::marker::Destruct::drop_in_place::(@1: *mut closure) = -fn core::marker::Destruct::drop_in_place::(@1: *mut NotCopy) +unsafe fn core::marker::Destruct::drop_in_place::(@1: *mut NotCopy) = // Full name: core::marker::Tuple::<(u8)> @@ -136,7 +136,7 @@ fn {impl FnOnce::}::call_once(@1: closure, @2: (u8)) -> u8 } // Full name: test_crate::main::closure::{impl Destruct::}::drop_in_place -fn {impl Destruct::}::drop_in_place(@1: *mut closure) +unsafe fn {impl Destruct::}::drop_in_place(@1: *mut closure) { let @0: (); // return let @1: *mut closure; // arg #1 @@ -174,7 +174,7 @@ fn apply_to_zero_once::(@1: closure) -> u8 } // Full name: test_crate::NotCopy::{impl Destruct::}::drop_in_place -fn {impl Destruct::}::drop_in_place(@1: *mut NotCopy) +unsafe fn {impl Destruct::}::drop_in_place(@1: *mut NotCopy) { let @0: (); // return let @1: *mut NotCopy; // arg #1 diff --git a/charon/tests/ui/monomorphization/closures.out b/charon/tests/ui/monomorphization/closures.out index 9c43831e9..6fd48ccea 100644 --- a/charon/tests/ui/monomorphization/closures.out +++ b/charon/tests/ui/monomorphization/closures.out @@ -107,16 +107,16 @@ pub trait Destruct:: vtable: core::marker::Destruct::{vtable}:: } -fn core::marker::Destruct::drop_in_place::>(@1: *mut test_crate::main::closure<'_>) +unsafe fn core::marker::Destruct::drop_in_place::>(@1: *mut test_crate::main::closure<'_>) = -fn core::marker::Destruct::drop_in_place::>(@1: *mut test_crate::main::closure#1<'_>) +unsafe fn core::marker::Destruct::drop_in_place::>(@1: *mut test_crate::main::closure#1<'_>) = -fn core::marker::Destruct::drop_in_place::(@1: *mut test_crate::main::closure#2) +unsafe fn core::marker::Destruct::drop_in_place::(@1: *mut test_crate::main::closure#2) = -fn core::marker::Destruct::drop_in_place::(@1: *mut Thing) +unsafe fn core::marker::Destruct::drop_in_place::(@1: *mut Thing) = // Full name: core::marker::Tuple::<(u8)> @@ -239,7 +239,7 @@ fn UNIT_METADATA() const UNIT_METADATA: () = @Fun1() // Full name: test_crate::Thing::{impl Destruct::}::drop_in_place -fn {impl Destruct::}::drop_in_place(@1: *mut Thing) +unsafe fn {impl Destruct::}::drop_in_place(@1: *mut Thing) { let @0: (); // return let @1: *mut Thing; // arg #1 @@ -283,7 +283,7 @@ fn {impl Fn::, (u8)>}::call<'_0, '_1>(@1: &'_1 (te } // Full name: test_crate::main::closure::{impl Destruct::>}::drop_in_place -fn {impl Destruct::>}::drop_in_place<'_0>(@1: *mut test_crate::main::closure<'_>) +unsafe fn {impl Destruct::>}::drop_in_place<'_0>(@1: *mut test_crate::main::closure<'_>) { let @0: (); // return let @1: *mut test_crate::main::closure<'_0>; // arg #1 @@ -350,7 +350,7 @@ fn {impl FnMut::, (u8)>}::call_mut<'_0, '_1>(@1: } // Full name: test_crate::main::closure#1::{impl Destruct::>}::drop_in_place -fn {impl Destruct::>}::drop_in_place<'_0>(@1: *mut test_crate::main::closure#1<'_>) +unsafe fn {impl Destruct::>}::drop_in_place<'_0>(@1: *mut test_crate::main::closure#1<'_>) { let @0: (); // return let @1: *mut test_crate::main::closure#1<'_0>; // arg #1 @@ -417,7 +417,7 @@ fn {impl FnOnce::}::call_once(@1: test_crate: } // Full name: test_crate::main::closure#2::{impl Destruct::}::drop_in_place -fn {impl Destruct::}::drop_in_place(@1: *mut test_crate::main::closure#2) +unsafe fn {impl Destruct::}::drop_in_place(@1: *mut test_crate::main::closure#2) { let @0: (); // return let @1: *mut test_crate::main::closure#2; // arg #1 diff --git a/charon/tests/ui/monomorphization/fndefs-casts.out b/charon/tests/ui/monomorphization/fndefs-casts.out index 71f95fb97..6d3f89e0a 100644 --- a/charon/tests/ui/monomorphization/fndefs-casts.out +++ b/charon/tests/ui/monomorphization/fndefs-casts.out @@ -80,7 +80,7 @@ pub trait Destruct:: foo::<'_0_1>> } // Full name: core::marker::Destruct::drop_in_place:: foo::<'_0_1>> -fn drop_in_place:: foo::<'_0_1>>(@1: *mut for<'_0_1> foo::<'_0_1>) +unsafe fn drop_in_place:: foo::<'_0_1>>(@1: *mut for<'_0_1> foo::<'_0_1>) = // Full name: core::marker::Tuple::<(&'_ (u32))> diff --git a/charon/tests/ui/monomorphization/issue-917-inline-const-with-poly-type.out b/charon/tests/ui/monomorphization/issue-917-inline-const-with-poly-type.out index 85ee52db1..2f0f10b34 100644 --- a/charon/tests/ui/monomorphization/issue-917-inline-const-with-poly-type.out +++ b/charon/tests/ui/monomorphization/issue-917-inline-const-with-poly-type.out @@ -47,10 +47,10 @@ pub trait Destruct::> vtable: core::marker::Destruct::{vtable}::> } -fn core::marker::Destruct::drop_in_place::>(@1: *mut closure::<()>) +unsafe fn core::marker::Destruct::drop_in_place::>(@1: *mut closure::<()>) = -fn core::marker::Destruct::drop_in_place::<()>(@1: *mut ()) +unsafe fn core::marker::Destruct::drop_in_place::<()>(@1: *mut ()) = // Full name: core::marker::Tuple::<(())> @@ -149,7 +149,7 @@ fn {impl FnMut::, (())>}::call_mut::<()><'_0>(@1: &'_0 mut (closur } // Full name: test_crate::foo::{const}::closure::{impl Destruct::>}::drop_in_place::<()> -fn {impl Destruct::>}::drop_in_place::<()>(@1: *mut closure::<()>) +unsafe fn {impl Destruct::>}::drop_in_place::<()>(@1: *mut closure::<()>) { let @0: (); // return let @1: *mut closure::<()>; // arg #1 diff --git a/charon/tests/ui/monomorphization/trait_impls.out b/charon/tests/ui/monomorphization/trait_impls.out index 4d0aedf62..b432a8946 100644 --- a/charon/tests/ui/monomorphization/trait_impls.out +++ b/charon/tests/ui/monomorphization/trait_impls.out @@ -21,7 +21,7 @@ pub trait Destruct:: } // Full name: core::marker::Destruct::drop_in_place:: -fn drop_in_place::(@1: *mut bool) +unsafe fn drop_in_place::(@1: *mut bool) = fn UNIT_METADATA() diff --git a/charon/tests/ui/monomorphization/trait_impls_ullbc.out b/charon/tests/ui/monomorphization/trait_impls_ullbc.out index a3045fb2b..4d8481cbd 100644 --- a/charon/tests/ui/monomorphization/trait_impls_ullbc.out +++ b/charon/tests/ui/monomorphization/trait_impls_ullbc.out @@ -57,7 +57,7 @@ pub trait Destruct:: } // Full name: core::marker::Destruct::drop_in_place:: -fn drop_in_place::(@1: *mut bool) +unsafe fn drop_in_place::(@1: *mut bool) = fn UNIT_METADATA() diff --git a/charon/tests/ui/monomorphize-mut-no-types.out b/charon/tests/ui/monomorphize-mut-no-types.out index 4c45e509e..19302159c 100644 --- a/charon/tests/ui/monomorphize-mut-no-types.out +++ b/charon/tests/ui/monomorphize-mut-no-types.out @@ -79,16 +79,16 @@ pub trait core::marker::Destruct::>><'_0, T0> } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = -fn core::marker::Destruct::drop_in_place::<&_ mut (_)><'_0, T0>(@1: *mut &'_0 mut (T0)) +unsafe fn core::marker::Destruct::drop_in_place::<&_ mut (_)><'_0, T0>(@1: *mut &'_0 mut (T0)) = -fn core::marker::Destruct::drop_in_place::><'_0, T0>(@1: *mut Option<&'_0 mut (T0)>) +unsafe fn core::marker::Destruct::drop_in_place::><'_0, T0>(@1: *mut Option<&'_0 mut (T0)>) = -fn core::marker::Destruct::drop_in_place::>><'_0, T0>(@1: *mut Option>) +unsafe fn core::marker::Destruct::drop_in_place::>><'_0, T0>(@1: *mut Option>) = fn UNIT_METADATA() diff --git a/charon/tests/ui/monomorphize-mut.out b/charon/tests/ui/monomorphize-mut.out index 79b0f7e96..58674c109 100644 --- a/charon/tests/ui/monomorphize-mut.out +++ b/charon/tests/ui/monomorphize-mut.out @@ -153,18 +153,18 @@ where } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = -fn core::marker::Destruct::drop_in_place::<&_ mut (_)><'_0, T0>(@1: *mut &'_0 mut (T0)) +unsafe fn core::marker::Destruct::drop_in_place::<&_ mut (_)><'_0, T0>(@1: *mut &'_0 mut (T0)) = -fn core::marker::Destruct::drop_in_place::<_, _>[@TraitClause0]><'_0, T0>(@1: *mut core::option::Option::<&_ mut (_)><'_0, T0>[@TraitClause0]) +unsafe fn core::marker::Destruct::drop_in_place::<_, _>[@TraitClause0]><'_0, T0>(@1: *mut core::option::Option::<&_ mut (_)><'_0, T0>[@TraitClause0]) where [@TraitClause0]: core::marker::Sized::<&_ mut (_)><'_0, T0>, = -fn core::marker::Destruct::drop_in_place::<_, _>[@TraitClause1]><_, _>[@TraitClause0, @TraitClause1]><'_0, T0>(@1: *mut core::option::Option::<_, _>[@TraitClause1]><'_0, T0>[@TraitClause0, @TraitClause1]) +unsafe fn core::marker::Destruct::drop_in_place::<_, _>[@TraitClause1]><_, _>[@TraitClause0, @TraitClause1]><'_0, T0>(@1: *mut core::option::Option::<_, _>[@TraitClause1]><'_0, T0>[@TraitClause0, @TraitClause1]) where [@TraitClause0]: core::marker::Sized::<_, _>[@TraitClause0]><'_0, T0>[@TraitClause1], [@TraitClause1]: core::marker::Sized::<&_ mut (_)><'_0, T0>, diff --git a/charon/tests/ui/no_nested_borrows.out b/charon/tests/ui/no_nested_borrows.out index 757a71824..e22efda69 100644 --- a/charon/tests/ui/no_nested_borrows.out +++ b/charon/tests/ui/no_nested_borrows.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::ops::deref::Deref @@ -59,7 +59,7 @@ where pub struct Global {} // Full name: alloc::boxed::Box::{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1]) where [@TraitClause0]: MetaSized, [@TraitClause1]: Sized, @@ -142,7 +142,7 @@ where } // Full name: test_crate::List::{impl Destruct for List[@TraitClause0]}::drop_in_place -fn {impl Destruct for List[@TraitClause0]}::drop_in_place(@1: *mut List[@TraitClause0]) +unsafe fn {impl Destruct for List[@TraitClause0]}::drop_in_place(@1: *mut List[@TraitClause0]) where [@TraitClause0]: Sized, = @@ -257,7 +257,7 @@ where } // Full name: test_crate::IdType::{impl Destruct for IdType[@TraitClause0]}::drop_in_place -fn {impl Destruct for IdType[@TraitClause0]}::drop_in_place(@1: *mut IdType[@TraitClause0]) +unsafe fn {impl Destruct for IdType[@TraitClause0]}::drop_in_place(@1: *mut IdType[@TraitClause0]) where [@TraitClause0]: Sized, = diff --git a/charon/tests/ui/predicates-on-late-bound-vars.out b/charon/tests/ui/predicates-on-late-bound-vars.out index 2055a5874..c757f7cbe 100644 --- a/charon/tests/ui/predicates-on-late-bound-vars.out +++ b/charon/tests/ui/predicates-on-late-bound-vars.out @@ -75,7 +75,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::option::Option @@ -89,7 +89,7 @@ where } // Full name: core::result::Result::{impl Destruct for Result[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for Result[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut Result[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for Result[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut Result[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Sized, diff --git a/charon/tests/ui/ptr_no_provenance.out b/charon/tests/ui/ptr_no_provenance.out index eeda94180..bfedffb63 100644 --- a/charon/tests/ui/ptr_no_provenance.out +++ b/charon/tests/ui/ptr_no_provenance.out @@ -258,7 +258,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::ptr::metadata::Pointee diff --git a/charon/tests/ui/quantified-clause.out b/charon/tests/ui/quantified-clause.out index 73ff4b7ff..f1df170d3 100644 --- a/charon/tests/ui/quantified-clause.out +++ b/charon/tests/ui/quantified-clause.out @@ -278,7 +278,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple diff --git a/charon/tests/ui/raw-boxes.out b/charon/tests/ui/raw-boxes.out index f8b4aee3a..46343df66 100644 --- a/charon/tests/ui/raw-boxes.out +++ b/charon/tests/ui/raw-boxes.out @@ -211,7 +211,7 @@ pub struct PhantomData {} // Full name: core::fmt::rt::ArgumentType enum ArgumentType<'a> { - Placeholder(value: NonNull<()>, formatter: fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut (Formatter<'_1_1>)) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], _lifetime: PhantomData<&'a (())>), + Placeholder(value: NonNull<()>, formatter: unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut (Formatter<'_1_1>)) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], _lifetime: PhantomData<&'a (())>), Count(u16), } @@ -1699,7 +1699,7 @@ where return } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::num::niche_types::NonZeroUsizeInner @@ -3268,7 +3268,7 @@ where } // Full name: alloc::boxed::Box::{impl Destruct for Box[@TraitClause0, @TraitClause1, @TraitClause2]}::drop_in_place -fn {impl Destruct for Box[@TraitClause0, @TraitClause1, @TraitClause2]}::drop_in_place(@1: *mut Box[@TraitClause0, @TraitClause1, @TraitClause2]) +unsafe fn {impl Destruct for Box[@TraitClause0, @TraitClause1, @TraitClause2]}::drop_in_place(@1: *mut Box[@TraitClause0, @TraitClause1, @TraitClause2]) where [@TraitClause0]: MetaSized, [@TraitClause1]: Sized, diff --git a/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out b/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out index 351c40eb9..f55c5a508 100644 --- a/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out +++ b/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -169,7 +169,7 @@ where } // Full name: test_crate::{SqrtTables[@TraitClause0]}::sqrt_common::closure::{impl Destruct for closure[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for closure[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut closure[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for closure[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut closure[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: PrimeField, diff --git a/charon/tests/ui/result-unwrap.out b/charon/tests/ui/result-unwrap.out index 4001e8337..2510ed6fb 100644 --- a/charon/tests/ui/result-unwrap.out +++ b/charon/tests/ui/result-unwrap.out @@ -60,7 +60,7 @@ where struct core::fmt::Debug::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Debug)), + drop: unsafe fn(*mut (dyn Debug)), method_fmt: fn<'_0_1, '_1_1, '_2_1>(&'_0_1 ((dyn Debug)), &'_1_1 mut (Formatter<'_2_1>)) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], } @@ -203,7 +203,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/rust-name-matcher-tests.out b/charon/tests/ui/rust-name-matcher-tests.out index 435a47c80..d764e0fb4 100644 --- a/charon/tests/ui/rust-name-matcher-tests.out +++ b/charon/tests/ui/rust-name-matcher-tests.out @@ -21,7 +21,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::option::Option diff --git a/charon/tests/ui/rvalues.out b/charon/tests/ui/rvalues.out index 3b048a163..27065c2ec 100644 --- a/charon/tests/ui/rvalues.out +++ b/charon/tests/ui/rvalues.out @@ -29,7 +29,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -220,7 +220,7 @@ unsafe fn exchange_malloc(@1: usize, @2: usize) -> *mut u8 = // Full name: alloc::boxed::Box::{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1]) where [@TraitClause0]: MetaSized, [@TraitClause1]: Sized, @@ -451,7 +451,7 @@ fn {impl FnMut<(u8)> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: (u8 } // Full name: test_crate::fn_casts::closure::{impl Destruct for closure}::drop_in_place -fn {impl Destruct for closure}::drop_in_place(@1: *mut closure) +unsafe fn {impl Destruct for closure}::drop_in_place(@1: *mut closure) = // Full name: test_crate::fn_casts::closure::{impl Destruct for closure} @@ -498,11 +498,11 @@ fn fn_casts() { let @0: (); // return let @1: fn(); // anonymous local - let @2: fn(); // anonymous local + let @2: unsafe fn(); // anonymous local let closure@3: closure; // local let @4: fn(u8); // anonymous local let @5: closure; // anonymous local - let @6: fn(u8); // anonymous local + let @6: unsafe fn(u8); // anonymous local let @7: closure; // anonymous local @0 := () @@ -510,7 +510,7 @@ fn fn_casts() @1 := cast(const (test_crate::fn_casts::foo)) storage_dead(@1) storage_live(@2) - @2 := cast(const (bar)) + @2 := cast(const (bar)) storage_dead(@2) storage_live(closure@3) closure@3 := closure { } @@ -523,7 +523,7 @@ fn fn_casts() storage_live(@6) storage_live(@7) @7 := copy (closure@3) - @6 := cast(const (as_fn)) + @6 := cast(const (as_fn)) storage_dead(@7) storage_dead(@6) @0 := () diff --git a/charon/tests/ui/send_bound.out b/charon/tests/ui/send_bound.out index 9c013e8e7..07f1b2aaf 100644 --- a/charon/tests/ui/send_bound.out +++ b/charon/tests/ui/send_bound.out @@ -25,7 +25,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/simple-cmp.out b/charon/tests/ui/simple-cmp.out index 35e484f1d..ad6b0c57e 100644 --- a/charon/tests/ui/simple-cmp.out +++ b/charon/tests/ui/simple-cmp.out @@ -150,7 +150,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/simple/additions.out b/charon/tests/ui/simple/additions.out index 08c5aa37f..2caf01636 100644 --- a/charon/tests/ui/simple/additions.out +++ b/charon/tests/ui/simple/additions.out @@ -121,7 +121,7 @@ impl Copy for u8 { } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = pub fn core::num::{u8}::saturating_add(@1: u8, @2: u8) -> u8 diff --git a/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.out b/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.out index ca2c353f0..b95e54a4f 100644 --- a/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.out +++ b/charon/tests/ui/simple/assoc-constraint-on-assoc-ty.out @@ -21,7 +21,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/simple/box-into-inner.out b/charon/tests/ui/simple/box-into-inner.out index 62fc4db68..ec9c45c37 100644 --- a/charon/tests/ui/simple/box-into-inner.out +++ b/charon/tests/ui/simple/box-into-inner.out @@ -24,7 +24,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::mem::SizedTypeProperties @@ -165,7 +165,7 @@ where pub opaque type String // Full name: alloc::string::String::{impl Destruct for String}::drop_in_place -fn {impl Destruct for String}::drop_in_place(@1: *mut String) +unsafe fn {impl Destruct for String}::drop_in_place(@1: *mut String) = // Full name: alloc::string::String::{impl Destruct for String} diff --git a/charon/tests/ui/simple/box-new.out b/charon/tests/ui/simple/box-new.out index 6f1805ab6..0483c6dad 100644 --- a/charon/tests/ui/simple/box-new.out +++ b/charon/tests/ui/simple/box-new.out @@ -61,7 +61,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: alloc::alloc::Global @@ -93,7 +93,7 @@ where [@TraitClause2]: Allocator, // Full name: alloc::boxed::Box::{impl Destruct for Box[@TraitClause0, @TraitClause1, @TraitClause2]}::drop_in_place -fn {impl Destruct for Box[@TraitClause0, @TraitClause1, @TraitClause2]}::drop_in_place(@1: *mut Box[@TraitClause0, @TraitClause1, @TraitClause2]) +unsafe fn {impl Destruct for Box[@TraitClause0, @TraitClause1, @TraitClause2]}::drop_in_place(@1: *mut Box[@TraitClause0, @TraitClause1, @TraitClause2]) where [@TraitClause0]: MetaSized, [@TraitClause1]: Sized, diff --git a/charon/tests/ui/simple/builtin-drop-mono.out b/charon/tests/ui/simple/builtin-drop-mono.out index 90a5f6cc3..9098b4e8d 100644 --- a/charon/tests/ui/simple/builtin-drop-mono.out +++ b/charon/tests/ui/simple/builtin-drop-mono.out @@ -79,7 +79,7 @@ fn UNIT_METADATA() const UNIT_METADATA: () = @Fun0() // Full name: alloc::string::String::{impl Destruct::}::drop_in_place -fn {impl Destruct::}::drop_in_place(@1: *mut String) +unsafe fn {impl Destruct::}::drop_in_place(@1: *mut String) = // Full name: alloc::string::String::{impl Destruct::} @@ -89,7 +89,7 @@ impl Destruct:: { } // Full name: test_crate::::{impl Destruct::>}::drop_in_place:: -fn {impl Destruct::>}::drop_in_place::(@1: *mut Slice) +unsafe fn {impl Destruct::>}::drop_in_place::(@1: *mut Slice) { let @0: (); // return let @1: *mut Slice; // arg #1 @@ -135,7 +135,7 @@ impl Destruct::> { } // Full name: alloc::alloc::Global::{impl Destruct::}::drop_in_place -fn {impl Destruct::}::drop_in_place(@1: *mut Global) +unsafe fn {impl Destruct::}::drop_in_place(@1: *mut Global) = // Full name: alloc::alloc::Global::{impl Destruct::} @@ -160,26 +160,26 @@ pub trait Destruct::<(String, String)> vtable: core::marker::Destruct::{vtable}::<(String, String)> } -fn core::marker::Destruct::drop_in_place::(@1: *mut Global) +unsafe fn core::marker::Destruct::drop_in_place::(@1: *mut Global) = -fn core::marker::Destruct::drop_in_place::>[{built_in impl MetaSized::>}, {built_in impl Sized::}, {impl Destruct::>}::, {impl Destruct::}]>(@1: *mut alloc::boxed::Box>[{built_in impl MetaSized::>}, {built_in impl Sized::}, {impl Destruct::>}::, {impl Destruct::}]) +unsafe fn core::marker::Destruct::drop_in_place::>[{built_in impl MetaSized::>}, {built_in impl Sized::}, {impl Destruct::>}::, {impl Destruct::}]>(@1: *mut alloc::boxed::Box>[{built_in impl MetaSized::>}, {built_in impl Sized::}, {impl Destruct::>}::, {impl Destruct::}]) = -fn core::marker::Destruct::drop_in_place::(@1: *mut String) +unsafe fn core::marker::Destruct::drop_in_place::(@1: *mut String) = -fn core::marker::Destruct::drop_in_place::>(@1: *mut Array) +unsafe fn core::marker::Destruct::drop_in_place::>(@1: *mut Array) = -fn core::marker::Destruct::drop_in_place::>(@1: *mut Slice) +unsafe fn core::marker::Destruct::drop_in_place::>(@1: *mut Slice) = -fn core::marker::Destruct::drop_in_place::<(String, String)>(@1: *mut (String, String)) +unsafe fn core::marker::Destruct::drop_in_place::<(String, String)>(@1: *mut (String, String)) = // Full name: alloc::boxed::Box::{impl Destruct::>[{built_in impl MetaSized::>}, {built_in impl Sized::}, {impl Destruct::>}::, {impl Destruct::}]>}::drop_in_place::, Global> -fn {impl Destruct::>[{built_in impl MetaSized::>}, {built_in impl Sized::}, {impl Destruct::>}::, {impl Destruct::}]>}::drop_in_place::, Global>(@1: *mut alloc::boxed::Box>[{built_in impl MetaSized::>}, {built_in impl Sized::}, {impl Destruct::>}::, {impl Destruct::}]) +unsafe fn {impl Destruct::>[{built_in impl MetaSized::>}, {built_in impl Sized::}, {impl Destruct::>}::, {impl Destruct::}]>}::drop_in_place::, Global>(@1: *mut alloc::boxed::Box>[{built_in impl MetaSized::>}, {built_in impl Sized::}, {impl Destruct::>}::, {impl Destruct::}]) = // Full name: alloc::boxed::Box::{impl Destruct::>[{built_in impl MetaSized::>}, {built_in impl Sized::}, {impl Destruct::>}::, {impl Destruct::}]>}::, Global> @@ -189,7 +189,7 @@ impl Destruct::>[{built_in impl MetaSized::::{impl Destruct::>}::drop_in_place:: -fn {impl Destruct::>}::drop_in_place::(@1: *mut Array) +unsafe fn {impl Destruct::>}::drop_in_place::(@1: *mut Array) { let @0: (); // return let @1: *mut Array; // arg #1 @@ -241,7 +241,7 @@ impl Destruct::> { } // Full name: test_crate::::{impl Destruct::<(String, String)>}::drop_in_place:: -fn {impl Destruct::<(String, String)>}::drop_in_place::(@1: *mut (String, String)) +unsafe fn {impl Destruct::<(String, String)>}::drop_in_place::(@1: *mut (String, String)) { let @0: (); // return let @1: *mut (String, String); // arg #1 diff --git a/charon/tests/ui/simple/builtin-drop.out b/charon/tests/ui/simple/builtin-drop.out index e28186a2f..e4eecf5bb 100644 --- a/charon/tests/ui/simple/builtin-drop.out +++ b/charon/tests/ui/simple/builtin-drop.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: alloc::alloc::Global @@ -28,7 +28,7 @@ fn core::marker::Destruct::drop_in_place(@1: *mut Self) pub struct Global {} // Full name: alloc::alloc::Global::{impl Destruct for Global}::drop_in_place -fn {impl Destruct for Global}::drop_in_place(@1: *mut Global) +unsafe fn {impl Destruct for Global}::drop_in_place(@1: *mut Global) = // Full name: alloc::alloc::Global::{impl Destruct for Global} @@ -38,7 +38,7 @@ impl Destruct for Global { } // Full name: alloc::boxed::Box::{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place -fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]) +unsafe fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]) where [@TraitClause0]: MetaSized, [@TraitClause1]: Sized, @@ -63,7 +63,7 @@ where pub opaque type String // Full name: alloc::string::String::{impl Destruct for String}::drop_in_place -fn {impl Destruct for String}::drop_in_place(@1: *mut String) +unsafe fn {impl Destruct for String}::drop_in_place(@1: *mut String) = // Full name: alloc::string::String::{impl Destruct for String} @@ -83,7 +83,7 @@ fn UNIT_METADATA() const UNIT_METADATA: () = @Fun0() // Full name: test_crate::::{impl Destruct for Array}::drop_in_place -fn {impl Destruct for Array}::drop_in_place(@1: *mut Array) +unsafe fn {impl Destruct for Array}::drop_in_place(@1: *mut Array) where [@TraitClause0]: Sized, [@TraitClause1]: Destruct, @@ -142,7 +142,7 @@ where } // Full name: test_crate::::{impl Destruct for Slice}::drop_in_place -fn {impl Destruct for Slice}::drop_in_place(@1: *mut Slice) +unsafe fn {impl Destruct for Slice}::drop_in_place(@1: *mut Slice) where [@TraitClause0]: Sized, [@TraitClause1]: Destruct, @@ -195,7 +195,7 @@ where } // Full name: test_crate::::{impl Destruct for (A, B)}::drop_in_place -fn {impl Destruct for (A, B)}::drop_in_place(@1: *mut (A, B)) +unsafe fn {impl Destruct for (A, B)}::drop_in_place(@1: *mut (A, B)) where [@TraitClause0]: Sized, [@TraitClause1]: Destruct, diff --git a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out index e9294f38d..a75e788ec 100644 --- a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out +++ b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = fn UNIT_METADATA() @@ -57,7 +57,7 @@ where } // Full name: test_crate::HashMap::{impl Destruct for HashMap[@TraitClause0]}::drop_in_place -fn {impl Destruct for HashMap[@TraitClause0]}::drop_in_place(@1: *mut HashMap[@TraitClause0]) +unsafe fn {impl Destruct for HashMap[@TraitClause0]}::drop_in_place(@1: *mut HashMap[@TraitClause0]) where [@TraitClause0]: Sized, = diff --git a/charon/tests/ui/simple/call-method-via-supertrait-bound.out b/charon/tests/ui/simple/call-method-via-supertrait-bound.out index ed519235f..435d35bdc 100644 --- a/charon/tests/ui/simple/call-method-via-supertrait-bound.out +++ b/charon/tests/ui/simple/call-method-via-supertrait-bound.out @@ -21,7 +21,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/simple/catch-unwind.out b/charon/tests/ui/simple/catch-unwind.out index d12f7f204..c91e234c1 100644 --- a/charon/tests/ui/simple/catch-unwind.out +++ b/charon/tests/ui/simple/catch-unwind.out @@ -47,7 +47,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -92,7 +92,7 @@ where } // Full name: core::result::Result::{impl Destruct for Result[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for Result[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut Result[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for Result[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut Result[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Sized, diff --git a/charon/tests/ui/simple/closure-capture-ref-by-move.out b/charon/tests/ui/simple/closure-capture-ref-by-move.out index 5b8e18ace..e4704b0f6 100644 --- a/charon/tests/ui/simple/closure-capture-ref-by-move.out +++ b/charon/tests/ui/simple/closure-capture-ref-by-move.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -132,7 +132,7 @@ fn foo() } // Full name: test_crate::foo::closure::{impl Destruct for closure<'_0>}::drop_in_place -fn {impl Destruct for closure<'_0>}::drop_in_place<'_0>(@1: *mut closure<'_0>) +unsafe fn {impl Destruct for closure<'_0>}::drop_in_place<'_0>(@1: *mut closure<'_0>) = // Full name: test_crate::foo::closure::{impl Destruct for closure<'_0>} diff --git a/charon/tests/ui/simple/closure-fn.out b/charon/tests/ui/simple/closure-fn.out index 995389554..27da16ae7 100644 --- a/charon/tests/ui/simple/closure-fn.out +++ b/charon/tests/ui/simple/closure-fn.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -231,7 +231,7 @@ fn {impl FnMut<(u8, u8)> for closure<'_0, '_1>}::call_mut<'_0, '_1, '_2>(@1: &'_ } // Full name: test_crate::main::closure::{impl Destruct for closure<'_0, '_1>}::drop_in_place -fn {impl Destruct for closure<'_0, '_1>}::drop_in_place<'_0, '_1>(@1: *mut closure<'_0, '_1>) +unsafe fn {impl Destruct for closure<'_0, '_1>}::drop_in_place<'_0, '_1>(@1: *mut closure<'_0, '_1>) = // Full name: test_crate::main::closure::{impl Destruct for closure<'_0, '_1>} diff --git a/charon/tests/ui/simple/closure-fnmut.out b/charon/tests/ui/simple/closure-fnmut.out index bf2842a2c..11591fb69 100644 --- a/charon/tests/ui/simple/closure-fnmut.out +++ b/charon/tests/ui/simple/closure-fnmut.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -134,7 +134,7 @@ fn {impl FnMut<(u8)> for closure<'_0>}::call_mut<'_0, '_1>(@1: &'_1 mut (closure } // Full name: test_crate::main::closure::{impl Destruct for closure<'_0>}::drop_in_place -fn {impl Destruct for closure<'_0>}::drop_in_place<'_0>(@1: *mut closure<'_0>) +unsafe fn {impl Destruct for closure<'_0>}::drop_in_place<'_0>(@1: *mut closure<'_0>) = // Full name: test_crate::main::closure::{impl Destruct for closure<'_0>} diff --git a/charon/tests/ui/simple/closure-fnonce.out b/charon/tests/ui/simple/closure-fnonce.out index 5d8cadbc1..f3371ba5e 100644 --- a/charon/tests/ui/simple/closure-fnonce.out +++ b/charon/tests/ui/simple/closure-fnonce.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -94,7 +94,7 @@ where struct NotCopy {} // Full name: test_crate::NotCopy::{impl Destruct for NotCopy}::drop_in_place -fn {impl Destruct for NotCopy}::drop_in_place(@1: *mut NotCopy) +unsafe fn {impl Destruct for NotCopy}::drop_in_place(@1: *mut NotCopy) { let @0: (); // return let @1: *mut NotCopy; // arg #1 diff --git a/charon/tests/ui/simple/closure-inside-impl.out b/charon/tests/ui/simple/closure-inside-impl.out index 7cf203b1d..6208f8bc3 100644 --- a/charon/tests/ui/simple/closure-inside-impl.out +++ b/charon/tests/ui/simple/closure-inside-impl.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -162,7 +162,7 @@ where } // Full name: test_crate::{Foo[@TraitClause0]}::method::closure::{impl Destruct for closure[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for closure[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut closure[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for closure[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut closure[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Sized, diff --git a/charon/tests/ui/simple/closure-inside-inline-const.out b/charon/tests/ui/simple/closure-inside-inline-const.out index d6bf5d024..212eb2477 100644 --- a/charon/tests/ui/simple/closure-inside-inline-const.out +++ b/charon/tests/ui/simple/closure-inside-inline-const.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -154,7 +154,7 @@ where } // Full name: test_crate::foo::{const}::closure::{impl Destruct for closure[@TraitClause0]}::drop_in_place -fn {impl Destruct for closure[@TraitClause0]}::drop_in_place(@1: *mut closure[@TraitClause0]) +unsafe fn {impl Destruct for closure[@TraitClause0]}::drop_in_place(@1: *mut closure[@TraitClause0]) where [@TraitClause0]: Sized, = diff --git a/charon/tests/ui/simple/closure-uses-ambient-self-clause.out b/charon/tests/ui/simple/closure-uses-ambient-self-clause.out index a07fb44b5..e5fb8b522 100644 --- a/charon/tests/ui/simple/closure-uses-ambient-self-clause.out +++ b/charon/tests/ui/simple/closure-uses-ambient-self-clause.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -104,7 +104,7 @@ trait Thing } // Full name: test_crate::::{impl Destruct for (A)}::drop_in_place -fn {impl Destruct for (A)}::drop_in_place(@1: *mut (A)) +unsafe fn {impl Destruct for (A)}::drop_in_place(@1: *mut (A)) { let @0: (); // return let @1: *mut (A); // arg #1 @@ -201,7 +201,7 @@ where } // Full name: test_crate::Thing::foo::closure::{impl Destruct for closure[@TraitClause0]}::drop_in_place -fn {impl Destruct for closure[@TraitClause0]}::drop_in_place(@1: *mut closure[@TraitClause0]) +unsafe fn {impl Destruct for closure[@TraitClause0]}::drop_in_place(@1: *mut closure[@TraitClause0]) where [@TraitClause0]: Thing, = diff --git a/charon/tests/ui/simple/closure-with-drops.out b/charon/tests/ui/simple/closure-with-drops.out index 8064eee29..1d672c24d 100644 --- a/charon/tests/ui/simple/closure-with-drops.out +++ b/charon/tests/ui/simple/closure-with-drops.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -118,7 +118,7 @@ where } // Full name: test_crate::foo::closure::{impl Destruct for test_crate::foo::closure[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for test_crate::foo::closure[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut test_crate::foo::closure[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for test_crate::foo::closure[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut test_crate::foo::closure[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Destruct, @@ -217,7 +217,7 @@ fn bar() } // Full name: test_crate::bar::closure::{impl Destruct for test_crate::bar::closure}::drop_in_place -fn {impl Destruct for test_crate::bar::closure}::drop_in_place(@1: *mut test_crate::bar::closure) +unsafe fn {impl Destruct for test_crate::bar::closure}::drop_in_place(@1: *mut test_crate::bar::closure) { let @0: (); // return let @1: *mut test_crate::bar::closure; // arg #1 diff --git a/charon/tests/ui/simple/conditional-drop.out b/charon/tests/ui/simple/conditional-drop.out index 73ad19791..b62d1aa9f 100644 --- a/charon/tests/ui/simple/conditional-drop.out +++ b/charon/tests/ui/simple/conditional-drop.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: alloc::alloc::Global @@ -28,7 +28,7 @@ fn core::marker::Destruct::drop_in_place(@1: *mut Self) pub struct Global {} // Full name: alloc::alloc::Global::{impl Destruct for Global}::drop_in_place -fn {impl Destruct for Global}::drop_in_place(@1: *mut Global) +unsafe fn {impl Destruct for Global}::drop_in_place(@1: *mut Global) = // Full name: alloc::alloc::Global::{impl Destruct for Global} @@ -38,7 +38,7 @@ impl Destruct for Global { } // Full name: alloc::boxed::Box::{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place -fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]) +unsafe fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]) where [@TraitClause0]: MetaSized, [@TraitClause1]: Sized, diff --git a/charon/tests/ui/simple/drop-cow.out b/charon/tests/ui/simple/drop-cow.out index 50984bfd1..534878bd8 100644 --- a/charon/tests/ui/simple/drop-cow.out +++ b/charon/tests/ui/simple/drop-cow.out @@ -38,7 +38,7 @@ pub trait Sized non-dyn-compatible } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: alloc::borrow::ToOwned @@ -86,7 +86,7 @@ where } // Full name: test_crate::Cow::{impl Destruct for Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]}::drop_in_place -fn {impl Destruct for Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]}::drop_in_place<'a, B>(@1: *mut Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]) +unsafe fn {impl Destruct for Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]}::drop_in_place<'a, B>(@1: *mut Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]) where [@TraitClause0]: MetaSized, [@TraitClause1]: ToOwned, diff --git a/charon/tests/ui/simple/drop-glue-with-const-generic-silenced.out b/charon/tests/ui/simple/drop-glue-with-const-generic-silenced.out index dea42175d..42d278042 100644 --- a/charon/tests/ui/simple/drop-glue-with-const-generic-silenced.out +++ b/charon/tests/ui/simple/drop-glue-with-const-generic-silenced.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: alloc::alloc::Global @@ -28,7 +28,7 @@ fn core::marker::Destruct::drop_in_place(@1: *mut Self) pub struct Global {} // Full name: alloc::alloc::Global::{impl Destruct for Global}::drop_in_place -fn {impl Destruct for Global}::drop_in_place(@1: *mut Global) +unsafe fn {impl Destruct for Global}::drop_in_place(@1: *mut Global) = // Full name: alloc::alloc::Global::{impl Destruct for Global} @@ -57,7 +57,7 @@ struct PortableHash { } // Full name: test_crate::PortableHash::{impl Destruct for PortableHash}::drop_in_place -fn {impl Destruct for PortableHash}::drop_in_place(@1: *mut PortableHash) +unsafe fn {impl Destruct for PortableHash}::drop_in_place(@1: *mut PortableHash) = // Full name: test_crate::PortableHash::{impl Destruct for PortableHash} diff --git a/charon/tests/ui/simple/drop-string.out b/charon/tests/ui/simple/drop-string.out index c2f5103cc..5be205364 100644 --- a/charon/tests/ui/simple/drop-string.out +++ b/charon/tests/ui/simple/drop-string.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: alloc::alloc::Global @@ -28,7 +28,7 @@ fn core::marker::Destruct::drop_in_place(@1: *mut Self) pub struct Global {} // Full name: alloc::alloc::Global::{impl Destruct for Global}::drop_in_place -fn {impl Destruct for Global}::drop_in_place(@1: *mut Global) +unsafe fn {impl Destruct for Global}::drop_in_place(@1: *mut Global) = // Full name: alloc::alloc::Global::{impl Destruct for Global} @@ -63,7 +63,7 @@ fn UNIT_METADATA() const UNIT_METADATA: () = @Fun0() // Full name: alloc::vec::Vec::{impl Destruct for Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place -fn {impl Destruct for Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place(@1: *mut Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]) +unsafe fn {impl Destruct for Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place(@1: *mut Vec[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]) where [@TraitClause0]: Sized, [@TraitClause1]: Sized, @@ -84,7 +84,7 @@ where } // Full name: alloc::string::String::{impl Destruct for String}::drop_in_place -fn {impl Destruct for String}::drop_in_place(@1: *mut String) +unsafe fn {impl Destruct for String}::drop_in_place(@1: *mut String) { let @0: (); // return let @1: *mut String; // arg #1 diff --git a/charon/tests/ui/simple/dyn-cast-to-supertrait.out b/charon/tests/ui/simple/dyn-cast-to-supertrait.out index 4d03acc4c..88f00539f 100644 --- a/charon/tests/ui/simple/dyn-cast-to-supertrait.out +++ b/charon/tests/ui/simple/dyn-cast-to-supertrait.out @@ -14,7 +14,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = fn UNIT_METADATA() @@ -30,7 +30,7 @@ const UNIT_METADATA: () = @Fun0() struct test_crate::Feline::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Feline)), + drop: unsafe fn(*mut (dyn Feline)), method_hunt: fn<'_0_1>(&'_0_1 ((dyn Feline))), super_trait_0: &'static (core::marker::MetaSized::{vtable}), } @@ -51,7 +51,7 @@ where struct test_crate::Pettable::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Pettable)), + drop: unsafe fn(*mut (dyn Pettable)), method_pet: fn<'_0_1>(&'_0_1 ((dyn Pettable))), super_trait_0: &'static (core::marker::MetaSized::{vtable}), } @@ -72,7 +72,7 @@ where struct test_crate::Cat::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Cat)), + drop: unsafe fn(*mut (dyn Cat)), method_meow: fn<'_0_1>(&'_0_1 ((dyn Cat))), super_trait_0: &'static (core::marker::MetaSized::{vtable}), super_trait_1: &'static (test_crate::Feline::{vtable}), @@ -98,7 +98,7 @@ where struct HouseCat {} // Full name: test_crate::HouseCat::{impl Destruct for HouseCat}::drop_in_place -fn {impl Destruct for HouseCat}::drop_in_place(@1: *mut HouseCat) +unsafe fn {impl Destruct for HouseCat}::drop_in_place(@1: *mut HouseCat) { let @0: (); // return let @1: *mut HouseCat; // arg #1 @@ -128,7 +128,7 @@ fn {impl Feline for HouseCat}::hunt<'_0>(@1: &'_0 (HouseCat)) } // Full name: test_crate::{impl Feline for HouseCat}::{vtable_drop_shim} -fn {impl Feline for HouseCat}::{vtable_drop_shim}(@1: *mut (dyn Feline)) +unsafe fn {impl Feline for HouseCat}::{vtable_drop_shim}(@1: *mut (dyn Feline)) { let ret@0: (); // return let dyn_self@1: *mut (dyn Feline + '0); // arg #1 @@ -192,7 +192,7 @@ fn {impl Pettable for HouseCat}::pet<'_0>(@1: &'_0 (HouseCat)) } // Full name: test_crate::{impl Pettable for HouseCat}::{vtable_drop_shim} -fn {impl Pettable for HouseCat}::{vtable_drop_shim}(@1: *mut (dyn Pettable)) +unsafe fn {impl Pettable for HouseCat}::{vtable_drop_shim}(@1: *mut (dyn Pettable)) { let ret@0: (); // return let dyn_self@1: *mut (dyn Pettable + '0); // arg #1 @@ -256,7 +256,7 @@ fn {impl Cat for HouseCat}::meow<'_0>(@1: &'_0 (HouseCat)) } // Full name: test_crate::{impl Cat for HouseCat}::{vtable_drop_shim} -fn {impl Cat for HouseCat}::{vtable_drop_shim}(@1: *mut (dyn Cat)) +unsafe fn {impl Cat for HouseCat}::{vtable_drop_shim}(@1: *mut (dyn Cat)) { let ret@0: (); // return let dyn_self@1: *mut (dyn Cat + '0); // arg #1 diff --git a/charon/tests/ui/simple/dyn-fn.out b/charon/tests/ui/simple/dyn-fn.out index e05bdf19e..8e019ef8d 100644 --- a/charon/tests/ui/simple/dyn-fn.out +++ b/charon/tests/ui/simple/dyn-fn.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -174,7 +174,7 @@ fn {impl FnMut<(&'_ mut (u32))> for closure}::call_mut<'_0, '_1>(@1: &'_1 mut (c } // Full name: test_crate::gives_fn::closure::{impl Destruct for closure}::drop_in_place -fn {impl Destruct for closure}::drop_in_place(@1: *mut closure) +unsafe fn {impl Destruct for closure}::drop_in_place(@1: *mut closure) = // Full name: test_crate::gives_fn::closure::{impl Destruct for closure} diff --git a/charon/tests/ui/simple/dyn-method-with-early-bound-lifetimes.out b/charon/tests/ui/simple/dyn-method-with-early-bound-lifetimes.out index 79d21cced..4c0df0a3b 100644 --- a/charon/tests/ui/simple/dyn-method-with-early-bound-lifetimes.out +++ b/charon/tests/ui/simple/dyn-method-with-early-bound-lifetimes.out @@ -19,7 +19,7 @@ const UNIT_METADATA: () = @Fun0() struct test_crate::Trait::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Trait)), + drop: unsafe fn(*mut (dyn Trait)), method_foo: fn<'_0_1>(&'_0_1 ((dyn Trait))), super_trait_0: &'static (core::marker::MetaSized::{vtable}), } diff --git a/charon/tests/ui/simple/fewer-clauses-in-method-impl.out b/charon/tests/ui/simple/fewer-clauses-in-method-impl.out index 38bee7b10..cd7ae1208 100644 --- a/charon/tests/ui/simple/fewer-clauses-in-method-impl.out +++ b/charon/tests/ui/simple/fewer-clauses-in-method-impl.out @@ -46,7 +46,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/simple/foreign-inline-const.out b/charon/tests/ui/simple/foreign-inline-const.out index fe554afe6..f8ba7d8f8 100644 --- a/charon/tests/ui/simple/foreign-inline-const.out +++ b/charon/tests/ui/simple/foreign-inline-const.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -154,7 +154,7 @@ where } // Full name: closure_inside_inline_const::foo::{const}::closure::{impl Destruct for closure[@TraitClause0]}::drop_in_place -fn {impl Destruct for closure[@TraitClause0]}::drop_in_place(@1: *mut closure[@TraitClause0]) +unsafe fn {impl Destruct for closure[@TraitClause0]}::drop_in_place(@1: *mut closure[@TraitClause0]) where [@TraitClause0]: Sized, = diff --git a/charon/tests/ui/simple/gat-complex-lifetimes.out b/charon/tests/ui/simple/gat-complex-lifetimes.out index 63e0b477a..8d87d5dd5 100644 --- a/charon/tests/ui/simple/gat-complex-lifetimes.out +++ b/charon/tests/ui/simple/gat-complex-lifetimes.out @@ -21,7 +21,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/simple/gat-implied-clause.out b/charon/tests/ui/simple/gat-implied-clause.out index 0f6eb2373..3c4e691c9 100644 --- a/charon/tests/ui/simple/gat-implied-clause.out +++ b/charon/tests/ui/simple/gat-implied-clause.out @@ -37,7 +37,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/simple/hello-world.out b/charon/tests/ui/simple/hello-world.out index 4c725d2c5..224e6284b 100644 --- a/charon/tests/ui/simple/hello-world.out +++ b/charon/tests/ui/simple/hello-world.out @@ -71,11 +71,11 @@ pub trait Destruct:: vtable: core::marker::Destruct::{vtable}:: } -fn core::marker::Destruct::drop_in_place::(@1: *mut String) +unsafe fn core::marker::Destruct::drop_in_place::(@1: *mut String) = // Full name: alloc::string::String::{impl Destruct::}::drop_in_place -fn {impl Destruct::}::drop_in_place(@1: *mut String) +unsafe fn {impl Destruct::}::drop_in_place(@1: *mut String) = // Full name: alloc::string::String::{impl Destruct::} diff --git a/charon/tests/ui/simple/hide-drops.out b/charon/tests/ui/simple/hide-drops.out index 90ad17fe4..cb3a9ca2b 100644 --- a/charon/tests/ui/simple/hide-drops.out +++ b/charon/tests/ui/simple/hide-drops.out @@ -8,7 +8,7 @@ pub trait Destruct vtable: {vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: alloc::string::String @@ -16,7 +16,7 @@ fn core::marker::Destruct::drop_in_place(@1: *mut Self) pub opaque type String // Full name: alloc::string::String::{impl Destruct for String}::drop_in_place -fn {impl Destruct for String}::drop_in_place(@1: *mut String) +unsafe fn {impl Destruct for String}::drop_in_place(@1: *mut String) = // Full name: alloc::string::String::{impl Destruct for String} diff --git a/charon/tests/ui/simple/impl-with-dyn-assoc-ty.out b/charon/tests/ui/simple/impl-with-dyn-assoc-ty.out index 8d593bfc8..fdf84be09 100644 --- a/charon/tests/ui/simple/impl-with-dyn-assoc-ty.out +++ b/charon/tests/ui/simple/impl-with-dyn-assoc-ty.out @@ -27,7 +27,7 @@ const UNIT_METADATA: () = @Fun0() struct test_crate::DynableTrait::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn DynableTrait)), + drop: unsafe fn(*mut (dyn DynableTrait)), super_trait_0: &'static (core::marker::MetaSized::{vtable}), } diff --git a/charon/tests/ui/simple/lending-iterator-gat.out b/charon/tests/ui/simple/lending-iterator-gat.out index 1541190b6..c4d83689b 100644 --- a/charon/tests/ui/simple/lending-iterator-gat.out +++ b/charon/tests/ui/simple/lending-iterator-gat.out @@ -24,7 +24,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -81,7 +81,7 @@ where } // Full name: core::option::Option::{impl Destruct for Option[@TraitClause0]}::drop_in_place -fn {impl Destruct for Option[@TraitClause0]}::drop_in_place(@1: *mut Option[@TraitClause0]) +unsafe fn {impl Destruct for Option[@TraitClause0]}::drop_in_place(@1: *mut Option[@TraitClause0]) where [@TraitClause0]: Sized, = @@ -125,7 +125,7 @@ pub trait LendingIterator } // Full name: test_crate::::{impl Destruct for (A)}::drop_in_place -fn {impl Destruct for (A)}::drop_in_place(@1: *mut (A)) +unsafe fn {impl Destruct for (A)}::drop_in_place(@1: *mut (A)) { let @0: (); // return let @1: *mut (A); // arg #1 @@ -288,7 +288,7 @@ fn {impl FnMut<(&'_ (i32))> for closure<'_0>}::call_mut<'_0, '_1, '_2>(@1: &'_2 } // Full name: test_crate::main::closure::{impl Destruct for closure<'_0>}::drop_in_place -fn {impl Destruct for closure<'_0>}::drop_in_place<'_0>(@1: *mut closure<'_0>) +unsafe fn {impl Destruct for closure<'_0>}::drop_in_place<'_0>(@1: *mut closure<'_0>) = // Full name: test_crate::main::closure::{impl Destruct for closure<'_0>} diff --git a/charon/tests/ui/simple/lifetime-unification-from-trait-impl.out b/charon/tests/ui/simple/lifetime-unification-from-trait-impl.out index 7023fcc44..10038ef34 100644 --- a/charon/tests/ui/simple/lifetime-unification-from-trait-impl.out +++ b/charon/tests/ui/simple/lifetime-unification-from-trait-impl.out @@ -21,7 +21,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::ptr::const_ptr::{*const T}::cast diff --git a/charon/tests/ui/simple/manual-drop-impl.out b/charon/tests/ui/simple/manual-drop-impl.out index ed8226973..616911f7d 100644 --- a/charon/tests/ui/simple/manual-drop-impl.out +++ b/charon/tests/ui/simple/manual-drop-impl.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::ops::drop::Drop @@ -67,7 +67,7 @@ where } // Full name: test_crate::Foo::{impl Destruct for Foo[@TraitClause0]}::drop_in_place -fn {impl Destruct for Foo[@TraitClause0]}::drop_in_place(@1: *mut Foo[@TraitClause0]) +unsafe fn {impl Destruct for Foo[@TraitClause0]}::drop_in_place(@1: *mut Foo[@TraitClause0]) where [@TraitClause0]: Sized, = diff --git a/charon/tests/ui/simple/mem-discriminant-from-derive.out b/charon/tests/ui/simple/mem-discriminant-from-derive.out index e533a91b3..020a88908 100644 --- a/charon/tests/ui/simple/mem-discriminant-from-derive.out +++ b/charon/tests/ui/simple/mem-discriminant-from-derive.out @@ -203,7 +203,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/simple/method-with-assoc-type-constraint.out b/charon/tests/ui/simple/method-with-assoc-type-constraint.out index be3e05726..9d0250e00 100644 --- a/charon/tests/ui/simple/method-with-assoc-type-constraint.out +++ b/charon/tests/ui/simple/method-with-assoc-type-constraint.out @@ -21,7 +21,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/simple/nested-closure-trait-ref.out b/charon/tests/ui/simple/nested-closure-trait-ref.out index 8f449b441..268324efd 100644 --- a/charon/tests/ui/simple/nested-closure-trait-ref.out +++ b/charon/tests/ui/simple/nested-closure-trait-ref.out @@ -36,7 +36,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -126,7 +126,7 @@ where } // Full name: test_crate::foo::closure::{impl Destruct for test_crate::foo::closure[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for test_crate::foo::closure[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut test_crate::foo::closure[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for test_crate::foo::closure[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut test_crate::foo::closure[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Clone, @@ -235,7 +235,7 @@ where } // Full name: test_crate::foo::closure::closure::{impl Destruct for test_crate::foo::closure::closure[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for test_crate::foo::closure::closure[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut test_crate::foo::closure::closure[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for test_crate::foo::closure::closure[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut test_crate::foo::closure::closure[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Clone, diff --git a/charon/tests/ui/simple/nested-closure.out b/charon/tests/ui/simple/nested-closure.out index 09702fd0c..978bf2d78 100644 --- a/charon/tests/ui/simple/nested-closure.out +++ b/charon/tests/ui/simple/nested-closure.out @@ -36,7 +36,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -307,7 +307,7 @@ where } // Full name: test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::{impl Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]}::drop_in_place<'a, '_1, T>(@1: *mut test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]}::drop_in_place<'a, '_1, T>(@1: *mut test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Clone, @@ -402,7 +402,7 @@ where } // Full name: test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure::{impl Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]}::drop_in_place<'a, '_1, T>(@1: *mut test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]}::drop_in_place<'a, '_1, T>(@1: *mut test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Clone, @@ -497,7 +497,7 @@ where } // Full name: test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure::closure::{impl Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]}::drop_in_place<'a, '_1, T>(@1: *mut test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]}::drop_in_place<'a, '_1, T>(@1: *mut test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Clone, diff --git a/charon/tests/ui/simple/non-lifetime-gats.out b/charon/tests/ui/simple/non-lifetime-gats.out index f374b1c17..13f88c568 100644 --- a/charon/tests/ui/simple/non-lifetime-gats.out +++ b/charon/tests/ui/simple/non-lifetime-gats.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::ops::deref::Deref @@ -44,7 +44,7 @@ where pub struct Global {} // Full name: alloc::boxed::Box::{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1]) where [@TraitClause0]: MetaSized, [@TraitClause1]: Sized, diff --git a/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out index 550e1f240..65c946d81 100644 --- a/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out +++ b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out @@ -21,7 +21,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple diff --git a/charon/tests/ui/simple/pointee_metadata.out b/charon/tests/ui/simple/pointee_metadata.out index eaa892cb3..b6825dc7f 100644 --- a/charon/tests/ui/simple/pointee_metadata.out +++ b/charon/tests/ui/simple/pointee_metadata.out @@ -201,7 +201,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::ptr::metadata::Pointee diff --git a/charon/tests/ui/simple/promoted-closure-no-warns.out b/charon/tests/ui/simple/promoted-closure-no-warns.out index 9c4584b4a..e0d199f9e 100644 --- a/charon/tests/ui/simple/promoted-closure-no-warns.out +++ b/charon/tests/ui/simple/promoted-closure-no-warns.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -151,7 +151,7 @@ fn {impl FnMut<(u32)> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: (u } // Full name: test_crate::foo::closure::{impl Destruct for closure}::drop_in_place -fn {impl Destruct for closure}::drop_in_place(@1: *mut closure) +unsafe fn {impl Destruct for closure}::drop_in_place(@1: *mut closure) = // Full name: test_crate::foo::closure::{impl Destruct for closure} diff --git a/charon/tests/ui/simple/promoted-closure.out b/charon/tests/ui/simple/promoted-closure.out index 9c4584b4a..e0d199f9e 100644 --- a/charon/tests/ui/simple/promoted-closure.out +++ b/charon/tests/ui/simple/promoted-closure.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -151,7 +151,7 @@ fn {impl FnMut<(u32)> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: (u } // Full name: test_crate::foo::closure::{impl Destruct for closure}::drop_in_place -fn {impl Destruct for closure}::drop_in_place(@1: *mut closure) +unsafe fn {impl Destruct for closure}::drop_in_place(@1: *mut closure) = // Full name: test_crate::foo::closure::{impl Destruct for closure} diff --git a/charon/tests/ui/simple/promoted_in_closure.out b/charon/tests/ui/simple/promoted_in_closure.out index d8bb2f478..3ad992792 100644 --- a/charon/tests/ui/simple/promoted_in_closure.out +++ b/charon/tests/ui/simple/promoted_in_closure.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -151,7 +151,7 @@ fn {impl FnMut<()> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: ()) } // Full name: test_crate::main::closure::{impl Destruct for closure}::drop_in_place -fn {impl Destruct for closure}::drop_in_place(@1: *mut closure) +unsafe fn {impl Destruct for closure}::drop_in_place(@1: *mut closure) = // Full name: test_crate::main::closure::{impl Destruct for closure} diff --git a/charon/tests/ui/simple/ptr-from-raw-parts.out b/charon/tests/ui/simple/ptr-from-raw-parts.out index 183d2e2ec..a542bb2b8 100644 --- a/charon/tests/ui/simple/ptr-from-raw-parts.out +++ b/charon/tests/ui/simple/ptr-from-raw-parts.out @@ -258,7 +258,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::ptr::metadata::from_raw_parts diff --git a/charon/tests/ui/simple/ptr_metadata.out b/charon/tests/ui/simple/ptr_metadata.out index f7f17006a..29e1a2f75 100644 --- a/charon/tests/ui/simple/ptr_metadata.out +++ b/charon/tests/ui/simple/ptr_metadata.out @@ -258,7 +258,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::ptr::metadata::Pointee diff --git a/charon/tests/ui/simple/slice_index_range.out b/charon/tests/ui/simple/slice_index_range.out index 1a8a010c9..82ac7b8fa 100644 --- a/charon/tests/ui/simple/slice_index_range.out +++ b/charon/tests/ui/simple/slice_index_range.out @@ -38,7 +38,7 @@ pub struct PhantomData {} // Full name: core::fmt::rt::ArgumentType enum ArgumentType<'a> { - Placeholder(value: NonNull<()>, formatter: fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut (Formatter<'_1_1>)) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], _lifetime: PhantomData<&'a (())>), + Placeholder(value: NonNull<()>, formatter: unsafe fn<'_0_1, '_1_1>(NonNull<()>, &'_0_1 mut (Formatter<'_1_1>)) -> Result<(), Error>[{built_in impl Sized for ()}, {built_in impl Sized for Error}], _lifetime: PhantomData<&'a (())>), Count(u16), } diff --git a/charon/tests/ui/simple/struct-with-drops.out b/charon/tests/ui/simple/struct-with-drops.out index ce2378e8f..ca6ddf5dc 100644 --- a/charon/tests/ui/simple/struct-with-drops.out +++ b/charon/tests/ui/simple/struct-with-drops.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::ops::drop::Drop @@ -43,7 +43,7 @@ where pub struct Global {} // Full name: alloc::alloc::Global::{impl Destruct for Global}::drop_in_place -fn {impl Destruct for Global}::drop_in_place(@1: *mut Global) +unsafe fn {impl Destruct for Global}::drop_in_place(@1: *mut Global) = // Full name: alloc::alloc::Global::{impl Destruct for Global} @@ -53,7 +53,7 @@ impl Destruct for Global { } // Full name: alloc::boxed::Box::{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place -fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]) +unsafe fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]) where [@TraitClause0]: MetaSized, [@TraitClause1]: Sized, @@ -107,7 +107,7 @@ pub fn {impl Drop for B}::drop<'_0>(@1: &'_0 mut (B)) } // Full name: test_crate::B::{impl Destruct for B}::drop_in_place -fn {impl Destruct for B}::drop_in_place(@1: *mut B) +unsafe fn {impl Destruct for B}::drop_in_place(@1: *mut B) { let @0: (); // return let @1: *mut B; // arg #1 @@ -134,7 +134,7 @@ impl Destruct for B { } // Full name: test_crate::A::{impl Destruct for A}::drop_in_place -fn {impl Destruct for A}::drop_in_place(@1: *mut A) +unsafe fn {impl Destruct for A}::drop_in_place(@1: *mut A) { let @0: (); // return let @1: *mut A; // arg #1 diff --git a/charon/tests/ui/simple/trait-alias.out b/charon/tests/ui/simple/trait-alias.out index 588be3541..f81ed2ce1 100644 --- a/charon/tests/ui/simple/trait-alias.out +++ b/charon/tests/ui/simple/trait-alias.out @@ -36,7 +36,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::option::Option diff --git a/charon/tests/ui/simple/trivial_generic_function.out b/charon/tests/ui/simple/trivial_generic_function.out index a927365f8..b2a74e23a 100644 --- a/charon/tests/ui/simple/trivial_generic_function.out +++ b/charon/tests/ui/simple/trivial_generic_function.out @@ -21,7 +21,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() diff --git a/charon/tests/ui/simple/vec-push.out b/charon/tests/ui/simple/vec-push.out index 49f97fd0e..3a48ffc6d 100644 --- a/charon/tests/ui/simple/vec-push.out +++ b/charon/tests/ui/simple/vec-push.out @@ -25,7 +25,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::mem::SizedTypeProperties diff --git a/charon/tests/ui/simple/vec-with-capacity.out b/charon/tests/ui/simple/vec-with-capacity.out index 07addd999..e557565f5 100644 --- a/charon/tests/ui/simple/vec-with-capacity.out +++ b/charon/tests/ui/simple/vec-with-capacity.out @@ -28,7 +28,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::mem::SizedTypeProperties @@ -154,7 +154,7 @@ where } // Full name: alloc::vec::Vec::{impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut Vec[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for Vec[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut Vec[@TraitClause0, @TraitClause1]) where [@TraitClause0]: Sized, [@TraitClause1]: Sized, diff --git a/charon/tests/ui/start_from.out b/charon/tests/ui/start_from.out index 5c14352fb..5ebef17f3 100644 --- a/charon/tests/ui/start_from.out +++ b/charon/tests/ui/start_from.out @@ -66,7 +66,7 @@ where = // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::num::{u32}::wrapping_add diff --git a/charon/tests/ui/string-literal.out b/charon/tests/ui/string-literal.out index 1cce424f2..87f13e94c 100644 --- a/charon/tests/ui/string-literal.out +++ b/charon/tests/ui/string-literal.out @@ -57,7 +57,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: alloc::string::String @@ -65,7 +65,7 @@ fn core::marker::Destruct::drop_in_place(@1: *mut Self) pub opaque type String // Full name: alloc::string::String::{impl Destruct for String}::drop_in_place -fn {impl Destruct for String}::drop_in_place(@1: *mut String) +unsafe fn {impl Destruct for String}::drop_in_place(@1: *mut String) = // Full name: alloc::string::String::{impl Destruct for String} diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out index d9a7a69aa..4f659eb8e 100644 --- a/charon/tests/ui/traits.out +++ b/charon/tests/ui/traits.out @@ -20,7 +20,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple @@ -94,7 +94,7 @@ where } // Full name: core::option::Option::{impl Destruct for Option[@TraitClause0]}::drop_in_place -fn {impl Destruct for Option[@TraitClause0]}::drop_in_place(@1: *mut Option[@TraitClause0]) +unsafe fn {impl Destruct for Option[@TraitClause0]}::drop_in_place(@1: *mut Option[@TraitClause0]) where [@TraitClause0]: Sized, = @@ -143,7 +143,7 @@ pub trait BoolTrait } // Full name: test_crate::::{impl Destruct for (A, B)}::drop_in_place -fn {impl Destruct for (A, B)}::drop_in_place(@1: *mut (A, B)) +unsafe fn {impl Destruct for (A, B)}::drop_in_place(@1: *mut (A, B)) where [@TraitClause0]: Sized, { @@ -462,7 +462,7 @@ where } // Full name: test_crate::Wrapper::{impl Destruct for Wrapper[@TraitClause0]}::drop_in_place -fn {impl Destruct for Wrapper[@TraitClause0]}::drop_in_place(@1: *mut Wrapper[@TraitClause0]) +unsafe fn {impl Destruct for Wrapper[@TraitClause0]}::drop_in_place(@1: *mut Wrapper[@TraitClause0]) where [@TraitClause0]: Sized, = diff --git a/charon/tests/ui/type_alias.out b/charon/tests/ui/type_alias.out index 16ef0510b..1f4e690c5 100644 --- a/charon/tests/ui/type_alias.out +++ b/charon/tests/ui/type_alias.out @@ -52,7 +52,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: alloc::alloc::Global diff --git a/charon/tests/ui/type_inference_is_order_dependent.out b/charon/tests/ui/type_inference_is_order_dependent.out index 6ebcaa83f..9dbc2510d 100644 --- a/charon/tests/ui/type_inference_is_order_dependent.out +++ b/charon/tests/ui/type_inference_is_order_dependent.out @@ -103,7 +103,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: std::io::stdio::_print diff --git a/charon/tests/ui/ullbc-control-flow.out b/charon/tests/ui/ullbc-control-flow.out index 27e6a4936..7095366e8 100644 --- a/charon/tests/ui/ullbc-control-flow.out +++ b/charon/tests/ui/ullbc-control-flow.out @@ -466,7 +466,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple diff --git a/charon/tests/ui/unsafe.out b/charon/tests/ui/unsafe.out index 46e148e99..64d648339 100644 --- a/charon/tests/ui/unsafe.out +++ b/charon/tests/ui/unsafe.out @@ -261,7 +261,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::ptr::const_ptr::{*const T}::read diff --git a/charon/tests/ui/unsize.out b/charon/tests/ui/unsize.out index dd14e74b2..4c9be6678 100644 --- a/charon/tests/ui/unsize.out +++ b/charon/tests/ui/unsize.out @@ -64,7 +64,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: alloc::alloc::Global @@ -72,7 +72,7 @@ fn core::marker::Destruct::drop_in_place(@1: *mut Self) pub struct Global {} // Full name: alloc::boxed::Box::{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1]) where [@TraitClause0]: MetaSized, [@TraitClause1]: Sized, @@ -96,7 +96,7 @@ where [@TraitClause1]: Sized, // Full name: alloc::rc::Rc::{impl Destruct for Rc[@TraitClause0, @TraitClause1]}::drop_in_place -fn {impl Destruct for Rc[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut Rc[@TraitClause0, @TraitClause1]) +unsafe fn {impl Destruct for Rc[@TraitClause0, @TraitClause1]}::drop_in_place(@1: *mut Rc[@TraitClause0, @TraitClause1]) where [@TraitClause0]: MetaSized, [@TraitClause1]: Sized, @@ -122,7 +122,7 @@ where pub opaque type String // Full name: alloc::string::String::{impl Destruct for String}::drop_in_place -fn {impl Destruct for String}::drop_in_place(@1: *mut String) +unsafe fn {impl Destruct for String}::drop_in_place(@1: *mut String) = // Full name: alloc::string::String::{impl Destruct for String} diff --git a/charon/tests/ui/unsupported/issue-79-bound-regions.out b/charon/tests/ui/unsupported/issue-79-bound-regions.out index cfc7d75de..b47eb9195 100644 --- a/charon/tests/ui/unsupported/issue-79-bound-regions.out +++ b/charon/tests/ui/unsupported/issue-79-bound-regions.out @@ -277,7 +277,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = // Full name: core::marker::Tuple diff --git a/charon/tests/ui/vtable-simple.out b/charon/tests/ui/vtable-simple.out index 13b8b9e07..da6c820f9 100644 --- a/charon/tests/ui/vtable-simple.out +++ b/charon/tests/ui/vtable-simple.out @@ -49,7 +49,7 @@ pub trait Destruct } // Full name: core::marker::Destruct::drop_in_place -fn drop_in_place(@1: *mut Self) +unsafe fn drop_in_place(@1: *mut Self) = fn UNIT_METADATA() @@ -65,7 +65,7 @@ const UNIT_METADATA: () = @Fun0() struct test_crate::Modifiable::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Modifiable)), + drop: unsafe fn(*mut (dyn Modifiable)), method_modify: fn<'_0_1, '_1_1>(&'_0_1 mut ((dyn Modifiable)), &'_1_1 (T)) -> T, super_trait_0: &'static (core::marker::MetaSized::{vtable}), } @@ -107,7 +107,7 @@ where } // Full name: test_crate::{impl Modifiable for i32}::{vtable_drop_shim} -fn {vtable_drop_shim}(@1: *mut (dyn Modifiable)) +unsafe fn {vtable_drop_shim}(@1: *mut (dyn Modifiable)) where [@TraitClause0]: Sized, [@TraitClause1]: Clone, diff --git a/charon/tests/ui/vtable_drop.out b/charon/tests/ui/vtable_drop.out index d4456d046..a63d33d15 100644 --- a/charon/tests/ui/vtable_drop.out +++ b/charon/tests/ui/vtable_drop.out @@ -52,7 +52,7 @@ impl Clone for i32 { non-dyn-compatible } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::ptr::non_null::NonNull @@ -71,7 +71,7 @@ where pub struct Global {} // Full name: alloc::alloc::Global::{impl Destruct for Global}::drop_in_place -fn {impl Destruct for Global}::drop_in_place(@1: *mut Global) +unsafe fn {impl Destruct for Global}::drop_in_place(@1: *mut Global) = // Full name: alloc::alloc::Global::{impl Destruct for Global} @@ -81,7 +81,7 @@ impl Destruct for Global { } // Full name: alloc::boxed::Box::{impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place -fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]) +unsafe fn {impl Destruct for alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]}::drop_in_place(@1: *mut alloc::boxed::Box[@TraitClause0, @TraitClause1, @TraitClause3, @TraitClause4]) where [@TraitClause0]: MetaSized, [@TraitClause1]: Sized, @@ -114,7 +114,7 @@ const UNIT_METADATA: () = @Fun0() struct test_crate::Modifiable::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Modifiable)), + drop: unsafe fn(*mut (dyn Modifiable)), method_modify: fn<'_0_1, '_1_1>(&'_0_1 mut ((dyn Modifiable)), &'_1_1 (T)) -> T, super_trait_0: &'static (core::marker::MetaSized::{vtable}), super_trait_1: &'static (core::marker::Destruct::{vtable}), @@ -179,7 +179,7 @@ where } // Full name: test_crate::{impl Modifiable for alloc::boxed::Box[{built_in impl MetaSized for i32}, {built_in impl Sized for Global}, {built_in impl Destruct for i32}, {impl Destruct for Global}]}::{vtable_drop_shim} -fn {vtable_drop_shim}(@1: *mut (dyn Modifiable)) +unsafe fn {vtable_drop_shim}(@1: *mut (dyn Modifiable)) where [@TraitClause0]: Sized, [@TraitClause1]: Clone, diff --git a/charon/tests/ui/vtables.out b/charon/tests/ui/vtables.out index 87d6d7272..df049b5d3 100644 --- a/charon/tests/ui/vtables.out +++ b/charon/tests/ui/vtables.out @@ -89,7 +89,7 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } -fn core::marker::Destruct::drop_in_place(@1: *mut Self) +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) = // Full name: core::option::Option @@ -114,7 +114,7 @@ pub enum AssertKind { pub opaque type String // Full name: alloc::string::String::{impl Destruct for String}::drop_in_place -fn {impl Destruct for String}::drop_in_place(@1: *mut String) +unsafe fn {impl Destruct for String}::drop_in_place(@1: *mut String) = // Full name: alloc::string::String::{impl Destruct for String} @@ -184,7 +184,7 @@ const UNIT_METADATA: () = @Fun0() struct test_crate::Super::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Super)), + drop: unsafe fn(*mut (dyn Super)), method_super_method: fn<'_0_1>(&'_0_1 ((dyn Super)), T) -> i32, super_trait_0: &'static (core::marker::MetaSized::{vtable}), } @@ -206,7 +206,7 @@ where struct test_crate::Checkable::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Checkable)), + drop: unsafe fn(*mut (dyn Checkable)), method_check: fn<'_0_1>(&'_0_1 ((dyn Checkable))) -> bool, super_trait_0: &'static (core::marker::MetaSized::{vtable}), super_trait_1: &'static (test_crate::Super::{vtable}), @@ -250,7 +250,7 @@ fn {impl Super for i32}::super_method<'_0>(@1: &'_0 (i32), @2: i32) -> i32 } // Full name: test_crate::{impl Super for i32}::{vtable_drop_shim} -fn {impl Super for i32}::{vtable_drop_shim}(@1: *mut (dyn Super)) +unsafe fn {impl Super for i32}::{vtable_drop_shim}(@1: *mut (dyn Super)) { let ret@0: (); // return let dyn_self@1: *mut (dyn Super + '0); // arg #1 @@ -321,7 +321,7 @@ fn {impl Checkable for i32}::check<'_0>(@1: &'_0 (i32)) -> bool } // Full name: test_crate::{impl Checkable for i32}::{vtable_drop_shim} -fn {impl Checkable for i32}::{vtable_drop_shim}(@1: *mut (dyn Checkable)) +unsafe fn {impl Checkable for i32}::{vtable_drop_shim}(@1: *mut (dyn Checkable)) { let ret@0: (); // return let dyn_self@1: *mut (dyn Checkable + '0); // arg #1 @@ -379,7 +379,7 @@ impl Checkable for i32 { struct test_crate::NoParam::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn NoParam)), + drop: unsafe fn(*mut (dyn NoParam)), method_dummy: fn<'_0_1>(&'_0_1 ((dyn NoParam))), super_trait_0: &'static (core::marker::MetaSized::{vtable}), } @@ -456,7 +456,7 @@ where struct test_crate::Modifiable::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Modifiable)), + drop: unsafe fn(*mut (dyn Modifiable)), method_modify: fn<'_0_1, '_1_1>(&'_0_1 mut ((dyn Modifiable)), &'_1_1 (T)) -> T, super_trait_0: &'static (core::marker::MetaSized::{vtable}), } @@ -498,7 +498,7 @@ where } // Full name: test_crate::{impl Modifiable for i32}::{vtable_drop_shim} -fn {impl Modifiable for i32}::{vtable_drop_shim}(@1: *mut (dyn Modifiable)) +unsafe fn {impl Modifiable for i32}::{vtable_drop_shim}(@1: *mut (dyn Modifiable)) where [@TraitClause0]: Sized, [@TraitClause1]: Clone, @@ -607,7 +607,7 @@ where struct test_crate::BaseOn::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn BaseOn)), + drop: unsafe fn(*mut (dyn BaseOn)), method_operate_on: fn<'_0_1, '_1_1>(&'_0_1 ((dyn BaseOn)), &'_1_1 (T)), super_trait_0: &'static (core::marker::MetaSized::{vtable}), } @@ -629,7 +629,7 @@ where struct test_crate::Both32And64::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn Both32And64)), + drop: unsafe fn(*mut (dyn Both32And64)), method_both_operate: fn<'_0_1, '_1_1, '_2_1>(&'_0_1 ((dyn Both32And64)), &'_1_1 (i32), &'_2_1 (i64)), super_trait_0: &'static (core::marker::MetaSized::{vtable}), super_trait_1: &'static (test_crate::BaseOn::{vtable}), @@ -715,7 +715,7 @@ fn {impl BaseOn for i32}::operate_on<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i3 } // Full name: test_crate::{impl BaseOn for i32}::{vtable_drop_shim} -fn {impl BaseOn for i32}::{vtable_drop_shim}(@1: *mut (dyn BaseOn)) +unsafe fn {impl BaseOn for i32}::{vtable_drop_shim}(@1: *mut (dyn BaseOn)) { let ret@0: (); // return let dyn_self@1: *mut (dyn BaseOn + '0); // arg #1 @@ -803,7 +803,7 @@ fn {impl BaseOn for i32}::operate_on<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i6 } // Full name: test_crate::{impl BaseOn for i32}::{vtable_drop_shim} -fn {impl BaseOn for i32}::{vtable_drop_shim}(@1: *mut (dyn BaseOn)) +unsafe fn {impl BaseOn for i32}::{vtable_drop_shim}(@1: *mut (dyn BaseOn)) { let ret@0: (); // return let dyn_self@1: *mut (dyn BaseOn + '0); // arg #1 @@ -894,7 +894,7 @@ fn {impl Both32And64 for i32}::both_operate<'_0, '_1, '_2>(@1: &'_0 (i32), @2: & } // Full name: test_crate::{impl Both32And64 for i32}::{vtable_drop_shim} -fn {impl Both32And64 for i32}::{vtable_drop_shim}(@1: *mut (dyn Both32And64)) +unsafe fn {impl Both32And64 for i32}::{vtable_drop_shim}(@1: *mut (dyn Both32And64)) { let ret@0: (); // return let dyn_self@1: *mut (dyn Both32And64 + '0); // arg #1 @@ -950,7 +950,7 @@ trait Alias struct test_crate::LifetimeTrait::{vtable} { size: usize, align: usize, - drop: fn(*mut (dyn LifetimeTrait)), + drop: unsafe fn(*mut (dyn LifetimeTrait)), method_lifetime_method: fn<'a, '_1_1>(&'_1_1 ((dyn LifetimeTrait)), &'a (Ty0)) -> &'a (Ty0), super_trait_0: &'static (core::marker::MetaSized::{vtable}), } @@ -1000,7 +1000,7 @@ fn {impl LifetimeTrait for i32}::lifetime_method<'a, '_1>(@1: &'_1 (i32), @2: &' } // Full name: test_crate::{impl LifetimeTrait for i32}::{vtable_drop_shim} -fn {impl LifetimeTrait for i32}::{vtable_drop_shim}(@1: *mut (dyn LifetimeTrait)) +unsafe fn {impl LifetimeTrait for i32}::{vtable_drop_shim}(@1: *mut (dyn LifetimeTrait)) { let ret@0: (); // return let dyn_self@1: *mut (dyn LifetimeTrait + '0); // arg #1