Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 15 additions & 3 deletions crates/synth-cli/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,8 @@ enum Commands {
/// List available compilation backends and their status
Backends,

/// Verify compilation correctness via Z3 (e.g., synth verify input.wat output.elf)
/// Verify compilation correctness via Z3 — requires a build with
/// `--features verify` (e.g., synth verify input.wat output.elf)
Verify {
/// Input WASM or WAT file (source)
#[arg(value_name = "WASM")]
Expand Down Expand Up @@ -2236,8 +2237,19 @@ fn verify_command(wasm_input: PathBuf, elf_input: PathBuf, backend_name: &str) -

#[cfg(not(feature = "verify"))]
{
println!("\n Rebuild with verification support:");
println!(" cargo build --features verify");
// This binary was built without the `verify` feature, so no Z3
// translation validation can run. Returning Ok here would make
// `synth verify` exit success-shaped while doing nothing — a
// script or CI step gating on `synth verify` would silently
// believe the binary was validated (issue #124). Fail loudly
// with a non-zero exit instead.
anyhow::bail!(
"this `synth` binary was built without the `verify` feature — \
Z3 translation validation is unavailable.\n \
Rebuild with verification support:\n \
cargo build --features verify\n \
(or `cargo install --path crates/synth-cli --features verify`)"
);
}
} else if caps.supports_binary_verification {
println!(" Strategy: Binary-level translation validation (ASIL B path)");
Expand Down
Loading