From 1b6fefae898d0a8c198b4aead71aaf885add603a Mon Sep 17 00:00:00 2001 From: Ivo Matijasevic Date: Tue, 6 Oct 2026 23:30:45 +0200 Subject: [PATCH] Write an INCOMPLETE marker before JSON verification RFC 0015 says an earlier --export-json file is replaced by an INCOMPLETE marker when verification begins, so a killed run cannot leave an older COMPLETE document that looks current. Kani now builds the run context once after harness selection, writes the marker atomically, and then replaces it with the terminal document from the same context. A failed marker write stops the run before any harness is verified. The new json-handler/incomplete-marker test blocks a fake cbmc, then kills the driver (the marker stays) or releases it (the terminal document keeps the marker's fields), and checks a bad export path and a rejected harness filter. --- docs/src/verification-results.md | 2 +- kani-driver/src/frontend/schema_utils.rs | 160 ++++++++++++-- kani-driver/src/main.rs | 3 +- rfc/src/rfcs/0015-export-json.md | 7 +- .../json-handler/incomplete-marker/config.yml | 3 + .../incomplete-marker/fake_cbmc.py | 34 +++ tests/json-handler/incomplete-marker/run.py | 208 ++++++++++++++++++ tests/json-handler/incomplete-marker/test.rs | 7 + tests/json-handler/incomplete-marker/test.sh | 11 + 9 files changed, 411 insertions(+), 24 deletions(-) create mode 100644 tests/json-handler/incomplete-marker/config.yml create mode 100755 tests/json-handler/incomplete-marker/fake_cbmc.py create mode 100755 tests/json-handler/incomplete-marker/run.py create mode 100644 tests/json-handler/incomplete-marker/test.rs create mode 100755 tests/json-handler/incomplete-marker/test.sh diff --git a/docs/src/verification-results.md b/docs/src/verification-results.md index 5b84c74def3f..3a98aa80c9e5 100644 --- a/docs/src/verification-results.md +++ b/docs/src/verification-results.md @@ -185,4 +185,4 @@ cargo kani -Z export-json --export-json kani.json The file describes the tool versions, the configuration and the outcome of every harness. The format is unstable and may change between releases; see [RFC 0015](https://model-checking.github.io/kani/rfc/rfcs/0015-export-json.html) for the schema. The flag requires `-Z export-json`; `-Z unstable-options` alone is no longer enough. -This version never writes the `INCOMPLETE` marker that the RFC describes. If a run is killed, the file from an earlier run can stay in place and look complete. Compare its `started_at` with the time of your run. +After a successful build and harness selection, Kani replaces any earlier file with an `INCOMPLETE` marker before verification starts, and replaces the marker with the final document at the end. A killed or failed run can leave the marker. A failure before the marker is written leaves any earlier file in place; compare its `started_at` with the time of your run. diff --git a/kani-driver/src/frontend/schema_utils.rs b/kani-driver/src/frontend/schema_utils.rs index 54becf0eb01a..68dc394937ca 100644 --- a/kani-driver/src/frontend/schema_utils.rs +++ b/kani-driver/src/frontend/schema_utils.rs @@ -32,7 +32,7 @@ const KANI_GIT_SHA: Option<&str> = option_env!("KANI_GIT_SHA"); /// `None` exactly when `KANI_GIT_SHA` is `None`. const KANI_GIT_DIRTY: Option<&str> = option_env!("KANI_GIT_DIRTY"); -struct RunContext { +pub(crate) struct RunContext { cbmc_version: Option, rustc_version: Option, kani_commit: Option<&'static str>, @@ -42,21 +42,29 @@ struct RunContext { harness_timeout_s: Option, configuration: ConfigurationExport, started_at: OffsetDateTime, - wall_time: Duration, } impl KaniSession { - /// Writes `--export-json` for a completed run; no-op if unset. `matched_harnesses` must be - /// the pre-verification list, not `results`, which `--fail-fast` can truncate. - pub fn write_export_json( + /// Writes the `--export-json` marker and returns its context; no-op if unset. + pub(crate) fn begin_export_json( &self, matched_harnesses: &[&HarnessMetadata], - results: &[HarnessResult<'_>], started_at: OffsetDateTime, + ) -> Result> { + let Some(path) = &self.args.export_json else { return Ok(None) }; + let ctx = self.build_run_context(matched_harnesses, started_at); + write_json_atomically(path, &IncompleteRun::from(&ctx))?; + Ok(Some(ctx)) + } + + /// Writes the terminal `--export-json` document; no-op if unset. + pub fn write_export_json( + &self, + results: &[HarnessResult<'_>], + ctx: Option, wall_time: Duration, ) -> Result<()> { - let Some(path) = &self.args.export_json else { return Ok(()) }; - let ctx = self.build_run_context(matched_harnesses, started_at, wall_time); + let (Some(path), Some(ctx)) = (&self.args.export_json, ctx) else { return Ok(()) }; let export = ExportedRun::from_harness_results( results, |harness| { @@ -67,6 +75,7 @@ impl KaniSession { ) }, ctx, + wall_time, ); write_json_atomically(path, &export) } @@ -75,7 +84,6 @@ impl KaniSession { &self, matched_harnesses: &[&HarnessMetadata], started_at: OffsetDateTime, - wall_time: Duration, ) -> RunContext { let enabled_unstable_features: BTreeSet = self .args @@ -104,7 +112,6 @@ impl KaniSession { harness_timeout_s: self.args.harness_timeout.map(|t| Duration::from(t).as_secs_f64()), configuration: configuration_from(&self.args), started_at, - wall_time, } } } @@ -287,6 +294,49 @@ struct ToolsExport { cbmc: Option, } +#[derive(Serialize)] +struct IncompleteRun<'a> { + schema_version: &'static str, + kani_commit: Option<&'static str>, + kani_commit_dirty: Option, + tools: ToolsExport, + enabled_unstable_features: &'a BTreeSet, + harness_selection: &'a HarnessSelectionExport, + harness_timeout_s: Option, + configuration: &'a ConfigurationExport, + run_state: IncompleteState, + target: &'static str, + started_at: String, +} + +#[derive(Serialize)] +#[serde(rename_all = "SCREAMING_SNAKE_CASE")] +enum IncompleteState { + Incomplete, +} + +impl<'a> From<&'a RunContext> for IncompleteRun<'a> { + fn from(ctx: &'a RunContext) -> Self { + Self { + schema_version: SCHEMA_VERSION, + kani_commit: ctx.kani_commit, + kani_commit_dirty: ctx.kani_commit_dirty, + tools: ToolsExport { + kani: KANI_VERSION, + rustc: ctx.rustc_version.clone(), + cbmc: ctx.cbmc_version.clone(), + }, + enabled_unstable_features: &ctx.enabled_unstable_features, + harness_selection: &ctx.harness_selection, + harness_timeout_s: ctx.harness_timeout_s, + configuration: &ctx.configuration, + run_state: IncompleteState::Incomplete, + target: env!("TARGET"), + started_at: format_started_at(ctx.started_at), + } + } +} + #[derive(Serialize)] struct ExportedRun { schema_version: &'static str, @@ -616,6 +666,7 @@ impl ExportedRun { results: &[HarnessResult<'_>], resolve: impl Fn(&HarnessMetadata) -> (Option, Option), ctx: RunContext, + wall_time: Duration, ) -> Self { let mut harnesses: Vec = results .iter() @@ -660,7 +711,7 @@ impl ExportedRun { run_state, target: env!("TARGET"), started_at: format_started_at(ctx.started_at), - wall_time_s: ctx.wall_time.as_secs_f64(), + wall_time_s: wall_time.as_secs_f64(), harnesses, summary, } @@ -885,7 +936,6 @@ mod tests { harness_timeout_s: None, configuration: test_ctx_config(), started_at: started(), - wall_time: Duration::from_millis(1), } } @@ -894,13 +944,86 @@ mod tests { } fn export_with(results: &[HarnessResult<'_>], ctx: RunContext) -> ExportedRun { - ExportedRun::from_harness_results(results, cadical, ctx) + ExportedRun::from_harness_results(results, cadical, ctx, Duration::from_millis(1)) } fn export_one(hr: HarnessResult<'_>) -> ExportedRun { export_with(&[hr], test_context()) } + #[test] + fn incomplete_marker_serializes_only_marker_fields() { + let mut ctx = test_context(); + ctx.kani_commit = Some("abc123"); + ctx.kani_commit_dirty = Some(true); + ctx.rustc_version = Some("rustc test".to_string()); + ctx.cbmc_version = Some("CBMC test".to_string()); + ctx.enabled_unstable_features.insert("export-json".to_string()); + + let marker = serde_json::to_value(IncompleteRun::from(&ctx)).unwrap(); + let keys: BTreeSet<&str> = marker.as_object().unwrap().keys().map(String::as_str).collect(); + assert_eq!( + keys, + BTreeSet::from([ + "configuration", + "enabled_unstable_features", + "harness_selection", + "harness_timeout_s", + "kani_commit", + "kani_commit_dirty", + "run_state", + "schema_version", + "started_at", + "target", + "tools", + ]) + ); + assert_eq!(marker["run_state"], "INCOMPLETE"); + assert_eq!(marker["kani_commit"], "abc123"); + assert_eq!(marker["kani_commit_dirty"], true); + assert_eq!(marker["tools"]["rustc"], "rustc test"); + assert_eq!(marker["tools"]["cbmc"], "CBMC test"); + let null_marker = serde_json::to_value(IncompleteRun::from(&test_context())).unwrap(); + assert!(null_marker["kani_commit"].is_null()); + assert!(null_marker["kani_commit_dirty"].is_null()); + assert!(null_marker["tools"]["rustc"].is_null()); + assert!(null_marker["tools"]["cbmc"].is_null()); + } + + #[test] + fn incomplete_marker_and_terminal_export_share_context() { + let mut ctx = test_context(); + ctx.kani_commit = Some("shared-commit"); + ctx.cbmc_version = Some("shared CBMC".to_string()); + ctx.enabled_unstable_features.insert("export-json".to_string()); + let marker = serde_json::to_value(IncompleteRun::from(&ctx)).unwrap(); + + let h = harness("h"); + let hr = HarnessResult { harness: &h, result: success_result(vec![]) }; + let terminal = serde_json::to_value(ExportedRun::from_harness_results( + &[hr], + cadical, + ctx, + Duration::from_millis(500), + )) + .unwrap(); + + for key in [ + "schema_version", + "kani_commit", + "kani_commit_dirty", + "tools", + "enabled_unstable_features", + "harness_selection", + "harness_timeout_s", + "configuration", + "target", + "started_at", + ] { + assert_eq!(marker[key], terminal[key], "shared field {key}"); + } + } + #[test] fn export_all_successful() { let h = harness("my_harness"); @@ -911,12 +1034,9 @@ mod tests { let result = success_result(properties); let hr = HarnessResult { harness: &h, result }; - let ctx = RunContext { - cbmc_version: Some("CBMC 6.8.0".to_string()), - wall_time: Duration::from_millis(500), - ..test_context() - }; - let export = export_with(&[hr], ctx); + let ctx = RunContext { cbmc_version: Some("CBMC 6.8.0".to_string()), ..test_context() }; + let export = + ExportedRun::from_harness_results(&[hr], cadical, ctx, Duration::from_millis(500)); let v = serde_json::to_value(&export).unwrap(); assert_eq!(v["schema_version"], "0.1.0"); @@ -1797,6 +1917,7 @@ mod tests { &[hr], |_| (Some("cadical".to_string()), Some(7)), test_context(), + Duration::from_millis(1), )) .unwrap(); let hj = &v["harnesses"][0]; @@ -1936,6 +2057,7 @@ mod tests { &[hr], |_| (Some("totally-unfamiliar-solver-v9".to_string()), None), test_context(), + Duration::from_millis(1), )) .unwrap(); assert_eq!(v["harnesses"][0]["resolved_solver"], "totally-unfamiliar-solver-v9"); diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 1bce00357e67..97232f8ada5a 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -191,6 +191,7 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> { let harnesses = session.determine_targets(project.get_all_harnesses())?; debug!(n = harnesses.len(), ?harnesses, "verify_project"); + let export_context = session.begin_export_json(&harnesses, started_at)?; // Verification let runner = harness_runner::HarnessRunner { sess: &session, project: &project }; @@ -215,7 +216,7 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> { session.save_coverage_results(&project, &results, ×tamp)?; } - session.write_export_json(&harnesses, &results, started_at, start_instant.elapsed())?; + session.write_export_json(&results, export_context, start_instant.elapsed())?; session.write_sarif(&results)?; if !session.args.common_args.quiet { session.print_final_summary(&results)?; diff --git a/rfc/src/rfcs/0015-export-json.md b/rfc/src/rfcs/0015-export-json.md index a8df498d0a4c..c4122cd4b0df 100644 --- a/rfc/src/rfcs/0015-export-json.md +++ b/rfc/src/rfcs/0015-export-json.md @@ -244,7 +244,8 @@ Each write puts full JSON in a temporary file in the target directory, then atom the target (same-filesystem POSIX rename). A mid-write kill leaves the previous target and possibly an orphaned temp file, never a partially written target. After building and selecting harnesses, when verification begins, an atomic `INCOMPLETE` marker replaces any earlier file. It contains known -pre-verification fields, without `outcome`, `wall_time_s`, `summary` or `harnesses[]`. +pre-verification fields, without `outcome`, `wall_time_s`, `summary` or `harnesses[]`. The marker is also +written for an empty, unfiltered harness selection before the terminal `NO_HARNESSES_SELECTED` document replaces it. First check `schema_version` (refuse unsupported major or, pre-1.0, minor), then `run_state`: - Only `COMPLETE` is complete verification evidence: every selected harness has an entry, regardless of outcome. @@ -257,7 +258,7 @@ deletion fails closed on `ENOENT`. Concurrent writers to one path are unsupporte `NO_HARNESSES_SELECTED` means an unfiltered project/workspace with no selectable proof harness or eligible autoharness function: `requested_filters == []`, `unmatched_filters == []`, `matched_count == 0`. A wholly unmatched filter set, or any unmatched `--exact` filter, errors non-zero before export (#4743). -Nonempty `unmatched_filters` occurs only without `--exact` in `COMPLETE`/`PARTIAL` when another filter matched. +Nonempty `unmatched_filters` occurs only without `--exact` in `INCOMPLETE`/`COMPLETE`/`PARTIAL` when another filter matched. ## Rationale and alternatives @@ -420,7 +421,7 @@ The narrower `INCOMPLETE` marker follows its presence matrix below. | `run_state` | `"INCOMPLETE"` \| `"COMPLETE"` \| `"PARTIAL"` \| `"NO_HARNESSES_SELECTED"` | — | Trust is based on this field; see Completeness under Reading the results. | | `target` | string | — | The Rust target triple Kani itself was built for. | | `started_at` | string | — | UTC, `YYYY-MM-DDTHH:MM:SSZ` (second resolution). Taken after the build, when target selection starts. | -| `wall_time_s` | number | — | Seconds from target selection to the start of the export write: target selection, verification and coverage output. The build is not included. Volatile between runs by design (see "Interaction with other flags"). | +| `wall_time_s` | number | — | Seconds from target selection to the start of the terminal export write: target selection, the tool version probes and the marker write, verification and coverage output. The build is not included. Volatile between runs by design (see "Interaction with other flags"). | | `harnesses[]` | array of harness objects | never null, may be empty (e.g. under `NO_HARNESSES_SELECTED`) | Sorted by `(crate_name, file, line, name)`. | | `harnesses[].name` | string | — | Fully qualified `pretty_name`; see Selection under Reading the results. | | `harnesses[].crate_name` | string | — | Distinguishes same-named harnesses across crates in one workspace. | diff --git a/tests/json-handler/incomplete-marker/config.yml b/tests/json-handler/incomplete-marker/config.yml new file mode 100644 index 000000000000..8258439d3e3f --- /dev/null +++ b/tests/json-handler/incomplete-marker/config.yml @@ -0,0 +1,3 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: test.sh diff --git a/tests/json-handler/incomplete-marker/fake_cbmc.py b/tests/json-handler/incomplete-marker/fake_cbmc.py new file mode 100755 index 000000000000..2f996c121173 --- /dev/null +++ b/tests/json-handler/incomplete-marker/fake_cbmc.py @@ -0,0 +1,34 @@ +#!/usr/bin/env python3 +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +import json +import os +import sys +import time + + +def main(): + real_cbmc = os.environ["REAL_CBMC"] + if sys.argv[1:] == ["--version"]: + os.execv(real_cbmc, [real_cbmc, "--version"]) + + ready = os.environ["FAKE_CBMC_READY"] + record = {"pid": os.getpid(), "ppid": os.getppid()} + temporary = f"{ready}.{os.getpid()}.tmp" + with open(temporary, "w", encoding="utf-8") as output: + json.dump(record, output) + os.replace(temporary, ready) + + deadline = time.monotonic() + float(os.environ.get("FAKE_CBMC_TIMEOUT_S", "25")) + release = os.environ["FAKE_CBMC_RELEASE"] + while time.monotonic() < deadline: + if os.path.exists(release): + os.execv(real_cbmc, [real_cbmc, *sys.argv[1:]]) + time.sleep(0.02) + print("fake cbmc timed out waiting for release", file=sys.stderr) + return 124 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/tests/json-handler/incomplete-marker/run.py b/tests/json-handler/incomplete-marker/run.py new file mode 100755 index 000000000000..272c2375a7ad --- /dev/null +++ b/tests/json-handler/incomplete-marker/run.py @@ -0,0 +1,208 @@ +#!/usr/bin/env python3 +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +import datetime +import json +import os +import pathlib +import shutil +import signal +import subprocess +import sys +import tempfile +import time + + +POLL_TIMEOUT_S = 30 + + +def load_json(path): + with path.open(encoding="utf-8") as source: + return json.load(source) + + +def remove(path): + try: + path.unlink() + except FileNotFoundError: + pass + + +def cleanup_group(pid): + try: + os.killpg(pid, signal.SIGKILL) + except (ProcessLookupError, PermissionError): + pass + + +def wait_for_marker(process, ready, output): + deadline = time.monotonic() + POLL_TIMEOUT_S + while time.monotonic() < deadline: + if process.poll() is not None: + raise AssertionError(f"Kani exited before CBMC blocked: {process.returncode}") + try: + record = load_json(ready) + marker = load_json(output) + except (FileNotFoundError, json.JSONDecodeError): + time.sleep(0.02) + continue + if marker.get("run_state") == "INCOMPLETE": + return record, marker + time.sleep(0.02) + raise AssertionError("timed out waiting for fake CBMC and the INCOMPLETE marker") + + +def start_kani(command, environment, root, groups): + process = subprocess.Popen( + command, + cwd=root, + env=environment, + stdout=subprocess.DEVNULL, + stderr=subprocess.DEVNULL, + start_new_session=True, + ) + groups.append(process.pid) + return process + + +def wait_for_next_utc_second(): + previous = datetime.datetime.now(datetime.timezone.utc).strftime("%Y-%m-%dT%H:%M:%SZ") + deadline = time.monotonic() + 2 + while time.monotonic() < deadline: + current = datetime.datetime.now(datetime.timezone.utc).strftime("%Y-%m-%dT%H:%M:%SZ") + if current != previous: + return + time.sleep(0.01) + raise AssertionError("UTC second did not advance") + + +def main(): + kani = pathlib.Path(sys.argv[1]) + real_cbmc = pathlib.Path(sys.argv[2]).resolve() + suite_dir = pathlib.Path(sys.argv[3]).resolve() + with tempfile.TemporaryDirectory(prefix="kani-incomplete-marker-") as temporary: + groups = [] + root = pathlib.Path(temporary) + output = root / "export.json" + ready = root / "ready.json" + release = root / "release" + fake_bin = root / "bin" + fake_bin.mkdir() + os.symlink(suite_dir / "fake_cbmc.py", fake_bin / "cbmc") + test = root / "test.rs" + shutil.copyfile(suite_dir / "test.rs", test) + + base_command = [ + str(kani), + "-Z", + "export-json", + str(test), + "--export-json", + str(output), + "--quiet", + ] + seeded = subprocess.run(base_command, cwd=root, capture_output=True, text=True) + assert seeded.returncode == 0, seeded.stderr + seeded_export = load_json(output) + assert seeded_export["run_state"] == "COMPLETE" + wait_for_next_utc_second() + + environment = os.environ.copy() + environment.update( + { + "PATH": f"{fake_bin}{os.pathsep}{environment['PATH']}", + "REAL_CBMC": str(real_cbmc), + "FAKE_CBMC_READY": str(ready), + "FAKE_CBMC_RELEASE": str(release), + "FAKE_CBMC_TIMEOUT_S": "25", + } + ) + + try: + # A killed driver leaves the INCOMPLETE marker bytes in place. + remove(ready) + remove(release) + process = start_kani(base_command, environment, root, groups) + record, marker = wait_for_marker(process, ready, output) + assert record["ppid"] == process.pid, (record, process.pid) + marker_bytes = output.read_bytes() + os.kill(process.pid, signal.SIGKILL) + assert process.wait(timeout=5) == -signal.SIGKILL + assert output.read_bytes() == marker_bytes + assert marker["run_state"] == "INCOMPLETE" + assert marker["started_at"] != seeded_export["started_at"] + for key in ["outcome", "wall_time_s", "summary", "harnesses"]: + assert key not in marker, key + cleanup_group(process.pid) + + # Releasing CBMC replaces the marker with a terminal document from the same context. + remove(ready) + remove(release) + process = start_kani(base_command, environment, root, groups) + record, marker = wait_for_marker(process, ready, output) + assert record["ppid"] == process.pid, (record, process.pid) + wait_for_next_utc_second() + release.touch() + assert process.wait(timeout=POLL_TIMEOUT_S) == 0 + terminal = load_json(output) + assert terminal["run_state"] == "COMPLETE" + assert terminal["started_at"] == marker["started_at"], ( + terminal["started_at"], + marker["started_at"], + ) + for key, value in marker.items(): + if key != "run_state": + assert terminal[key] == value, key + + # A marker write error prevents CBMC from starting. + remove(ready) + remove(release) + regular_file = root / "regular-file" + regular_file.write_text("not a directory", encoding="utf-8") + bad_parent = regular_file / "child" / "export.json" + command = [*base_command] + command[command.index(str(output))] = str(bad_parent) + result = subprocess.run( + command, + cwd=root, + env=environment, + capture_output=True, + text=True, + timeout=POLL_TIMEOUT_S, + ) + diagnostic = result.stdout + result.stderr + assert result.returncode != 0, diagnostic + assert "Failed to create --export-json output directory" in diagnostic, diagnostic + assert not ready.exists() + + # Rejected selection leaves the seeded terminal file unchanged. + remove(ready) + remove(release) + seeded_bytes = output.read_bytes() + command = [*base_command, "--harness", "does-not-exist"] + result = subprocess.run( + command, + cwd=root, + env=environment, + capture_output=True, + text=True, + timeout=POLL_TIMEOUT_S, + ) + diagnostic = result.stdout + result.stderr + expected = ( + "Failed to match the following harness(es):\n" + "does-not-exist\n" + "Please specify the fully-qualified name of a harness." + ) + assert result.returncode != 0, diagnostic + assert expected in diagnostic, diagnostic + assert output.read_bytes() == seeded_bytes + assert not ready.exists() + finally: + for pid in groups: + cleanup_group(pid) + + +if __name__ == "__main__": + main() diff --git a/tests/json-handler/incomplete-marker/test.rs b/tests/json-handler/incomplete-marker/test.rs new file mode 100644 index 000000000000..b216a49f130b --- /dev/null +++ b/tests/json-handler/incomplete-marker/test.rs @@ -0,0 +1,7 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn check_true() { + assert!(true); +} diff --git a/tests/json-handler/incomplete-marker/test.sh b/tests/json-handler/incomplete-marker/test.sh new file mode 100755 index 000000000000..22208e6b4abe --- /dev/null +++ b/tests/json-handler/incomplete-marker/test.sh @@ -0,0 +1,11 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eu + +SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +KANI_BIN="$(command -v kani)" +CBMC_BIN="$(command -v cbmc)" + +python3 "$SCRIPT_DIR/run.py" "$KANI_BIN" "$CBMC_BIN" "$SCRIPT_DIR"