From a1da3d815e8d9958fed0037d7e8e222bf7852ea4 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Fri, 29 Dec 2023 05:55:42 -0500 Subject: [PATCH] Add a regression test --- tests/verus-consistency.rs | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs index b2667ba..187561a 100644 --- a/tests/verus-consistency.rs +++ b/tests/verus-consistency.rs @@ -1312,3 +1312,31 @@ exec static LAZY_X: Lazy ensures LAZY_X.wf() { Lazy::::new() } } // verus! "###); } + +#[test] +fn verus_requires_clauses_confusable_with_generics() { + // Regression test for https://github.com/jaybosamiya/verusfmt/issues/19 + let file = r#" +verus! { + +fn test() + requires i < 0, len > 0, +{ +} + +} // verus! +"#; + + assert_snapshot!(parse_and_format(file).unwrap(), @r###" + verus! { + + fn test() + requires + i < 0, + len > 0, + { + } + + } // verus! + "###); +}