Deal with another case where an expression preceding a function body was

misinterpretted as a struct
verus-lang · Dec 24, 2023 · d264a92 · d264a92
1 parent 7c3cd0b
commit d264a92
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 2 deletions.
diff --git a/examples/wip.rs b/examples/wip.rs
@@ -1,5 +1,9 @@
 verus! {
 
-exec static THREAD_COUNT: core::sync::atomic::AtomicUsize = core::sync::atomic::AtomicUsize::new(0);
+fn count_size_overflow()
+    ensures !x.1 ==> x.0 == count * size
+{
+    true
+}
 
 } // verus!
diff --git a/src/verus.pest b/src/verus.pest
@@ -1035,7 +1035,7 @@ fn_block_expr = {
 }
 
 prefix_expr = {
-    attr* ~ (dash_str | bang_str | star_str | triple_or | triple_and) ~ expr
+    attr* ~ (dash_str | bang_str | star_str | triple_or | triple_and) ~ expr_no_struct
 }
 
 assignment_ops = {

diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
@@ -46,6 +46,12 @@ pub fn test_function(x: bool, y: bool) -> u32
     5
 }
 
+fn count_size_overflow()
+    ensures !x.1 ==> x.0 == count * size
+{
+    true
+}
+
 spec fn dec0(a: int) -> int
     decreases a,
     when a
@@ -140,6 +146,13 @@ ensures  res.is_Ok() ==> (res.get_Ok_0().1)@@.results_in(((), *mut_state))
         5
     }
 
+    fn count_size_overflow()
+        ensures
+            !x.1 ==> x.0 == count * size,
+    {
+        true
+    }
+
     spec fn dec0(a: int) -> int
         decreases a,
         when a