bugfix: small lifetime-generate issue for FnDef types

verus-lang · Nov 15, 2024 · 8bc6dd8 · 8bc6dd8
1 parent c3635a2
commit 8bc6dd8
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 0 deletions.
diff --git a/source/rust_verify/src/lifetime_generate.rs b/source/rust_verify/src/lifetime_generate.rs
@@ -1289,6 +1289,7 @@ fn erase_expr<'tcx>(
                     if expect_spec || ctxt.var_modes[&expr.hir_id] == Mode::Spec {
                         None
                     } else {
+                        state.reach_fun(id);
                         let vir_path = def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, id);
                         let fun_name = Arc::new(FunX { path: vir_path });
                         return mk_exp(ExpX::Var(state.fun_name(&fun_name)));

diff --git a/source/rust_verify_test/tests/fndef_types.rs b/source/rust_verify_test/tests/fndef_types.rs
@@ -1704,3 +1704,24 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_vir_error_msg(err, "Foo::clone` is not supported")
 }
+
+test_verify_one_file! {
+    #[test] clone_assign_type_param_trait_function_to_variable verus_code! {
+        use vstd::*;
+
+        pub struct X<T> {
+            pub t: T,
+        }
+
+        impl<T: Clone> Clone for X<T> {
+            fn clone(&self) -> (s: Self)
+                ensures
+                    call_ensures(T::clone, (&self.t,), s.t)
+            {
+                let t_clone = T::clone;
+                let new_t = t_clone(&self.t);
+                X { t: new_t }
+            }
+        }
+    } => Ok(())
+}