Skip to content

Releases: verus-lang/verus-analyzer

2024-12-11

11 Dec 16:54
Compare
Choose a tag to compare
Clean up the release workflow: disable the triggers we don't plan to

use, and remove the special cases for the now merged `infra` branch.

2024-12-05

05 Dec 20:42
6fa093d
Compare
Choose a tag to compare
Various parsing fixes (#39)

Fixes needed to get the source code of the [verified-storage project](https://github.com/microsoft/verified-storage/) to parse correctly, at least on the `kv_dev` branch.  The improvements include:
- Tricky corner cases created by Verus's triple operators (`|||` and `&&&`), including interactions with Rust block expressions
- We no longer confuse Rust's `assert!(...)` for a Verus `assert(...)`
- Fix for `assert(e) by (name)` without a following block
- Proper parsing for both styles of `global` declarations
- Allow `where` to be followed by a `recommends` clause
- Demote verus to be a contextual keyword, so that it will show up as an identifier when used inside an attribute, e.g., as
`#[verus::line_count::ignore]`
- Don't emit an error when we encounter a normal for loop without a named iterator

nightly

03 Dec 13:29
Compare
Choose a tag to compare
nightly Pre-release
Pre-release
Allow dead code in the proof actions