rust_verify_test: support expected message in FAILS comment

source/rust_verify_test/tests/common/mod.rs

@@ -462,17 +462,27 @@ pub fn relevant_error_span(err: &Vec<DiagnosticSpan>) -> &DiagnosticSpan {
         .expect("span")
 }
 
+fn assert_diagnostic_fails(diag: &Diagnostic) {
+    // Expect "FAILS" to appear in the diagnostic.
+    let fail_diag_text =
+        relevant_error_span(&diag.spans).text.iter().find(|x| x.text.contains("FAILS"));
+    assert!(fail_diag_text.is_some());
+    let fail_text = &fail_diag_text.unwrap().text;
+
+    // Check expected message, if specified.
+    let expect_re = regex::Regex::new(r"(?m)FAILS:\s*(?<expect>.+)").unwrap();
+    let Some(caps) = expect_re.captures(fail_text) else { return };
+    let expect = &caps["expect"];
+
+    println!("expect message to contain: {expect:?}");
+    assert!(diag.message.contains(expect));
+}
+
 /// Assert that one verification failure happened on source lines containing the string "FAILS".
 #[allow(dead_code)]
 pub fn assert_one_fails(err: TestErr) {
     assert_eq!(err.errors.len(), 1);
-    assert!(
-        relevant_error_span(&err.errors[0].spans)
-            .text
-            .iter()
-            .find(|x| x.text.contains("FAILS"))
-            .is_some()
-    );
+    assert_diagnostic_fails(&err.errors[0]);
 }
 
 /// When this testcase has ONE verification failure,
@@ -494,13 +504,7 @@ pub fn assert_expand_fails(err: TestErr, span_count: usize) {
 pub fn assert_fails(err: TestErr, count: usize) {
     assert_eq!(err.errors.len(), count);
     for c in 0..count {
-        assert!(
-            relevant_error_span(&err.errors[c].spans)
-                .text
-                .iter()
-                .find(|x| x.text.contains("FAILS"))
-                .is_some()
-        );
+        assert_diagnostic_fails(&err.errors[c]);
     }
 }
 

source/rust_verify_test/tests/integer_ring.rs

@@ -183,7 +183,7 @@ test_verify_one_file! {
     #[test]
     #[cfg_attr(not(feature = "singular"), ignore)]
     type_fail verus_code! {
-        proof fn test(x: u32, y: u32, z:u32, m:int) by(integer_ring) // FAILS (not supported)
+        proof fn test(x: u32, y: u32, z:u32, m:int) by(integer_ring) // FAILS: should all be int type
             requires
               (x-y) % m == 0
             ensures
@@ -239,7 +239,7 @@ test_verify_one_file! {
         pub proof fn test(x: int, y: int, m: int) by(integer_ring)
             ensures
                 ((x % m) * y) % m == (x * y) % m,
-                ((x % m) * (y % m)) % m == (x) % m, // FAILS
+                ((x % m) * (y % m)) % m == (x) % m, // FAILS: postcondition not satisfied
                 (x * (y % m)) % m == (x * y) % m
         {}
     } => Err(err) => assert_one_fails(err)
@@ -253,7 +253,7 @@ test_verify_one_file! {
             ensures
                 ((x % m) * y) % m == (x * y) % m,
                 ((x % m) * (y % m)) % m == (x) % m, // FAILS
-                (x * (y % m)) % m == (x) % m // also FAILS (but should not report this, since we stop at the first failure)
+                (x * (y % m)) % m == (x) % m // also fails (but should not report this, since we stop at the first failure)
         {}
     } => Err(err) => assert_one_fails(err)
 }
@@ -263,7 +263,7 @@ test_verify_one_file! {
     #[cfg_attr(not(feature = "singular"), ignore)]
     neq_not_supported verus_code! {
         proof fn test(x: int, y: int, z:int, m:int) by(integer_ring)
-            requires (x-y) % m != 0  //FAILS (not supported)
+            requires (x-y) % m != 0  // FAILS: Unsupported expression
             ensures (x*z + y*z) % m == 0
         {}
     } => Err(err) => assert_one_fails(err)
@@ -274,7 +274,7 @@ test_verify_one_file! {
     #[cfg_attr(not(feature = "singular"), ignore)]
     gt_not_supported verus_code! {
         proof fn test(x: int, y: int, z:int, m:int) by(integer_ring)
-            requires (x-y) % m > 0  //FAILS (not supported)
+            requires (x-y) % m > 0  // FAILS: Unsupported expression
             ensures (x*z + y*z) % m == 0
         {}
     } => Err(err) => assert_one_fails(err)
@@ -286,7 +286,7 @@ test_verify_one_file! {
     lt_not_supported verus_code! {
         proof fn test(x: int, y: int, z:int, m:int) by(integer_ring)
             requires (x-y) % m == 0
-            ensures (x*z + y*z) % m < 0 //FAILS (not supported)
+            ensures (x*z + y*z) % m < 0 // FAILS: Unsupported expression
         {}
     } => Err(err) => assert_one_fails(err)
 }

source/vir/src/sst_to_air.rs

@@ -2604,7 +2604,7 @@ pub(crate) fn body_stm_to_air(
             for req in reqs.iter() {
                 let error = error_with_label(
                     &req.span,
-                    "Unspported expression in integer_ring".to_string(),
+                    "Unsupported expression in integer_ring".to_string(),
                     "at the require clause".to_string(),
                 );
                 let air_expr = exp_to_expr(ctx, req, &ExprCtxt::new_mode(ExprMode::BodyPre))?;
@@ -2616,7 +2616,7 @@ pub(crate) fn body_stm_to_air(
             for ens in post_condition.ens_exps.iter() {
                 let error = error_with_label(
                     &ens.span,
-                    "Unspported expression in integer_ring".to_string(),
+                    "Unsupported expression in integer_ring".to_string(),
                     "at the ensure clause".to_string(),
                 );
                 let air_expr = exp_to_expr(ctx, ens, &ExprCtxt::new_mode(ExprMode::BodyPre))?;