Add basic support for statics

verus-lang · Dec 24, 2023 · 266f014 · 266f014
1 parent 4fcd45b
commit 266f014
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 5 deletions.
diff --git a/examples/wip.rs b/examples/wip.rs
@@ -1,7 +1,5 @@
 verus! {
 
-fn test() {
-    let tracked mut points_to = points_to_raw.into_typed::<Page>(pt as int);
-}
+exec static THREAD_COUNT: core::sync::atomic::AtomicUsize = core::sync::atomic::AtomicUsize::new(0);
 
 } // verus!
diff --git a/src/lib.rs b/src/lib.rs
@@ -741,7 +741,7 @@ fn to_doc<'a>(
         Rule::union => unsupported(pair),
         //Rule::initializer => soft_indent(arena, map_to_doc(ctx, arena, pair)),
         Rule::r#const => map_to_doc(ctx, arena, pair),
-        Rule::r#static => unsupported(pair),
+        Rule::r#static => map_to_doc(ctx, arena, pair),
         Rule::r#trait => map_to_doc(ctx, arena, pair),
         Rule::trait_alias => unsupported(pair),
         Rule::assoc_items => map_to_doc_lines(ctx, arena, pair),

diff --git a/src/verus.pest b/src/verus.pest
@@ -703,7 +703,7 @@ const = {
 }
 
 static = {
-    attr* ~ visibility? ~
+    attr* ~ visibility? ~ fn_mode? ~
     static_str ~ mut_str? ~ name ~ colon_str ~ type ~
     (eq_str ~ expr)? ~ semi_str
 }

diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
@@ -1154,3 +1154,22 @@ fn test(thread_token: &mut bool) {
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_statics() {
+    let file = r#"
+verus! {
+
+exec static THREAD_COUNT: core::sync::atomic::AtomicUsize = core::sync::atomic::AtomicUsize::new(0);
+
+} // verus!
+"#;
+
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    exec static THREAD_COUNT: core::sync::atomic::AtomicUsize = core::sync::atomic::AtomicUsize::new(0);
+
+    } // verus!
+    "###);
+}