From 266f014d025b32175d75015508b18813c94f5361 Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@cmu.edu>
Date: Sun, 24 Dec 2023 17:50:26 -0500
Subject: [PATCH] Add basic support for statics

---
 examples/wip.rs            |  4 +---
 src/lib.rs                 |  2 +-
 src/verus.pest             |  2 +-
 tests/verus-consistency.rs | 19 +++++++++++++++++++
 4 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/examples/wip.rs b/examples/wip.rs
index de25766..1e41b63 100644
--- 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
index d1ec17f..a879b74 100644
--- 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
index 4f84974..5754db9 100644
--- 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
index 6079869..344f85e 100644
--- 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!
+    "###);
+}