Support attributes in broadcast groups

CHANGELOG.md

@@ -1,5 +1,7 @@
 # Unreleased
 
+* Support attributes in `broadcast group`s
+
 # v0.3.6
 
 * Support parsing empty requires/ensures/... clauses

src/lib.rs

@@ -876,6 +876,7 @@ fn to_doc<'a>(
         Rule::use_tree => map_to_doc(ctx, arena, pair),
         Rule::use_tree_list => comma_delimited(ctx, arena, pair, false).braces().group(),
         Rule::broadcast_use_list => comma_delimited(ctx, arena, pair, false).group(),
+        Rule::broadcast_group_member => map_to_doc(ctx, arena, pair),
         Rule::broadcast_group_list => comma_delimited(ctx, arena, pair, false).braces(),
         Rule::fn_qualifier => map_to_doc(ctx, arena, pair),
         Rule::fn_terminator => map_to_doc(ctx, arena, pair),

src/verus.pest

@@ -950,8 +950,12 @@ broadcast_group_identifier = {
     identifier
 }
 
+broadcast_group_member = {
+    attr* ~ path
+}
+
 broadcast_group_list = {
-    "{" ~ (path ~ ("," ~ path)* ~ ","?)? ~ "}"
+    "{" ~ (broadcast_group_member ~ ("," ~ broadcast_group_member)* ~ ","?)? ~ "}"
 }
 
 broadcast_group = {

tests/verus-consistency.rs

@@ -2362,3 +2362,43 @@ verus! {
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_broadcast_group_with_attributes() {
+    let file = r#"
+verus! {
+#[cfg_attr(verus_keep_ghost, verifier::prune_unless_this_module_is_used)]
+pub broadcast group group_hash_axioms { axiom_hash_map_contains_deref_key,
+  #[cfg(feature = "alloc")]
+    axiom_hash_map_contains_box,
+    axiom_hash_map_maps_deref_key_to_value,
+  #[cfg(feature = "alloc")]
+    #[some_other_attribute]
+    axiom_hash_map_maps_box_key_to_value,
+   axiom_primitive_types_have_deterministic_hash,
+       axiom_random_state_conforms_to_build_hasher_model,
+     axiom_spec_hash_map_len,
+}
+}
+"#;
+
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    #[cfg_attr(verus_keep_ghost, verifier::prune_unless_this_module_is_used)]
+    pub broadcast group group_hash_axioms {
+        axiom_hash_map_contains_deref_key,
+        #[cfg(feature = "alloc")]
+        axiom_hash_map_contains_box,
+        axiom_hash_map_maps_deref_key_to_value,
+        #[cfg(feature = "alloc")]
+        #[some_other_attribute]
+        axiom_hash_map_maps_box_key_to_value,
+        axiom_primitive_types_have_deterministic_hash,
+        axiom_random_state_conforms_to_build_hasher_model,
+        axiom_spec_hash_map_len,
+    }
+
+    } // verus!
+    "###);
+}