diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc index 3ee2f399aa32..501b4052203e 100755 --- a/scripts/cargo-rmc +++ b/scripts/cargo-rmc @@ -29,16 +29,12 @@ def main(): parser.add_argument("--target-dir", default="target", help="Directory for all generated artifacts") parser.add_argument("--wkdir", default=".") + parser.add_argument("--function", default="main") parser.add_argument("crate", help="crate to verify") parser.add_argument("cbmc_args", nargs=argparse.REMAINDER, default=[], help="Pass through directly to CBMC") args = parser.parse_args() - # In the future we hope to make this configurable in the command line. - # For now, however, changing this from "main" breaks rmc. - # Issue: https://github.com/model-checking/rmc/issues/169 - args.function = "main" - if args.quiet: args.verbose = False diff --git a/scripts/rmc.py b/scripts/rmc.py index a6c7d0458692..95fd31725a98 100644 --- a/scripts/rmc.py +++ b/scripts/rmc.py @@ -117,7 +117,7 @@ def run_visualize(cbmc_filename, cbmc_args, verbose=False, quiet=False, keep_tem # 4) cbmc --xml-ui --show-properties ~/rmc/library/rmc/rmc_lib.c temp.goto > property.xml # 5) cbmc-viewer --result results.xml --coverage coverage.xml --property property.xml --srcdir . --goto temp.goto --reportdir report - run_goto_cc(cbmc_filename, temp_goto_filename, verbose, quiet) + run_goto_cc(cbmc_filename, temp_goto_filename, verbose, quiet, function=function) def run_cbmc_local(cbmc_args, output_to): cbmc_cmd = ["cbmc"] + cbmc_args + [temp_goto_filename] diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs index a1958f7f7fd4..3163dd8d8cb2 100644 --- a/src/tools/compiletest/src/runtest.rs +++ b/src/tools/compiletest/src/runtest.rs @@ -2430,11 +2430,10 @@ impl<'test> TestCx<'test> { let function_name = self.testpaths.file.file_stem().unwrap().to_str().unwrap(); cargo .arg("rmc") + .args(["--function", function_name]) .arg("--target") .arg(self.output_base_dir().join("target")) - .arg(&parent_dir) - .arg("--") - .args(["--function", function_name]); + .arg(&parent_dir); 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();