diff --git a/src/test/cargo-rmc/simple-lib/test_one_plus_two.config b/src/test/cargo-rmc/simple-lib/test_one_plus_two.config new file mode 100644 index 000000000000..d6f8e7d59347 --- /dev/null +++ b/src/test/cargo-rmc/simple-lib/test_one_plus_two.config @@ -0,0 +1,2 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT diff --git a/src/test/cargo-rmc/simple-lib/test_sum.config b/src/test/cargo-rmc/simple-lib/test_sum.config new file mode 100644 index 000000000000..d6f8e7d59347 --- /dev/null +++ b/src/test/cargo-rmc/simple-lib/test_sum.config @@ -0,0 +1,2 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT diff --git a/src/test/cargo-rmc/simple-main/main.config b/src/test/cargo-rmc/simple-main/main.config new file mode 100644 index 000000000000..78ced6c2ae4a --- /dev/null +++ b/src/test/cargo-rmc/simple-main/main.config @@ -0,0 +1,3 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +cbmc-flags: --unwind 11 --unwinding-assertions diff --git a/src/test/cargo-rmc/simple-main/main.expected b/src/test/cargo-rmc/simple-main/main.expected index 4253bc716933..bb22bdfec521 100644 --- a/src/test/cargo-rmc/simple-main/main.expected +++ b/src/test/cargo-rmc/simple-main/main.expected @@ -1,2 +1,3 @@ -[main.assertion.1] line 4 assertion failed: 1 == 2: FAILURE +[memcmp.precondition.1] line 19 memcmp region 1 readable: FAILURE +[memcmp.precondition.2] line 21 memcpy region 2 readable: FAILURE VERIFICATION FAILED diff --git a/src/test/cargo-rmc/simple-main/src/main.rs b/src/test/cargo-rmc/simple-main/src/main.rs index 37592b921f22..f4a5e83973cf 100644 --- a/src/test/cargo-rmc/simple-main/src/main.rs +++ b/src/test/cargo-rmc/simple-main/src/main.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +include!("../../../rmc-prelude.rs"); + fn main() { - assert!(1 == 2); + assert!("stationary" == "stationary", "the two words are different"); } diff --git a/src/tools/compiletest/src/header.rs b/src/tools/compiletest/src/header.rs index 997f0b9f902d..4453a167f11b 100644 --- a/src/tools/compiletest/src/header.rs +++ b/src/tools/compiletest/src/header.rs @@ -699,7 +699,13 @@ fn iter_header(testfile: &Path, cfg: Option<&str>, rdr: R, it: &mut dyn return; } - let comment = if testfile.to_string_lossy().ends_with(".rs") { "//" } else { "#" }; + let comment = if testfile.to_string_lossy().ends_with(".rs") { + "//" + } else if testfile.to_string_lossy().ends_with(".config") { + "" + } else { + "#" + }; let mut rdr = BufReader::new(rdr); let mut ln = String::new(); diff --git a/src/tools/compiletest/src/main.rs b/src/tools/compiletest/src/main.rs index 5d62d9fb5340..0e8afdd53a3a 100644 --- a/src/tools/compiletest/src/main.rs +++ b/src/tools/compiletest/src/main.rs @@ -585,14 +585,14 @@ fn collect_tests_from_dir( fs::create_dir_all(&build_dir).unwrap(); // If we find a `Cargo.toml` file in the current directory and we're in - // Cargo-rmc mode, we should look for `*.expected` files and create an - // output directory corresponding to each to avoid race conditions during - // the testing phase. We immediately return after adding the tests to avoid + // Cargo-rmc mode, we should look for `*.config` files and create an output + // directory corresponding to each to avoid race conditions during the + // testing phase. We immediately return after adding the tests to avoid // treating `*.rs` files as tests. if config.mode == Mode::CargoRMC && dir.join("Cargo.toml").exists() { for file in fs::read_dir(dir)? { let file_path = file?.path(); - if file_path.to_str().unwrap().ends_with(".expected") { + if file_path.to_str().unwrap().ends_with(".config") { fs::create_dir_all(&build_dir.join(file_path.file_stem().unwrap())).unwrap(); let paths = TestPaths { file: file_path, relative_dir: relative_dir_path.to_path_buf() }; diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs index 3163dd8d8cb2..5df90cc7c7f6 100644 --- a/src/tools/compiletest/src/runtest.rs +++ b/src/tools/compiletest/src/runtest.rs @@ -2424,20 +2424,23 @@ impl<'test> TestCx<'test> { fn run_cargo_rmc_test(&self) { // We create our own command for the same reasons listed in `run_rmc_test` method. let mut cargo = Command::new("cargo"); - // We run `cargo` on the directory where we found the `*.expected` file + // We run `cargo` on the directory where we found the `*.config` file let parent_dir = self.testpaths.file.parent().unwrap(); - // The name of the function to test is the same as the stem of `*.expected` file + // The name of the function to test is the same as the stem of `*.config` file let function_name = self.testpaths.file.file_stem().unwrap().to_str().unwrap(); cargo .arg("rmc") + .args(&self.props.rmc_flags) .args(["--function", function_name]) .arg("--target") .arg(self.output_base_dir().join("target")) - .arg(&parent_dir); + .arg(&parent_dir) + .arg("--") + .args(&self.props.cbmc_flags); self.add_rmc_dir_to_path(&mut cargo); let proc_res = self.compose_and_run_compiler(cargo, None); - let expected = fs::read_to_string(self.testpaths.file.clone()).unwrap(); - self.verify_output(&proc_res, &expected); + let expected_path = parent_dir.join(function_name.to_string() + ".expected"); + self.verify_output(&proc_res, &expected_path); } /// Runs RMC on the test file specified by `self.testpaths.file`. An error @@ -2453,14 +2456,14 @@ impl<'test> TestCx<'test> { .args(&self.props.cbmc_flags); self.add_rmc_dir_to_path(&mut rmc); let proc_res = self.compose_and_run_compiler(rmc, None); - let expected = - fs::read_to_string(self.testpaths.file.parent().unwrap().join("expected")).unwrap(); - self.verify_output(&proc_res, &expected); + let expected_path = self.testpaths.file.parent().unwrap().join("expected"); + self.verify_output(&proc_res, &expected_path); } /// Print an error if the verification output does not contain the expected - /// lines. - fn verify_output(&self, proc_res: &ProcRes, expected: &str) { + /// lines in the file specified by `path`. + fn verify_output(&self, proc_res: &ProcRes, path: &PathBuf) { + let expected = fs::read_to_string(path).unwrap(); if let Some(line) = TestCx::contains_lines(&proc_res.stdout, expected.split('\n').collect()) { self.fatal_proc_rec(