add regression test for misleading error message

addresses #387 (comment)
verus-lang · Aug 16, 2023 · 5c40584 · 5c40584
1 parent b7be992
commit 5c40584
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/source/rust_verify_test/tests/regression.rs b/source/rust_verify_test/tests/regression.rs
@@ -666,3 +666,11 @@ test_verify_one_file! {
         assert!(err.errors[0].rendered.contains("let tracked x: i32 = s;"));
     }
 }
+
+test_verify_one_file! {
+    #[test] test_unwrapped_tracked_wrong_span_387_discussioncomment_6680621 verus_code! {
+        exec fn f(foo: &mut usize) {
+            let tracked tracked_foo = Tracked(foo);
+        }
+    } => Err(err) => { err.errors[0].rendered.contains("let tracked tracked_foo = Tracked(foo);"); }
+}