rapx 0.7.20

#![allow(clippy::bool_assert_comparison)]
use fs4::fs_std::FileExt;
use std::ffi::OsString;
use std::fs::File;
use std::path::{Path, PathBuf};
use std::process::Command;

/// Checks if any bug message in the output has confidence > 50
pub fn detected_high_confidence(output: &str) -> bool {
    // Regex to find confidence, e.g., `confidence 50%`
    let re = regex::Regex::new(r"confidence (\d+)%").unwrap();
    output.lines().any(|line| {
        if let Some(cap) = re.captures(line) {
            if let Some(conf_str) = cap.get(1) {
                if let Ok(conf) = conf_str.as_str().parse::<u32>() {
                    return conf > 10;
                }
            }
        }
        false
    })
}

#[inline(always)]
fn project_path(dir: &str) -> PathBuf {
    Path::new("tests").join(dir)
}

/// Count `  Path [` lines inside a function's output block.
fn path_count_for(output: &str, fn_name: &str) -> usize {
    let header = format!("Function: \"{}\":", fn_name);
    let mut in_block = false;
    let mut count = 0;
    for line in output.lines() {
        if line.contains(&header) {
            in_block = true;
            continue;
        }
        if in_block {
            if line.contains("Function:") {
                break;
            }
            if line.trim().starts_with("Path [") {
                count += 1;
            }
        }
    }
    count
}

#[inline(always)]
fn run_with_args(dir: &str, args: &[&str]) -> String {
    // let raw_path = "./tests/".to_owned() + dir;
    // let project_path = Path::new(&raw_path);
    let project_path = project_path(dir);

    let lock_path = project_path.join(".rapx-test.lock");
    let lock_file = File::create(&lock_path).expect("Failed to create lock file");
    lock_file.lock_exclusive().expect("Failed to acquire lock");

    let mut command = cargo_rapx_command();
    let output = command
        .args(args)
        .current_dir(project_path)
        .output()
        .expect("Failed to execute cargo rapx");

    lock_file.unlock().expect("Failed to release lock");

    String::from_utf8_lossy(&output.stderr).into_owned()
}

fn cargo_rapx_command() -> Command {
    if let Some(path) = option_env!("CARGO_BIN_EXE_cargo-rapx") {
        let path = PathBuf::from(path);
        let mut command = Command::new(&path);
        command.arg("rapx");
        prepend_local_bin_to_path(&mut command, path.parent());
        return command;
    }

    let mut command = Command::new("cargo");
    command.arg("rapx");
    command
}

fn prepend_local_bin_to_path(command: &mut Command, cargo_rapx_dir: Option<&Path>) {
    let local_rapx_dir = option_env!("CARGO_BIN_EXE_rapx")
        .and_then(|path| PathBuf::from(path).parent().map(Path::to_path_buf))
        .or_else(|| cargo_rapx_dir.map(Path::to_path_buf));
    let Some(local_rapx_dir) = local_rapx_dir else {
        return;
    };

    let mut paths = vec![local_rapx_dir];
    if let Some(path) = std::env::var_os("PATH") {
        paths.extend(std::env::split_paths(&path));
    }
    if let Ok(path) = std::env::join_paths(paths) {
        command.env("PATH", OsString::from(path));
    }
}

fn assert_contain(output: &str, pattern: &str) {
    assert!(
        output.contains(pattern),
        "Missing pattern:\n{}\nFull output:\n{}",
        pattern,
        output
    );
}

fn assert_not_contain(output: &str, pattern: &str) {
    assert!(
        !output.contains(pattern),
        "Unexpected pattern:\n{}\nFull output:\n{}",
        pattern,
        output
    );
}


const CHECK_UAF_CMD: &[&str] = &["check", "-f"];
const CHECK_MLEAK_CMD: &[&str] = &["check", "-m"];
const ANALYZE_ALIAS_CMD: &[&str] = &["analyze", "alias"];
const ANALYZE_ALIAS_MFP_CMD: &[&str] = &["analyze", "alias", "--strategy", "mfp"];
const ANALYZE_OWNED_HEAP_CMD: &[&str] = &["analyze", "ownedheap"];
const ANALYZE_PATHS_CMD: &[&str] = &["analyze", "paths"];
const ANALYZE_PATHS_REPEAT1_CMD: &[&str] = &["analyze", "paths", "--postfix-repeat", "1"];
const ANALYZE_PATHS_REPEAT2_CMD: &[&str] = &["analyze", "paths", "--postfix-repeat", "2"];
const ANALYZE_SAFETYFLOW_CMD: &[&str] = &["analyze", "safetyflow"];
const ANALYZE_SSA_CMD: &[&str] = &["analyze", "ssa"];
const ANALYZE_RANGE_CMD: &[&str] = &["analyze", "range"];
const ANALYZE_CALLGRAPH_CMD: &[&str] = &["analyze", "callgraph"];
const ANALYZE_ADG_CMD: &[&str] = &["analyze", "adg", "--dump", "api_graph.yml"];
const VERIFY_CMD: &[&str] = &["verify"];
const VERIFY_PREPARE_CMD: &[&str] = &["verify", "--prepare-targets"];
const VERIFY_ALLOW_REPEAT_CMD: &[&str] = &["verify", "--postfix-repeat", "1"];
const VERIFY_ALLOW_REPEAT2_CMD: &[&str] = &["verify", "--postfix-repeat", "2"];
const VERIFY_SCAN_CMD: &[&str] = &["verify", "--mode", "scan"];
const VERIFY_INVLESS_CMD: &[&str] = &["verify", "--mode", "invless"];

// ================Dangling Pointer Detection Test=====================
#[test]
fn uaf_1() {
    let output = run_with_args("check/uaf_1", CHECK_UAF_CMD);
    assert_contain(
        &output,
        "Dangling pointer detected in function \"create_vec\"",
    );
}

#[test]
fn uaf_2() {
    let output = run_with_args("check/uaf_2", CHECK_UAF_CMD);
    assert_contain(&output, "Double free detected in function \"main\"");
}

#[test]
fn uaf_3() {
    let output = run_with_args("check/uaf_3", CHECK_UAF_CMD);
    assert_contain(&output, "Double free detected");
}

/*
#[test]
fn uaf_4() {
    let output = run_with_args("check/uaf_4", CHECK_UAF_CMD);
    assert_contain(&output, "Dangling pointer detected in function \"call\"");
}
*/

#[test]
fn uaf_5() {
    let output = run_with_args("check/uaf_5", CHECK_UAF_CMD);
    assert_contain(&output, "Use-after-free detected in function \"main\"");
}

#[test]
fn uaf_6() {
    let output = run_with_args("check/uaf_6", CHECK_UAF_CMD);
    assert_contain(&output, "Use-after-free detected in function \"main\"");
}

#[test]
fn uaf_7() {
    let output = run_with_args("check/uaf_7", CHECK_UAF_CMD);
    assert_contain(&output, "Double free detected in function \"main\"");
}

#[test]
fn uaf_8() {
    let output = run_with_args("check/uaf_8", CHECK_UAF_CMD);
    assert_contain(&output, "Use-after-free detected in function \"main\"");
}

#[test]
fn uaf_9() {
    let output = run_with_args("check/uaf_9", CHECK_UAF_CMD);
    assert_contain(&output, "Use-after-free detected in function \"main\"");
}

#[test]
fn uaf_10() {
    let output = run_with_args("check/uaf_10", CHECK_UAF_CMD);
    assert_contain(&output, "Double free detected in function \"evil_test\"");
}

#[test]
fn uaf_false_1() {
    let output = run_with_args("check/uaf_false_1", CHECK_UAF_CMD);
    assert!(
        !detected_high_confidence(&output),
        "Unexpected high-confidence bug in output:\n{}",
        output
    );
}

#[test]
fn uaf_false_2() {
    let output = run_with_args("check/uaf_false_2", CHECK_UAF_CMD);
    assert_not_contain(&output, "detected");
}

#[test]
fn uaf_false_3() {
    let output = run_with_args("check/uaf_false_3", CHECK_UAF_CMD);
    assert!(
        !detected_high_confidence(&output),
        "Unexpected high-confidence bug in output:\n{}",
        output
    );
}

#[test]
fn uaf_false_4() {
    let output = run_with_args("check/uaf_false_4", CHECK_UAF_CMD);
    assert_not_contain(&output, "detected");
}

