support attributes on broadcast group items

verus-lang · Apr 7, 2024 · f041289 · f041289
1 parent d3dda00
commit f041289
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/src/verus.pest b/src/verus.pest
@@ -916,7 +916,7 @@ broadcast_group_list = {
 }
 
 broadcast_group = {
-    visibility? ~ broadcast_str ~ group_str ~ broadcast_group_identifier ~ broadcast_group_list
+    attr* ~ visibility? ~ broadcast_str ~ group_str ~ broadcast_group_identifier ~ broadcast_group_list
 }
 
 //****************************//

diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
@@ -1879,6 +1879,7 @@ mod ring {
         }
     }
 
+    #[verifier::prune_unless_this_module_is_used]
     pub    broadcast    group    properties {
     Ring::spec_succ_ensures,
             Ring::spec_prev_ensures,
@@ -1972,6 +1973,7 @@ mod m4 {
             }
         }
 
+        #[verifier::prune_unless_this_module_is_used]
         pub broadcast group properties {
             Ring::spec_succ_ensures,
             Ring::spec_prev_ensures,