From 7462a855b55188c9fcd9e067d45459cc74c76b55 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 24 Jul 2024 19:28:06 +0000 Subject: [PATCH] compiletest: ensure extra arguments are appended at the end We must not mix arguments to be passed to Kani with those parsed by compiletest. Will enable use of `--cbmc-args` to increase CBMC's verbosity as needed for certain tests. --- tools/compiletest/src/runtest.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 7925ed83e6e5..50f1e3035ac8 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -272,14 +272,14 @@ impl<'test> TestCx<'test> { .arg("kani") .arg("--target-dir") .arg(self.output_base_dir().join("target")) - .current_dir(parent_dir) - .args(&self.config.extra_args); + .current_dir(parent_dir); if test { cargo.arg("--tests"); } if "expected" != self.testpaths.file.file_name().unwrap() { cargo.args(["--harness", function_name]); } + cargo.args(&self.config.extra_args); let proc_res = self.compose_and_run(cargo); self.verify_output(&proc_res, &self.testpaths.file);