verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.06k stars 58 forks source link

Support parsing of assert macro with `syn_verus` #1160

Closed matthias-brun closed 3 weeks ago

matthias-brun commented 3 weeks ago

This PR makes a small change to syn_verus to support parsing macros named assert. Without this change, syn_verus fails to parse files containing an assert macro. For example, the line counting tool currently fails to parse the file pervasive.rs in vstd because of this.

The same issue exists for assume and reveal, which would be similarly easy to fix, if we want to, but assert!, being a commonly-used macro, seems particularly important to support.