#[test]
fn uaf_false_5() {
    #[allow(unused)]
    let output = run_with_args("check/uaf_false_5", CHECK_UAF_CMD);
    assert_not_contain(&output, "detected");
}

#[test]
fn uaf_false_6() {
    #[allow(unused)]
    let output = run_with_args("check/uaf_false_6", CHECK_UAF_CMD);
    assert!(
        !detected_high_confidence(&output),
        "Unexpected high-confidence bug in output:\n{}",
        output
    );
}

#[test]
fn uaf_false_8() {
    #[allow(unused)]
    let output = run_with_args("check/uaf_false_8", CHECK_UAF_CMD);
    assert_not_contain(&output, "detected");
}

#[test]
fn uaf_false_9() {
    #[allow(unused)]
    let output = run_with_args("check/uaf_false_9", CHECK_UAF_CMD);
    assert_not_contain(&output, "detected");
}

#[test]
fn uaf_false_10() {
    #[allow(unused)]
    let output = run_with_args("check/uaf_false_10", CHECK_UAF_CMD);
    assert_not_contain(&output, "detected");
}

#[test]
fn uaf_false_11() {
    #[allow(unused)]
    let output = run_with_args("check/uaf_false_11", CHECK_UAF_CMD);
    assert_not_contain(&output, "detected");
}

// ===============Alias(MOP) Analysis Test==============
#[test]
fn alias_1() {
    let output = run_with_args("analyze/alias_1", ANALYZE_ALIAS_CMD);
    assert_contain(&output, "foo\": (0.0,1)");
}

#[test]
fn alias_2() {
    let output = run_with_args("analyze/alias_2", ANALYZE_ALIAS_CMD);
    assert_contain(&output, "foo\": (0,1)");
}

#[test]
fn alias_3() {
    let output = run_with_args("analyze/alias_3", ANALYZE_ALIAS_CMD);
    assert_contain(&output, "foo\": null");
}

#[test]
fn alias_4() {
    let output = run_with_args("analyze/alias_4", ANALYZE_ALIAS_CMD);
    let has_either = output.contains("\"foo\": (0,1.1), (0,1.0)")
        || output.contains("\"foo\": (0,1.0), (0,1.1)");
    assert!(
        has_either,
        "Missing alias field variations\nFull output:\n{}",
        output
    );
}

#[test]
fn alias_5() {
    let output = run_with_args("analyze/alias_5", ANALYZE_ALIAS_CMD);
    assert_contain(&output, "new\": (0.0,1.0)");
}

#[test]
fn alias_6() {
    let output = run_with_args("analyze/alias_6", ANALYZE_ALIAS_CMD);
    assert_contain(&output, "foo\": (0,1)");
}

#[test]
fn alias_7() {
    let output = run_with_args("analyze/alias_7", ANALYZE_ALIAS_CMD);
    assert_contain(&output, "foo\": (0,1)");
}

#[test]
fn alias_8() {
    let output = run_with_args("analyze/alias_8", ANALYZE_ALIAS_CMD);
    assert_contain(&output, "foo\": (0,1), (0,2)");
}

#[test]
fn alias_9() {
    let output = run_with_args("analyze/alias_9", ANALYZE_ALIAS_CMD);
    assert_contain(&output, "foo\": (0,1)");
}

#[test]
fn alias_10() {
    let output = run_with_args("analyze/alias_10", ANALYZE_ALIAS_CMD);
    assert_contain(&output, "new\": (0.0,1.0)");
}

#[test]
fn alias_11() {
    let output = run_with_args("analyze/alias_11", ANALYZE_ALIAS_CMD);
    assert_contain(&output, "iter_prop\": (0.0,1.0)");
}

// ===============Alias(MFP) Analysis Test==============
#[test]
fn alias_1_mfp() {
    let output = run_with_args("analyze/alias_1", ANALYZE_ALIAS_MFP_CMD);
    assert_contain(&output, "foo\": (0.0,1)");
}

#[test]
fn alias_2_mfp() {
    let output = run_with_args("analyze/alias_2", ANALYZE_ALIAS_MFP_CMD);
    // MOP expects "foo": (0,1) but MFP reports a slightly different format.
    assert_contain(&output, "foo\": (0.0,1)"); // This is slightly different from MOP
}

#[test]
fn alias_3_mfp() {
    let output = run_with_args("analyze/alias_3", ANALYZE_ALIAS_MFP_CMD);
    assert_contain(&output, "foo\": null");
}

#[test]
fn alias_4_mfp() {
    let output = run_with_args("analyze/alias_4", ANALYZE_ALIAS_MFP_CMD);
    let has_either = output.contains("\"foo\": (0,1.1), (0,1.0)")
        || output.contains("\"foo\": (0,1.0), (0,1.1)");
    assert!(
        has_either,
        "Missing alias field variations\nFull output:\n{}",
        output
    );
}

#[test]
fn alias_5_mfp() {
    let output = run_with_args("analyze/alias_5", ANALYZE_ALIAS_MFP_CMD);
    assert_contain(&output, "new\": (0.0,1.0)");
}

#[test]
fn alias_6_mfp() {
    let output = run_with_args("analyze/alias_6", ANALYZE_ALIAS_MFP_CMD);
    assert_contain(&output, "foo\": (0,1)");
}

#[test]
fn alias_7_mfp() {
    let output = run_with_args("analyze/alias_7", ANALYZE_ALIAS_MFP_CMD);
    assert_contain(&output, "foo\": (0,1)");
}

#[test]
fn alias_8_mfp() {
    let output = run_with_args("analyze/alias_8", ANALYZE_ALIAS_MFP_CMD);
    assert_contain(&output, "foo\": (0,1), (0,2)");
}

#[test]
fn alias_9_mfp() {
    let output = run_with_args("analyze/alias_9", ANALYZE_ALIAS_MFP_CMD);
    assert_contain(&output, "foo\": (0,1)");
}

#[test]
fn alias_10_mfp() {
    let output = run_with_args("analyze/alias_10", ANALYZE_ALIAS_MFP_CMD);
    assert_contain(&output, "new\": (0.0,1.0)");
}

#[test]
fn alias_11_mfp() {
    let output = run_with_args("analyze/alias_11", ANALYZE_ALIAS_MFP_CMD);
    assert_contain(&output, "iter_prop\": (0.0,1.0)");
}

#[test]
fn leak_1() {
    let output = run_with_args("check/memleak_1", CHECK_MLEAK_CMD);
    assert_not_contain(&output, "Memory Leak detected in function main");
}

#[test]
fn leak_2() {
    let output = run_with_args("check/memleak_2", CHECK_MLEAK_CMD);
    assert_contain(&output, "Memory Leak detected in function main");
}

#[test]
fn leak_2_timeout() {
    let mut args = Vec::from(["--timeout", "0"]);
    args.extend(CHECK_MLEAK_CMD);
    let output = run_with_args("check/memleak_2", &args);
    assert!(output.contains("Process killed due to timeout"));
}

#[test]
fn leak_3() {
    let output = run_with_args("check/memleak_3", CHECK_MLEAK_CMD);
    assert_contain(&output, "Memory Leak detected in function main");
}

#[test]
fn heap_cell() {
    let output = run_with_args("analyze/ownedheap_cell", ANALYZE_OWNED_HEAP_CMD);
    for pattern in [
        "Cell\": False, <1>",
        "RefCell\": False, <1>",
        "UnsafeCell\": False, <1>",
        "Rc\": True, <1,1>",
        "Arc\": True, <1,1>",
        "UniqueRc\": True, <1,1>",
    ] {
        assert_contain(&output, pattern);
    }
}

#[test]
fn heap_collections() {
    let output = run_with_args("analyze/ownedheap_collections", ANALYZE_OWNED_HEAP_CMD);
    for pattern in [
        "Unique\": True, <0>",
        "Box\": True, <0,1>",
        "Vec\": True, <0,1>",
        "String\": True, <>",
        "LinkedList\": True, <1,1>",
    ] {
        assert_contain(&output, pattern);
    }
    #[cfg(rapx_rustc_ge_196)]
    {
        assert_contain(&output, "HashMap\": True, <0,0,1,1>");
        assert_contain(&output, "HashSet\": True, <0,1,1>");
        assert_contain(&output, "BTreeMap\": True, <0,0,1>");
        assert_contain(&output, "BTreeSet\": True, <0,1>");
    }
    #[cfg(not(rapx_rustc_ge_196))]
    {
        assert_contain(&output, "HashMap\": True, <0,0,1>");
        assert_contain(&output, "HashSet\": True, <0,1>");
        assert_contain(&output, "BTreeMap\": True, <0,0,1>");
        assert_contain(&output, "BTreeSet\": True, <0,1>");
    }
}

