Skip to content

Commit

Permalink
compiletest: ensure extra arguments are appended at the end
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
tautschnig committed Jul 24, 2024
1 parent 1b1a9b6 commit 7462a85
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions tools/compiletest/src/runtest.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down

0 comments on commit 7462a85

Please sign in to comment.