add regression test, fixes #1322, external_body const no longer panic…

…s verus
verus-lang · Jan 22, 2025 · edcff70 · edcff70
1 parent f172d14
commit edcff70
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/source/rust_verify_test/tests/consts.rs b/source/rust_verify_test/tests/consts.rs
@@ -406,3 +406,10 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] allow_external_body_const_regression_1322 verus_code! {
+        #[verifier(external_body)]
+        const A: usize = unimplemented!();
+    } => Err(err) => assert_rust_error_msg(err, "evaluation of constant value failed")
+}