allow #[verifier(external_body)] again on consts

* add failing test for #1322
verus-lang · Oct 29, 2024 · f94e290 · f94e290
1 parent 5f2d2fc
commit f94e290
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 0 deletions.
diff --git a/source/rust_verify/src/external.rs b/source/rust_verify/src/external.rs
@@ -478,6 +478,7 @@ impl<'a> GeneralItem<'a> {
                 ItemKind::Struct(..) => true,
                 ItemKind::Enum(..) => true,
                 ItemKind::Union(..) => true,
+                ItemKind::Const(..) => true,
                 _ => false,
             },
             GeneralItem::ForeignItem(_) => false,

diff --git a/source/rust_verify_test/tests/consts.rs b/source/rust_verify_test/tests/consts.rs
@@ -341,3 +341,18 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_one_fails(err)
 }
+
+test_verify_one_file! {
+    #[test] allow_external_body_const_regression_1322_1 verus_code! {
+        #[verifier(external_body)]
+        const A: usize = unimplemented!();
+    } => Ok(())
+}
+
+test_verify_one_file! {
+    // TODO un-ignore once fixed
+    #[ignore] #[test] allow_external_body_const_regression_1322_2 verus_code! {
+        #[verifier(external_body)]
+        const A: usize ensures 32 <= A <= 52 { unimplemented!() }
+    } => Ok(())
+}