Remove obsolete EXPECTED FAIL code from compiletest (#2031)

tools/compiletest/src/runtest.rs

@@ -13,7 +13,6 @@ use crate::header::TestProps;
 use crate::json;
 use crate::read2::read2;
 use crate::util::logv;
-use regex::Regex;
 
 use std::env;
 use std::fs::{self, create_dir_all};
@@ -222,43 +221,19 @@ impl<'test> TestCx<'test> {
     /// message is printed to stdout if the verification result is not expected.
     fn verify(&self) {
         let proc_res = self.run_kani();
-        // If the test file contains expected failures in some locations, ensure
-        // that verification does indeed fail in those locations
-        if proc_res.stdout.contains("EXPECTED FAIL") {
-            let lines = TestCx::verify_expect_fail(&proc_res.stdout);
-            if !lines.is_empty() {
-                self.fatal_proc_rec(
-                    &format!("test failed: expected failure in lines {lines:?}, got success"),
-                    &proc_res,
-                )
-            }
-        } else {
-            // The code above depends too much on the exact string output of
-            // Kani. If the output of Kani changes in the future, the check below
-            // will (hopefully) force some tests to fail and remind us to
-            // update the code above as well.
-            if fs::read_to_string(&self.testpaths.file).unwrap().contains("__VERIFIER_expect_fail")
-            {
-                self.fatal_proc_rec(
-                    "found call to `__VERIFIER_expect_fail` with no corresponding \
-                 \"EXPECTED FAIL\" in Kani's output",
-                    &proc_res,
-                )
-            }
-            // Print an error if the verification result is not expected.
-            if self.props.kani_panic_step == Some(KaniFailStep::Verify) {
-                if proc_res.status.success() {
-                    self.fatal_proc_rec(
-                        "test failed: expected verification failure, got success",
-                        &proc_res,
-                    );
-                }
-            } else if !proc_res.status.success() {
+        // Print an error if the verification result is not expected.
+        if self.props.kani_panic_step == Some(KaniFailStep::Verify) {
+            if proc_res.status.success() {
                 self.fatal_proc_rec(
-                    "test failed: expected verification success, got failure",
+                    "test failed: expected verification failure, got success",
                     &proc_res,
                 );
             }
+        } else if !proc_res.status.success() {
+            self.fatal_proc_rec(
+                "test failed: expected verification success, got failure",
+                &proc_res,
+            );
         }
     }
 
@@ -279,18 +254,6 @@ impl<'test> TestCx<'test> {
         }
     }
 
-    /// If the test file contains expected failures in some locations, ensure
-    /// that verification does not succeed in those locations.
-    fn verify_expect_fail(str: &str) -> Vec<usize> {
-        let re = Regex::new(r"line ([0-9]+) EXPECTED FAIL: SUCCESS").unwrap();
-        let mut lines = vec![];
-        for m in re.captures_iter(str) {
-            let num = m.get(1).unwrap().as_str().parse().unwrap();
-            lines.push(num);
-        }
-        lines
-    }
-
     /// Runs cargo-kani on the function specified by the stem of `self.testpaths.file`.
     /// The `test` parameter controls whether to specify `--tests` to `cargo kani`.
     /// An error message is printed to stdout if verification output does not