splitrs 0.3.3

AST-based Rust refactoring tool with trait separation, config files, and intelligent module generation
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75

//! Integration tests for the `--verify-equiv` CLI core (`smt` feature).
//!
//! Writes two `.rs` fixtures into a temp directory and drives the library
//! `run_verify_equiv_core` (the structured-return surface), asserting on the
//! outcome without scraping stdout. Temp files use the OS temp dir per policy.

#![cfg(feature = "smt")]

use std::fs;

use splitrs::smt_cli::{run_verify_equiv_core, VerifyOutcome};
use tempfile::TempDir;

/// Write `contents` to `<dir>/<name>` and return the path as a String.
fn write_fixture(dir: &TempDir, name: &str, contents: &str) -> String {
    let path = dir.path().join(name);
    fs::write(&path, contents).expect("fixture write should succeed");
    path.to_string_lossy().into_owned()
}

#[test]
fn equivalent_pair_verifies() {
    let dir = TempDir::new().expect("temp dir");
    let left = write_fixture(
        &dir,
        "left.rs",
        "pub fn add(a: u32, b: u32) -> u32 { a + b }\n",
    );
    let right = write_fixture(
        &dir,
        "right.rs",
        "pub fn add_swapped(a: u32, b: u32) -> u32 { b + a }\n",
    );

    let outcome = run_verify_equiv_core(&format!("{left}::add"), &format!("{right}::add_swapped"))
        .expect("verify-equiv core should run");
    assert!(
        matches!(outcome, VerifyOutcome::Verified),
        "expected Verified, got {outcome:?}"
    );
}

#[test]
fn non_equivalent_pair_refutes() {
    let dir = TempDir::new().expect("temp dir");
    let left = write_fixture(
        &dir,
        "sum.rs",
        "pub fn sum(a: u32, b: u32) -> u32 { a + b }\n",
    );
    let right = write_fixture(
        &dir,
        "diff.rs",
        "pub fn diff(a: u32, b: u32) -> u32 { a - b }\n",
    );

    let outcome = run_verify_equiv_core(&format!("{left}::sum"), &format!("{right}::diff"))
        .expect("verify-equiv core should run");
    match outcome {
        VerifyOutcome::Refuted(cx) => {
            assert_eq!(cx.inputs.len(), 2, "expected two input bindings");
        }
        other => panic!("expected Refuted, got {other:?}"),
    }
}

#[test]
fn missing_function_is_an_error() {
    let dir = TempDir::new().expect("temp dir");
    let left = write_fixture(&dir, "a.rs", "pub fn present(a: u32) -> u32 { a }\n");
    let right = write_fixture(&dir, "b.rs", "pub fn present(a: u32) -> u32 { a }\n");

    let result = run_verify_equiv_core(&format!("{left}::absent"), &format!("{right}::present"));
    assert!(result.is_err(), "missing function should be an error");
}