#[test]
fn heap_nested() {
    let output: String = run_with_args("analyze/ownedheap_nested", ANALYZE_OWNED_HEAP_CMD);
    for pattern in [
        "X\": False, <1>",
        "Y\": False, <1>",
        "Example\": True, <1,1,0,1>",
    ] {
        assert_contain(&output, pattern);
    }
}

#[test]
fn heap_proxy() {
    let output = run_with_args("analyze/ownedheap_proxy", ANALYZE_OWNED_HEAP_CMD);
    for pattern in [
        "Proxy1\": False, <0>",
        "Proxy2\": True, <0>",
        "Proxy3\": False, <0,0>",
        "Proxy4\": False, <1>",
        "Proxy5\": True, <0>",
    ] {
        assert_contain(&output, pattern);
    }
}

#[test]
fn path_1() {
    let output = run_with_args("analyze/path_1", ANALYZE_PATHS_CMD);
    assert_contain(&output, "Function: \"example\":");
    // 2 paths — reachability filtering prunes crossed enum branches
    assert_contain(&output, "Path [0, 3, 4, 6, 7, 9]");
    assert_contain(&output, "Path [0, 2, 4, 5, 8, 9]");
    assert_eq!(path_count_for(&output, "example"), 2);
}

#[test]
fn path_2() {
    let output = run_with_args("analyze/path_2", ANALYZE_PATHS_CMD);
    assert_contain(&output, "Function: \"read2\":");
    // 3 paths — direct + ManuallyDrop branch (block 12 is cleanup)
    assert_contain(&output, "Path [0, 1, 2, 3, 10, 11]");
    assert_contain(&output, "Path [0, 1, 2, 4, 5, 6, 7, 8, 9, 10, 11]");
    assert_contain(&output, "Path [0, 1, 2, 4, 5, 6, 12*]");
    assert_eq!(path_count_for(&output, "read2"), 3);
}

#[test]
fn path_3() {
    let output = run_with_args("analyze/path_3", ANALYZE_PATHS_CMD);
    assert_contain(&output, "Function: \"retry_once\":");
    assert_contain(&output, "Path [0, 1, 2, 1, 3]");
    assert_eq!(path_count_for(&output, "retry_once"), 1);
}

#[test]
fn path_4() {
    let output = run_with_args("analyze/path_4", ANALYZE_PATHS_CMD);
    assert_contain(&output, "Function: \"read1\":");
    assert_contain(&output, "Path [0, 1, 2, 6]");
    assert_contain(&output, "Path [0, 1, 3, 4, 1, 3, 5, 6]");
    assert_eq!(path_count_for(&output, "read1"), 2);
}

#[test]
fn path_5() {
    let output = run_with_args("analyze/path_5", ANALYZE_PATHS_CMD);
    assert_contain(&output, "Function: \"read2\":");
    assert_contain(&output, "Path [0, 1, 2, 3, 9]");
    assert_eq!(path_count_for(&output, "read2"), 2);
}

#[test]
fn path_false_1() {
    let output = run_with_args("analyze/path_false_1", ANALYZE_PATHS_CMD);
    assert_contain(&output, "Function: \"classify\":");
    // 9 paths — SCC with if-else branches
    assert_contain(&output, "Path [0, 1, 2]");
    assert_contain(&output, "Path [0, 1, 3, 4, 5, 6, 7, 10, 1, 2]");
    assert_contain(&output, "Path [0, 1, 3, 4, 5, 8, 9, 10, 1, 2]");
    assert_eq!(path_count_for(&output, "classify"), 9);
}

#[test]
fn path_6() {
    let output = run_with_args("analyze/path_6", ANALYZE_PATHS_CMD);
    assert_contain(&output, "Function: \"early_exit\":");
    // 2 paths — loop with return: zero-iter, one-iter
    assert_contain(&output, "Path [0, 1, 2]");
    assert_contain(&output, "Path [0, 1, 3, 4, 1, 2]");
    assert_eq!(path_count_for(&output, "early_exit"), 2);
}

#[test]
fn path_7() {
    let output = run_with_args("analyze/path_7", ANALYZE_PATHS_CMD);
    assert_contain(&output, "Function: \"walk\":");
    // 4 paths — nested SCC
    assert_contain(&output, "Path [0, 1, 2]");
    assert_contain(&output, "Path [0, 1, 3, 4, 5, 9, 1, 2]");
    assert_contain(&output, "Path [0, 1, 3, 4, 6, 7, 8, 4, 5, 9, 1, 2]");
    assert_contain(
        &output,
        "Path [0, 1, 3, 4, 6, 7, 8, 4, 5, 9, 1, 3, 4, 5, 9, 1, 2]",
    );
    assert_eq!(path_count_for(&output, "walk"), 4);
}

#[test]
fn scc_repeat1() {
    let output = run_with_args("analyze/path_false_1", ANALYZE_PATHS_REPEAT1_CMD);
    // postfix_repeat=1: 39 paths vs 11 at repeat=0
    assert_eq!(path_count_for(&output, "classify"), 39);
    assert_contain(&output, "Path [0, 1, 2]");
}

#[test]
fn scc_repeat2() {
    let output = run_with_args("analyze/path_false_1", ANALYZE_PATHS_REPEAT2_CMD);
    // postfix_repeat=2: 128 paths vs 11 at repeat=0
    assert_eq!(path_count_for(&output, "classify"), 128);
    assert_contain(&output, "Path [0, 1, 2]");
}

