Fixing test cases and allowing multiple .expected files

model-checking · Jun 28, 2023 · 7e08f3f · 7e08f3f
1 parent c15a591
commit 7e08f3f
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 5 deletions.
diff --git a/tests/expected/function-contract/arbitrary_requires_fail.expected b/tests/expected/function-contract/arbitrary_requires_fail.expected
@@ -2,9 +2,7 @@ RESULTS:
 Check 1: div.assertion.1
  - Status: FAILURE
  - Description: "attempt to divide by zero"
- - Location: arbitrary_requires_fail.rs:6:5 in function div
 
 Check 2: div.division-by-zero.1
  - Status: SUCCESS
  - Description: "division by zero"
- - Location: arbitrary_requires_fail.rs:6:5 in function div
diff --git a/tests/expected/function-contract/arbitrary_requires_pass.expected b/tests/expected/function-contract/arbitrary_requires_pass.expected
@@ -2,9 +2,7 @@ RESULTS:
 Check 1: div.assertion.1
  - Status: SUCCESS
  - Description: "attempt to divide by zero"
- - Location: arbitrary_requires_pass.rs:6:5 in function div
 
 Check 2: div.division-by-zero.1
  - Status: SUCCESS
  - Description: "division by zero"
- - Location: arbitrary_requires_pass.rs:6:5 in function div
diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs
@@ -375,7 +375,12 @@ impl<'test> TestCx<'test> {
  /// the expected output in `expected` file.
  fn run_expected_test(&self) {
  let proc_res = self.run_kani();
- let expected_path = self.testpaths.file.parent().unwrap().join("expected");
+ let dot_expected_path = self.testpaths.file.with_extension("expected");
+ let expected_path = if dot_expected_path.exists() {
+ dot_expected_path
+ } else {
+ self.testpaths.file.parent().unwrap().join("expected")
+ };
  self.verify_output(&proc_res, &expected_path);
  }