Added --function flag to cargo-rmc (rust-lang#239)

* Added --function flag to cargo-rmc

Author: vecchiot-aws

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
 

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]

src/tools/compiletest/src/runtest.rs

@@ -2442,11 +2442,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();