#[test]
fn align_sound_1() {
    let output = run_with_args("verify/align_sound_1", VERIFY_CMD);
    assert_contain(&output, "function: sound_named_contract_binds_callsite_arg");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_sound_2() {
    let output = run_with_args("verify/align_sound_2", VERIFY_CMD);
    assert_contain(&output, "function: sound_enum_paths_inside_scc");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_1() {
    let output = run_with_args("verify/align_unsound_1", VERIFY_CMD);
    assert_contain(&output, "function: unsound_enum_paths_inside_scc");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_sound_3() {
    let output = run_with_args("verify/align_sound_3", VERIFY_CMD);
    assert_contain(&output, "function: sound_scc_selects_aligned_source");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_2() {
    let output = run_with_args("verify/align_unsound_2", VERIFY_CMD);
    assert_contain(&output, "function: unsound_scc_selects_mixed_source");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_sound_4() {
    let output = run_with_args("verify/align_sound_4", VERIFY_CMD);
    assert_contain(&output, "function: sound_scc_computes_aligned_offset");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_3() {
    let output = run_with_args("verify/align_unsound_3", VERIFY_CMD);
    assert_contain(&output, "function: unsound_scc_computes_misaligned_offset");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_sound_5() {
    let output = run_with_args("verify/align_sound_5", VERIFY_CMD);
    assert_contain(&output, "function: sound_nested_scc_controller");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_4() {
    let output = run_with_args("verify/align_unsound_4", VERIFY_ALLOW_REPEAT_CMD);
    assert_contain(&output, "function: unsound_nested_scc_controller");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_sound_6() {
    let output = run_with_args("verify/align_sound_6", VERIFY_CMD);
    assert_contain(
        &output,
        "function: sound_iteration_count_switches_aligned_offsets",
    );
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_5() {
    let output = run_with_args("verify/align_unsound_5", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_iteration_count_can_leave_unaligned",
    );
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_sound_7() {
    let output = run_with_args("verify/align_sound_7", VERIFY_CMD);
    assert_contain(
        &output,
        "function: sound_unrelated_scc_does_not_pollute_align",
    );
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_sound_8() {
    let output = run_with_args("verify/align_sound_8", VERIFY_CMD);
    assert_contain(
        &output,
        "function: sound_unrelated_nested_scc_with_bad_scratch",
    );
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_sound_9() {
    let output = run_with_args("verify/align_sound_9", VERIFY_CMD);
    assert_contain(&output, "function: sound_pre_scc_guard_with_scc_offsets");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_6() {
    let output = run_with_args("verify/align_unsound_6", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_pre_scc_guard_overwritten_by_scc",
    );
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_sound_10() {
    let output = run_with_args("verify/align_sound_10", VERIFY_CMD);
    assert_contain(&output, "function: sound_scc_internal_noise_ignored");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_7() {
    let output = run_with_args("verify/align_unsound_7", VERIFY_CMD);
    assert_contain(&output, "function: unsound_scc_guard_only_on_one_branch");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_sound_11() {
    let output = run_with_args("verify/align_sound_11", VERIFY_CMD);
    assert_contain(&output, "function: sound_helper_with_conjunctive_guard");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_8() {
    let output = run_with_args("verify/align_unsound_8", VERIFY_CMD);
    assert_contain(&output, "function: unsound_helper_with_disjunctive_guard");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_sound_12() {
    let output = run_with_args("verify/align_sound_12", VERIFY_CMD);
    assert_contain(&output, "function: sound_nested_if_before_helper");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_9() {
    let output = run_with_args("verify/align_unsound_9", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_helper_return_path_selects_bad_ptr",
    );
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_sound_13() {
    let output = run_with_args("verify/align_sound_13", VERIFY_CMD);
    assert_contain(&output, "function: sound_helper_return_paths_all_aligned");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_sound_14() {
    let output = run_with_args("verify/align_sound_14", VERIFY_CMD);
    assert_contain(&output, "function: sound_multi_hop_helper");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_10() {
    let output = run_with_args("verify/align_unsound_10", VERIFY_CMD);
    assert_contain(&output, "function: unsound_multi_hop_missing_offset_guard");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_sound_15() {
    let output = run_with_args("verify/align_sound_15", VERIFY_CMD);
    assert_contain(&output, "function: sound_unrelated_condition_ignored");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_sound_16() {
    let output = run_with_args("verify/align_sound_16", VERIFY_CMD);
    assert_contain(&output, "function: sound_add_sub_chain");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_11() {
    let output = run_with_args("verify/align_unsound_11", VERIFY_CMD);
    assert_contain(&output, "function: unsound_sub_missing_guard");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_sound_17() {
    let output = run_with_args("verify/align_sound_17", VERIFY_CMD);
    assert_contain(&output, "function: sound_offset_zero_preserves_align");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_12() {
    let output = run_with_args("verify/align_unsound_12", VERIFY_CMD);
    assert_contain(&output, "function: unsound_byte_offset_one");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_sound_18() {
    let output = run_with_args("verify/align_sound_18", VERIFY_CMD);
    assert_contain(&output, "function: sound_usize_round_trip");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_sound_19() {
    let output = run_with_args("verify/align_sound_19", VERIFY_CMD);
    assert_contain(&output, "function: sound_usize_add_guarded");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_13() {
    let output = run_with_args("verify/align_unsound_13", VERIFY_CMD);
    assert_contain(&output, "function: unsound_usize_add_missing_offset_guard");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_sound_20() {
    let output = run_with_args("verify/align_sound_20", VERIFY_CMD);
    assert_contain(&output, "function: sound_usize_mul_div_offset");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_sound_21() {
    let output = run_with_args("verify/align_sound_21", VERIFY_CMD);
    assert_contain(&output, "function: sound_repr_c_field");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_sound_22() {
    let output = run_with_args("verify/align_sound_22", VERIFY_CMD);
    assert_contain(&output, "function: sound_repr_align_object");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_14() {
    let output = run_with_args("verify/align_unsound_14", VERIFY_CMD);
    assert_contain(&output, "function: unsound_repr_packed_field");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_sound_23() {
    let output = run_with_args("verify/align_sound_23", VERIFY_CMD);
    assert_contain(&output, "function: sound_zst_trivial_alignment");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_15() {
    let output = run_with_args("verify/align_unsound_15", VERIFY_CMD);
    assert_contain(&output, "function: unsound_four_phase_scc_alignment");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_unsound_16() {
    let output = run_with_args("verify/align_unsound_16", VERIFY_CMD);
    assert_contain(&output, "function: unsound_trait_bound_cross_cast");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_sound_24() {
    let output = run_with_args("verify/align_sound_24", VERIFY_CMD);
    assert_contain(&output, "function: sound_trait_bound_cross_cast");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_sound_25() {
    let output = run_with_args("verify/align_sound_25", VERIFY_CMD);
    assert_contain(
        &output,
        "function: sound_contract_type_param_binds_concrete",
    );
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_sound_26() {
    let output = run_with_args("verify/align_sound_26", VERIFY_CMD);
    assert_contain(&output, "function: sound_contract_type_param_binds_generic");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_unsound_17() {
    let output = run_with_args("verify/align_unsound_17", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_contract_type_param_binds_generic",
    );
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn align_repeat_threshold_repeat1_sound() {
    let output = run_with_args("verify/align_repeat_threshold", VERIFY_ALLOW_REPEAT_CMD);
    assert_contain(&output, "function: repeat2_reveals_delayed_unaligned");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn align_repeat_threshold_repeat2_unsound() {
    let output = run_with_args("verify/align_repeat_threshold", VERIFY_ALLOW_REPEAT2_CMD);
    assert_contain(&output, "function: repeat2_reveals_delayed_unaligned");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn nonnull_sound_7() {
    let output = run_with_args("verify/nonnull_sound_7", VERIFY_CMD);
    assert_contain(&output, "function: sound_ref_cast_copy_chain");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn nonnull_sound_2() {
    let output = run_with_args("verify/nonnull_sound_2", VERIFY_CMD);
    assert_contain(&output, "function: sound_slice_as_ptr_branch");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn nonnull_sound_3() {
    let output = run_with_args("verify/nonnull_sound_3", VERIFY_CMD);
    assert_contain(&output, "function: sound_intra_helper_from_ref");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn nonnull_sound_4() {
    let output = run_with_args("verify/nonnull_sound_4", VERIFY_CMD);
    assert_contain(&output, "function: sound_scc_unrelated_state");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn nonnull_sound_5() {
    let output = run_with_args("verify/nonnull_sound_5", VERIFY_CMD);
    assert_contain(&output, "function: sound_raw_arg_guarded");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn nonnull_sound_6() {
    let output = run_with_args("verify/nonnull_sound_6", VERIFY_CMD);
    assert_contain(&output, "function: sound_nonnull_wrapper_from_ref");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn nonnull_unsound_1() {
    let output = run_with_args("verify/nonnull_unsound_1", VERIFY_CMD);
    assert_contain(&output, "function: unsound_explicit_null_constant");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn nonnull_unsound_2() {
    let output = run_with_args("verify/nonnull_unsound_2", VERIFY_CMD);
    assert_contain(&output, "function: unsound_raw_pointer_argument");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn nonnull_unsound_3() {
    let output = run_with_args("verify/nonnull_unsound_3", VERIFY_CMD);
    assert_contain(&output, "function: unsound_branch_selects_null");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn nonnull_unsound_4() {
    let output = run_with_args("verify/nonnull_unsound_4", VERIFY_CMD);
    assert_contain(&output, "function: unsound_scc_overwrites_with_null");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn nonnull_unsound_5() {
    let output = run_with_args("verify/nonnull_unsound_5", VERIFY_CMD);
    assert_contain(&output, "function: unsound_unrelated_guard");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn nonnull_unsound_6() {
    let output = run_with_args("verify/nonnull_unsound_6", VERIFY_CMD);
    assert_contain(&output, "function: unsound_nonnull_wrapper_from_null");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn allocated_sound_1() {
    let output = run_with_args("verify/allocated_sound_1", VERIFY_CMD);
    assert_contain(&output, "function: sound_stack_local_allocated");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn allocated_sound_2() {
    let output = run_with_args("verify/allocated_sound_2", VERIFY_CMD);
    assert_contain(&output, "function: sound_slice_prefix_allocated");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn allocated_sound_3() {
    let output = run_with_args("verify/allocated_sound_3", VERIFY_CMD);
    assert_contain(&output, "function: sound_live_vec_allocated");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn allocated_sound_4() {
    let output = run_with_args("verify/allocated_sound_4", VERIFY_CMD);
    assert_contain(&output, "function: sound_live_box_allocated");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn allocated_sound_5() {
    let output = run_with_args("verify/allocated_sound_5", VERIFY_CMD);
    assert_contain(&output, "function: sound_branch_selects_live_local");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn allocated_sound_6() {
    let output = run_with_args("verify/allocated_sound_6", VERIFY_CMD);
    assert_contain(&output, "function: sound_loop_slice_element_allocated");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn allocated_sound_7() {
    let output = run_with_args("verify/allocated_sound_7", VERIFY_CMD);
    assert_contain(&output, "function: sound_scc_selects_live_array");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn allocated_sound_8() {
    let output = run_with_args("verify/allocated_sound_8", VERIFY_CMD);
    assert_contain(&output, "function: sound_intra_returns_slice_pointer");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn allocated_unsound_1() {
    let output = run_with_args("verify/allocated_unsound_1", VERIFY_CMD);
    assert_contain(&output, "function: unsound_null_not_allocated");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn allocated_unsound_2() {
    let output = run_with_args("verify/allocated_unsound_2", VERIFY_CMD);
    assert_contain(&output, "function: unsound_stack_scope_ended");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn allocated_unsound_3() {
    let output = run_with_args("verify/allocated_unsound_3", VERIFY_CMD);
    assert_contain(&output, "function: unsound_vec_dropped_before_use");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn allocated_unsound_4() {
    let output = run_with_args("verify/allocated_unsound_4", VERIFY_CMD);
    assert_contain(&output, "function: unsound_empty_slice_needs_one_element");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn allocated_unsound_5() {
    let output = run_with_args("verify/allocated_unsound_5", VERIFY_CMD);
    assert_contain(&output, "function: unsound_branch_may_select_null");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn allocated_unsound_6() {
    let output = run_with_args("verify/allocated_unsound_6", VERIFY_CMD);
    assert_contain(&output, "function: unsound_scc_overwrites_with_null");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn allocated_unsound_7() {
    let output = run_with_args("verify/allocated_unsound_7", VERIFY_CMD);
    assert_contain(&output, "function: unsound_vec_reallocates_old_pointer");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn allocated_unsound_8() {
    let output = run_with_args("verify/allocated_unsound_8", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_slice_too_short_for_requested_len",
    );
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn allocated_unsound_9() {
    let output = run_with_args("verify/allocated_unsound_9", VERIFY_CMD);
    assert_contain(&output, "function: unsound_intra_returns_dangling_pointer");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn allocated_unsound_10() {
    let output = run_with_args("verify/allocated_unsound_10", VERIFY_CMD);
    assert_contain(&output, "function: unsound_scc_selects_dead_temporary");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn allocated_unsound_11() {
    let output = run_with_args("verify/allocated_unsound_11", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_adjacent_stack_objects_do_not_merge",
    );
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn inbound_sound_1() {
    let output = run_with_args("verify/inbound_sound_1", VERIFY_CMD);
    assert_contain(&output, "function: sound_ptr_add_guarded");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn inbound_unsound_1() {
    let output = run_with_args("verify/inbound_unsound_1", VERIFY_CMD);
    assert_contain(&output, "function: unsound_ptr_add_without_guard");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn inbound_sound_2() {
    let output = run_with_args("verify/inbound_sound_2", VERIFY_CMD);
    assert_contain(&output, "function: sound_from_raw_parts_prefix_two");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn inbound_unsound_2() {
    let output = run_with_args("verify/inbound_unsound_2", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_from_raw_parts_two_only_nonempty",
    );
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn inbound_sound_3() {
    let output = run_with_args("verify/inbound_sound_3", VERIFY_CMD);
    assert_contain(&output, "function: sound_get_unchecked_generic");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn inbound_unsound_3() {
    let output = run_with_args("verify/inbound_unsound_3", VERIFY_CMD);
    assert_contain(&output, "function: unsound_get_unchecked_wrong_guard");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn inbound_sound_4() {
    let output = run_with_args("verify/inbound_sound_4", VERIFY_CMD);
    assert_contain(&output, "function: sound_copy_nonoverlapping_one");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn inbound_unsound_4() {
    let output = run_with_args("verify/inbound_unsound_4", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_copy_nonoverlapping_dst_unguarded",
    );
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn inbound_sound_5() {
    let output = run_with_args("verify/inbound_sound_5", VERIFY_CMD);
    assert_contain(&output, "function: sound_intra_slice_add_guarded");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn inbound_unsound_5() {
    let output = run_with_args("verify/inbound_unsound_5", VERIFY_CMD);
    assert_contain(&output, "function: unsound_branch_selects_unguarded_index");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn inbound_unsound_6() {
    let output = run_with_args("verify/inbound_unsound_6", VERIFY_CMD);
    assert_contain(&output, "function: unsound_scc_off_by_one");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn inbound_unsound_7() {
    let output = run_with_args("verify/inbound_unsound_7", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_inclusive_range_off_by_one",
    );
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn inbound_sound_6() {
    let output = run_with_args("verify/inbound_sound_6", VERIFY_CMD);
    assert_contain(&output, "function: sound_scc_loop_index_guard");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn inbound_std_sound_1() {
    let output = run_with_args("verify/inbound_std_sound_1", VERIFY_CMD);
    assert_contain(&output, "function: sound_std_get_unchecked");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn inbound_std_unsound_1() {
    let output = run_with_args("verify/inbound_std_unsound_1", VERIFY_CMD);
    assert_contain(&output, "function: unsound_std_get_unchecked_wrong_guard");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn sliceindex_inbound_sound_1() {
    let output = run_with_args("verify/sliceindex_sound_01", VERIFY_CMD);
    assert_contain(&output, "function: sound_scalar_index_guard");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn sliceindex_inbound_unsound_1() {
    let output = run_with_args("verify/sliceindex_unsound_01", VERIFY_CMD);
    assert_contain(&output, "function: unsound_scalar_index_wrong_guard");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn sliceindex_inbound_sound_2() {
    let output = run_with_args("verify/sliceindex_sound_02", VERIFY_CMD);
    assert_contain(&output, "function: sound_range_index_guard");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn sliceindex_inbound_unsound_2() {
    let output = run_with_args("verify/sliceindex_unsound_02", VERIFY_CMD);
    assert_contain(&output, "function: unsound_range_index_missing_end_guard");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn sliceindex_inbound_std_sound_1() {
    let output = run_with_args("verify/sliceindex_sound_03", VERIFY_CMD);
    assert_contain(&output, "function: sound_std_get_unchecked_sliceindex");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn sliceindex_inbound_std_range_cases() {
    let output = run_with_args("verify/sliceindex_sound_04", VERIFY_CMD);
    assert_contain(&output, "function: sound_std_range_get_unchecked");
    assert_contain(&output, "result: SOUND");

    let output = run_with_args("verify/sliceindex_unsound_03", VERIFY_CMD);
    assert_contain(&output, "function: unsound_std_range_missing_end_guard");
    assert_contain(&output, "result: UNSOUND");
}

// FIXME: requires SMT improvements for variable-length ValidPtr and NonOverlap
// #[test]
// fn inbound_std_sound_2() {
//     let output = run_with_args("verify/inbound_std_sound_2", VERIFY_CMD);
//     assert_contain(&output, "function: sound_std_copy_nonoverlapping");
//     assert_contain(&output, "result: SOUND");
// }

#[test]
fn inbound_std_unsound_2() {
    let output = run_with_args("verify/inbound_std_unsound_2", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_std_copy_nonoverlapping_dst_unguarded",
    );
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn init_std_sound_1() {
    let output = run_with_args("verify/init_std_sound_1", VERIFY_CMD);
    assert_contain(&output, "function: sound_assume_init_read_after_write");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn init_std_sound_2() {
    let output = run_with_args("verify/init_std_sound_2", VERIFY_CMD);
    assert_contain(&output, "function: sound_assume_init_after_write");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn init_std_sound_3() {
    let output = run_with_args("verify/init_std_sound_3", VERIFY_CMD);
    assert_contain(&output, "function: sound_branch_local_init");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn init_std_sound_4() {
    let output = run_with_args("verify/init_std_sound_4", VERIFY_CMD);
    assert_contain(&output, "function: sound_intra_helper_initializes");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn init_std_sound_5() {
    let output = run_with_args("verify/init_std_sound_5", VERIFY_CMD);
    assert_contain(&output, "function: sound_loop_initializes_slice");
    assert_contain(&output, "Init | Proved");
}

#[test]
fn init_std_sound_6() {
    let output = run_with_args("verify/init_std_sound_6", VERIFY_CMD);
    assert_contain(&output, "function: sound_len_bound_loop_initializes_slice");
    assert_contain(&output, "Init | Proved");
}

#[test]
fn init_std_unsound_1() {
    let output = run_with_args("verify/init_std_unsound_1", VERIFY_CMD);
    assert_contain(&output, "function: unsound_assume_init_read_without_write");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn init_std_unsound_2() {
    let output = run_with_args("verify/init_std_unsound_2", VERIFY_CMD);
    assert_contain(&output, "function: unsound_assume_init_without_write");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn init_std_unsound_3() {
    let output = run_with_args("verify/init_std_unsound_3", VERIFY_CMD);
    assert_contain(&output, "function: unsound_conditional_write_then_assume");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn init_std_unsound_4() {
    let output = run_with_args("verify/init_std_unsound_4", VERIFY_CMD);
    assert_contain(&output, "function: unsound_write_different_slot");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn init_std_unsound_5() {
    let output = run_with_args("verify/init_std_unsound_5", VERIFY_CMD);
    assert_contain(&output, "function: unsound_intra_helper_maybe_initializes");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn init_std_unsound_6() {
    let output = run_with_args("verify/init_std_unsound_6", VERIFY_CMD);
    assert_contain(&output, "function: unsound_from_raw_parts_uninitialized");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn init_std_unsound_7() {
    let output = run_with_args("verify/init_std_unsound_7", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_from_raw_parts_wrong_element_type",
    );
    assert_contain(&output, "Init | Unknown");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn init_std_unsound_8() {
    let output = run_with_args("verify/init_std_unsound_8", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_len_bound_loop_skips_even_indices",
    );
    assert_contain(&output, "Init | Unknown");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn validnum_sound_1() {
    let output = run_with_args("verify/validnum_sound_1", VERIFY_CMD);
    assert_contain(&output, "function: sound_guarded_less_than");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn validnum_unsound_1() {
    let output = run_with_args("verify/validnum_unsound_1", VERIFY_CMD);
    assert_contain(&output, "function: unsound_missing_less_than_guard");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn validnum_sound_2() {
    let output = run_with_args("verify/validnum_sound_2", VERIFY_CMD);
    assert_contain(&output, "function: sound_guarded_nonzero");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn validnum_unsound_2() {
    let output = run_with_args("verify/validnum_unsound_2", VERIFY_CMD);
    assert_contain(&output, "function: unsound_missing_nonzero_guard");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn validnum_sound_3() {
    let output = run_with_args("verify/validnum_sound_3", VERIFY_CMD);
    assert_contain(&output, "function: sound_constant_sum_below_cap");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn validnum_unsound_3() {
    let output = run_with_args("verify/validnum_unsound_3", VERIFY_CMD);
    assert_contain(&output, "function: unsound_partial_sum_guard");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn validnum_sound_4() {
    let output = run_with_args("verify/validnum_sound_4", VERIFY_CMD);
    assert_contain(&output, "function: sound_trait_bound_size_limit");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn validnum_unsound_4() {
    let output = run_with_args("verify/validnum_unsound_4", VERIFY_CMD);
    assert_contain(&output, "function: unsound_trait_bound_missing_size_limit");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn validnum_sound_5() {
    let output = run_with_args("verify/validnum_sound_5", VERIFY_CMD);
    assert_contain(&output, "function: sound_scc_validnum_index_guard");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn validnum_sound_6() {
    let output = run_with_args("verify/validnum_sound_6", VERIFY_CMD);
    assert_contain(&output, "function: sound_guarded_variable_sum");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn validnum_sound_7() {
    let output = run_with_args("verify/validnum_sound_7", VERIFY_CMD);
    assert_contain(&output, "function: sound_interval_guard");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn validnum_unsound_5() {
    let output = run_with_args("verify/validnum_unsound_5", VERIFY_CMD);
    assert_contain(&output, "function: unsound_interval_inclusive_guard");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn validnum_sound_8() {
    let output = run_with_args("verify/validnum_sound_8", VERIFY_CMD);
    assert_contain(&output, "function: sound_trait_bound_align_order");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn validnum_std_sound_1() {
    let output = run_with_args("verify/validnum_std_sound_1", VERIFY_CMD);
    assert_contain(&output, "function: sound_std_from_raw_parts_validnum");
    assert_contain(&output, "ValidNum | Proved");
}

#[test]
fn validnum_std_unsound_1() {
    let output = run_with_args("verify/validnum_std_unsound_1", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_std_from_raw_parts_validnum_overflow",
    );
    assert_contain(&output, "ValidNum | Unknown");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn validnum_std_sound_2() {
    let output = run_with_args("verify/validnum_std_sound_2", VERIFY_CMD);
    assert_contain(&output, "function: sound_std_copy_nonoverlapping_validnum");
    assert_contain(&output, "ValidNum | Proved");
}

#[test]
fn validnum_std_unsound_2() {
    let output = run_with_args("verify/validnum_std_unsound_2", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_std_copy_nonoverlapping_validnum",
    );
    assert_contain(&output, "ValidNum | Unknown");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn as_chunks_unchecked_validnum_sound_1() {
    let output = run_with_args("verify/as_chunks_sound_01", VERIFY_CMD);
    assert_contain(&output, "function: sound_as_chunks_unchecked_exact_div");
    assert_contain(&output, "result: SOUND");
    assert_contain(&output, "function: sound_exact_div_guard");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn as_chunks_unchecked_validnum_unsound_1() {
    let output = run_with_args("verify/as_chunks_unsound_01", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_as_chunks_unchecked_missing_exact_div",
    );
    assert_contain(&output, "result: UNSOUND");
    assert_contain(&output, "function: unsound_exact_div_missing_guard");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn validptr_size_or_deref_sound_cases() {
    let output = run_with_args("verify/validptr_sound_1", VERIFY_CMD);
    assert_contain(&output, "function: sound_zst_dangling_valid_for_any_len");
    assert_contain(&output, "result: SOUND");

    let output = run_with_args("verify/validptr_sound_2", VERIFY_CMD);
    assert_contain(&output, "function: sound_stack_array_full_range");
    assert_contain(&output, "result: SOUND");

    let output = run_with_args("verify/validptr_sound_3", VERIFY_CMD);
    assert_contain(&output, "function: sound_slice_suffix_guarded");
    assert_contain(&output, "result: SOUND");

    let output = run_with_args("verify/validptr_sound_5", VERIFY_CMD);
    assert_contain(&output, "function: sound_signed_suffix_guarded");
    assert_contain(&output, "result: SOUND");

    let output = run_with_args("verify/validptr_sound_4", VERIFY_CMD);
    assert_contain(&output, "function: sound_scc_each_slice_element");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn validptr_size_or_deref_unsound_cases() {
    let output = run_with_args("verify/validptr_unsound_1", VERIFY_CMD);
    assert_contain(&output, "function: unsound_non_zst_dangling_not_allocated");
    assert_contain(&output, "result: UNSOUND");

    let output = run_with_args("verify/validptr_unsound_2", VERIFY_CMD);
    assert_contain(&output, "function: unsound_one_past_requires_one_element");
    assert_contain(&output, "result: UNSOUND");

    let output = run_with_args("verify/validptr_unsound_3", VERIFY_CMD);
    assert_contain(&output, "function: unsound_stack_array_len_too_large");
    assert_contain(&output, "result: UNSOUND");

    let output = run_with_args("verify/validptr_unsound_4", VERIFY_CMD);
    assert_contain(&output, "function: unsound_scc_branch_uses_one_past");
    assert_contain(&output, "result: UNSOUND");

    let output = run_with_args("verify/validptr_unsound_5", VERIFY_CMD);
    assert_contain(
        &output,
        "function: unsound_signed_suffix_missing_lower_bound",
    );
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn deref_allocated_and_inbound_cases() {
    let output = run_with_args("verify/deref_sound_1", VERIFY_CMD);
    assert_contain(&output, "function: sound_deref_slice_prefix");
    assert_contain(&output, "Deref | Proved");
    assert_contain(&output, "result: SOUND");

    let output = run_with_args("verify/deref_unsound_1", VERIFY_CMD);
    assert_contain(&output, "function: unsound_deref_one_past");
    assert_contain(&output, "Deref | Unknown");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn typed_provenance_cases() {
    let output = run_with_args("verify/typed_cases", VERIFY_CMD);

    for function in [
        "sound_reference_source",
        "sound_slice_element_source",
        "sound_repr_c_field_source",
        "sound_generic_reference_source",
        "sound_branch_all_sources_typed",
        "sound_scc_preserves_typed_source",
        "sound_maybeuninit_after_write",
        "sound_align_to_same_type",
    ] {
        assert_contain(&output, &format!("function: {function}"));
    }
    assert_contain(&output, "Typed | Proved");
    assert_contain(&output, "result: SOUND");

    for function in [
        "unsound_u8_bytes_as_u32",
        "unsound_u16_slice_as_u32",
        "unsound_uninit_memory_as_u32",
        "unsound_invalid_bool_bits",
        "unsound_invalid_char_bits",
        "unsound_invalid_enum_discriminant",
        "unsound_branch_selects_untyped_source",
        "unsound_scc_overwrites_with_untyped_source",
        "unsound_align_to_bool_from_bytes",
    ] {
        assert_contain(&output, &format!("function: {function}"));
    }
    assert_contain(&output, "Typed | Unknown");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn alive_lifetime_sound_cases() {
    let output = run_with_args("verify/alive_sound_01", VERIFY_CMD);
    assert_contain(&output, "function: SliceHost::<'a, T>::get");
    assert_contain(&output, "Alive | Proved");

    let output = run_with_args("verify/alive_sound_02", VERIFY_CMD);
    assert_contain(&output, "function: MutSliceHost::<'a, T>::get_mut");
    assert_contain(&output, "Alive | Proved");

    let output = run_with_args("verify/alive_sound_03", VERIFY_CMD);
    assert_contain(&output, "function: slice_from_host");
    assert_contain(&output, "Alive | Proved");
}

#[test]
fn alive_lifetime_unsound_cases() {
    let output = run_with_args("verify/alive_unsound_01", VERIFY_CMD);
    assert_contain(&output, "function: DangerousAliaser::<'a, T>::get_mut");
    assert_contain(&output, "Alive | Failed");
    assert_contain(&output, "result: UNSOUND");

    let output = run_with_args("verify/alive_unsound_02", VERIFY_CMD);
    assert_contain(&output, "function: slice_tied_to_unrelated_host");
    assert_contain(&output, "Alive | Failed");
    assert_contain(&output, "result: UNSOUND");

    let output = run_with_args("verify/alive_unsound_03", VERIFY_CMD);
    assert_contain(&output, "function: static_slice_from_local_vec");
    assert_contain(&output, "Alive | Failed");
    assert_contain(&output, "result: UNSOUND");
}

#[test]
fn struct_invariant_1() {
    let output = run_with_args("verify/struct_invariant_1", VERIFY_CMD);
    // unsound_new: constructor with requires, all struct invariants proved
    assert_contain(&output, "function: Wrapper::<T>::unsound_new");
    assert_contain(&output, "Align | Proved");
    assert_contain(&output, "InBound | Proved");
    assert_contain(&output, "Init | Proved");
    // unsound_set_len: mutator with requires, struct invariants proved via self
    assert_contain(&output, "function: Wrapper::<T>::unsound_set_len");
    // sound_read: alignment proved via guard, but raw-ptr deref still unproved
    assert_contain(&output, "function: Wrapper::<T>::sound_read");
    // unsound_read: raw-ptr deref unproved, struct invariants hold via precond
    assert_contain(&output, "function: Wrapper::<T>::unsound_read");
}

#[test]
fn invless_skips_struct_invariant() {
    let output = run_with_args("verify/struct_invariant_1", VERIFY_INVLESS_CMD);
    // 4 sequences: 2 read methods × 2 options (direct, through set_len)
    assert_contain(&output, "sequence: unsound_new -> sound_read");
    assert_contain(
        &output,
        "sequence: unsound_new -> unsound_set_len -> sound_read",
    );
    assert_contain(&output, "sequence: unsound_new -> unsound_read");
    assert_contain(
        &output,
        "sequence: unsound_new -> unsound_set_len -> unsound_read",
    );
    // All UNSOUND: ValidPtr/Typed unimplemented
    assert_contain(&output, "result: UNSOUND");
    assert_not_contain(&output, "result: SOUND");
    // sound_read Align proved via guard; unsound_read Align Unknown
    assert_contain(&output, "Align | Proved");
    assert_contain(&output, "Align | Unknown");
    assert_not_contain(&output, "function: Wrapper::<T>::unsound_new");
    assert_not_contain(&output, "function: Wrapper::<T>::unsound_set_len");
    assert_not_contain(&output, "struct-invariant");
}

#[test]
fn invless_1_no_annotations() {
    let output = run_with_args("verify/invless_1", VERIFY_INVLESS_CMD);
    // 4 sequences generated
    assert_contain(&output, "sequence: unsound_new -> sound_read");
    assert_contain(
        &output,
        "sequence: unsound_new -> unsound_set_len -> sound_read",
    );
    assert_contain(&output, "sequence: unsound_new -> unsound_read");
    assert_contain(
        &output,
        "sequence: unsound_new -> unsound_set_len -> unsound_read",
    );
    // sound_read: Align Proved (internal guard), ValidPtr/Typed Unknown → UNSOUND(2)
    // set_len→sound_read: same
    // unsound_read: Align Unknown (no contracts), ValidPtr/Typed Unknown → UNSOUND(3)
    // set_len→unsound_read: same
    assert_contain(&output, "result: UNSOUND");
    assert_not_contain(&output, "result: SOUND");
    assert_contain(&output, "Align | Proved");
    assert_contain(&output, "Align | Unknown");
    assert_not_contain(&output, "struct-invariant");
}

#[test]
fn invless_2_with_contracts() {
    let output = run_with_args("verify/invless_2", VERIFY_INVLESS_CMD);
    // 4 sequences generated
    assert_contain(&output, "sequence: unsound_new -> sound_read");
    assert_contain(
        &output,
        "sequence: unsound_new -> unsound_set_len -> sound_read",
    );
    assert_contain(&output, "sequence: unsound_new -> unsound_read");
    assert_contain(
        &output,
        "sequence: unsound_new -> unsound_set_len -> unsound_read",
    );
    // sound_read: Align Proved (guard), ValidPtr/Typed Unknown → UNSOUND(2)
    // set_len→sound_read: Align Proved (guard; set_len mutates len but Align depends only on ptr)
    // unsound_read: Align Unknown (contract Align(self.ptr, u32) not connected to casted ptr via SMT)
    // set_len→unsound_read: Align Unknown (same; set_len mutates len, Align not invalidated)
    assert_contain(&output, "result: UNSOUND");
    assert_not_contain(&output, "result: SOUND");
    assert_contain(&output, "Align | Proved");
    assert_contain(&output, "Align | Unknown");
    assert_contain(&output, "ValidPtr | Unknown");
    assert_contain(&output, "Typed | Unknown");
    assert_not_contain(&output, "struct-invariant");
}

#[test]
fn invless_sound_callee() {
    let output = run_with_args("verify/align_sound_1", VERIFY_INVLESS_CMD);
    assert_contain(&output, "function: sound_named_contract_binds_callsite_arg");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn safetyflow_safe_caller() {
    let output = run_with_args("analyze/safetyflow_safe_caller", ANALYZE_SAFETYFLOW_CMD);
    assert_contain(&output, "from_raw_parts");
}

#[test]
fn safetyflow_raw_ptr() {
    let output = run_with_args("analyze/safetyflow_raw_ptr", ANALYZE_SAFETYFLOW_CMD);
    assert_contain(&output, "*raw* ptr deref");
}

#[test]
fn safetyflow_static_mut() {
    let output = run_with_args("analyze/safetyflow_static_mut", ANALYZE_SAFETYFLOW_CMD);
    assert_contain(&output, "COUNTER");
}

#[test]
fn verify_raw_ptr_stack_local_sound() {
    let output = run_with_args("analyze/safetyflow_raw_ptr", VERIFY_SCAN_CMD);
    assert_contain(&output, "[rapx::verify] function: main");
    assert_contain(&output, "ValidPtr | Proved");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn verify_static_mut_unknown() {
    let output = run_with_args("analyze/safetyflow_static_mut", VERIFY_SCAN_CMD);
    assert_contain(&output, "[rapx::verify] function: main");
    assert_contain(&output, "Unknown");
    assert_contain(&output, "UNSOUND");
}

#[test]
fn verify_slice() {
    let output = run_with_args("verify/slice", VERIFY_CMD);

    let functions = [
        "<[T] as SliceExt<T>>::get_unchecked_ext",
        "<[T] as SliceExt<T>>::get_unchecked_mut_ext",
        "<[T] as SliceExt<T>>::split_at_unchecked_ext",
        "<[T] as SliceExt<T>>::split_at_mut_unchecked_ext",
        "<[T] as SliceExt<T>>::swap_unchecked_ext",
        "<[T] as SliceExt<T>>::as_chunks_unchecked_ext",
        "<[T] as SliceExt<T>>::as_chunks_unchecked_mut_ext",
        "<[T] as SliceExt<T>>::align_to_ext",
        "<[T] as SliceExt<T>>::align_to_mut_ext",
        "<[T] as SliceExt<T>>::get_disjoint_unchecked_mut_ext",
    ];

    for fn_name in &functions {
        assert_contain(&output, fn_name);
    }

    assert_eq!(
        output.matches("result: SOUND").count(),
        functions.len(),
        "expected {} SOUND results",
        functions.len()
    );
}

#[test]
fn trait_unsound_1() {
    let output = run_with_args("verify/trait_unsound_1", VERIFY_PREPARE_CMD);
    assert_contain(&output, "prepare targets for unsafe trait: Buffer");
    assert_contain(&output, "impl for: VecBuf");
    assert_contain(&output, "ensures");
    assert_contain(&output, "ValidSlice");
}

#[test]
fn trait_unsound_1_verify() {
    let output = run_with_args("verify/trait_unsound_1", VERIFY_CMD);
    assert_contain(&output, "unsafe trait impl: Buffer");
    assert_contain(&output, "impl for: VecBuf");
    assert_contain(&output, "ensures");
    assert_contain(&output, "ValidSlice");
    assert_contain(&output, "verification: deferred");
}

#[test]
fn ssa_transform() {
    let output = run_with_args("analyze/ssa_transform", ANALYZE_SSA_CMD);
    assert_contain(&output, "ssa lvalue check true");
}
#[test]
fn range_analysis() {
    let output = run_with_args("analyze/range_1", ANALYZE_RANGE_CMD);

    let expected_ranges = vec![
        "_1 => Regular [0, 0]",
        "_2 => Regular [Min, Max]",
        "_4 => Regular [0, 100]",
        "_6 => Regular [0, 99]",
        "_11 => Regular [1, 99]",
        "_12 => Regular [0, 98]",
        "_34 => Regular [1, 100]",
    ];

    for expected in expected_ranges {
        assert!(
            output.contains(expected),
            "Missing expected range: '{}'\nFull output:\n{}",
            expected,
            output
        );
    }
}

#[test]

fn interprocedual_range_analysis() {
    let output = run_with_args("analyze/range_2", ANALYZE_RANGE_CMD);

    let expected_ranges = vec![
        "_1 => Regular [42, 42]",
        "_2 => Regular [Min, Max]",
        "_4 => Regular [52, 52]",
        "_5 => Regular [100, 100]",
    ];

    for expected in expected_ranges {
        assert!(
            output.contains(expected),
            "Missing expected range: '{}'\nFull output:\n{}",
            expected,
            output
        );
    }
}

#[test]
fn callgraph_dynamic_dispatch() {
    let output = run_with_args("analyze/callgraph_dynamic", ANALYZE_CALLGRAPH_CMD);

    let expected_calls = vec!["-> <Dog as Animal>::speak", "-> <Cat as Animal>::speak"];

    for expected in expected_calls {
        assert!(
            output.contains(expected),
            "Missing dynamic call '{}'\nFull output:\n{}",
            expected,
            output
        );
    }
}

#[test]
fn symbolic_interval() {
    let output = run_with_args("analyze/range_symbolic", ANALYZE_RANGE_CMD);

    let expected_ranges = vec![
        "Var: (_5.0: i32). [ Binary(AddWithOverflow, Place(_1), Constant(Val(Scalar(0x00000001), i32))) , Binary(AddWithOverflow, Place(_1), Constant(Val(Scalar(0x00000001), i32))) ]",
        "Var: _6. [ Place(_1) , Place(_1) ]",
        "Var: _8. [ Constant(Val(Scalar(0x00000001), i32)) , Constant(Val(Scalar(0x00000001), i32)) ]",
    ];

    for expected in expected_ranges {
        assert!(
            output.contains(expected),
            "Missing expected symbolic interval: '{}'\nFull output:\n{}",
            expected,
            output
        );
    }
}

#[test]
fn nonnull_sound_1() {
    let output = run_with_args("verify/nonnull_sound_1", VERIFY_CMD);
    assert_contain(&output, "function: caller_with_contract");
    assert_contain(&output, "result: SOUND");
    assert_contain(&output, "function: sound_chained_propagation");
    assert_contain(&output, "result: SOUND");
}

#[test]
fn adg_bug() {
    // This test pass if don't panic (e.g., stack overflow) during ADG construction and resolution.
    let _ = run_with_args("analyze/adg_bug_regression", ANALYZE_ADG_CMD);
}

#[test]
fn adg_simple_graph() {
    let _ = run_with_args("analyze/adg_simple_graph", ANALYZE_ADG_CMD);
    let graph_str =
        std::fs::read_to_string(project_path("analyze/adg_simple_graph").join("api_graph.yml"))
            .expect("read api_graph.yml fail");
    assert_contain(&graph_str, "path: foo");
    assert_contain(&graph_str, "path: bar");
    assert_contain(&graph_str, "path: vec_arg");
    assert_contain(&graph_str, "path: std::vec::Vec::<i32, std::alloc::Global>");
    assert_contain(&graph_str, "path: Item");
    assert_contain(&graph_str, "type: Api");
    assert_contain(&graph_str, "type: Ty");
    assert_contain(&graph_str, "type: Ret");
    assert_contain(&graph_str, "type: Arg");
    assert_contain(&graph_str, "from: 0");
    assert_contain(&graph_str, "to: 1");
    assert_contain(&graph_str, "from: 1");
    assert_contain(&graph_str, "to: 2");
    assert_contain(&graph_str, "from: 3");
    assert_contain(&graph_str, "to: 4");
}

#[test]
fn verify_module_filter() {
    let output = run_with_args(
        "verify/module_filter",
        &["verify", "--mode", "targeted", "--module", "a"],
    );
    assert_contain(&output, "function: a::f");
    assert_not_contain(&output, "function: b::g");
    assert_not_contain(&output, "function: c::h");

    let output = run_with_args(
        "verify/module_filter",
        &["verify", "--mode", "scan", "--module", "b"],
    );
    assert_contain(&output, "function: b::g");
    assert_not_contain(&output, "function: a::f");
    assert_not_contain(&output, "function: c::h");
}

#[test]
fn verify_crate_filter() {
    let output = run_with_args(
        "verify/module_filter",
        &["verify", "--mode", "targeted", "--crate", "verify_module_filter"],
    );
    assert_contain(&output, "function: a::f");
    assert_contain(&output, "function: b::g");
    assert_contain(&output, "function: c::h");

    let output = run_with_args(
        "verify/module_filter",
        &["verify", "--mode", "targeted", "--crate", "verify_module_filter", "--module", "a"],
    );
    assert_contain(&output, "function: a::f");
    assert_not_contain(&output, "function: b::g");
    assert_not_contain(&output, "function: c::h");

    let output = run_with_args(
        "verify/module_filter",
        &["verify", "--mode", "targeted", "--crate", "nonexistent_crate"],
    );
    assert_contain(&output, "--crate \"nonexistent_crate\" matched no targets");
}

#[test]
fn opt_bounds_len() {
    let output = run_with_args("opt/bounds_len", &["opt"]);
    assert_not_contain(&output, "RAPx|ERROR|");
    assert_contain(&output, "Potential optimizations detected");
    assert_contain(&output, "Bounds Checking: 2");
}

#[test]
fn opt_encoding_check() {
    let output = run_with_args("opt/encoding_check", &["opt"]);
    assert_not_contain(&output, "RAPx|ERROR|");
    assert_contain(&output, "Potential optimizations detected");
    assert_contain(&output, "Encoding Checking: 2");
}

#[test]
fn opt_hash_key_cloning() {
    let output = run_with_args("opt/hash_key_cloning", &["opt"]);
    assert_not_contain(&output, "RAPx|ERROR|");
    assert_contain(&output, "Potential optimizations detected");
    assert_contain(&output, "Cloning: 1");
}