Document Cargo usage and add integration tests

README.md

@@ -66,6 +66,45 @@ safe
 
 Integration test examples are located under `tests/ui/` and can be executed using `cargo test`. You can review these examples to understand what the current Thrust implementation can handle.
 
+### Using Thrust with Cargo
+
+Thrust can check Cargo projects that have no dependencies. External crates are not supported yet (#255).
+
+First, build Thrust in its source directory:
+
+```sh
+cargo build --bin thrust-rustc
+```
+
+Set up a project using the same Rust toolchain as Thrust (currently `nightly-2025-09-08`):
+
+```sh
+cargo +nightly-2025-09-08 new --edition 2021 thrust-example
+cd thrust-example
+```
+
+Add assertions to your code. For example, write the following in `src/main.rs`:
+
+```rust
+fn add(x: i64, y: i64) -> i64 {
+    x + y
+}
+
+fn main() {
+    assert!(add(1, 2) == 3);
+}
+```
+
+With Z3 on your `PATH`, set `RUSTC` to the absolute path of the built `thrust-rustc` binary and run:
+
+```sh
+RUSTC=/absolute/path/to/thrust/target/debug/thrust-rustc \
+RUSTFLAGS='-C debug-assertions=false' \
+cargo +nightly-2025-09-08 check
+```
+
+For the example above, the check succeeds. Changing the assertion to `add(1, 2) == 2` makes it fail with `verification error: Unsat` and a nonzero exit status.
+
 ## Annotation
 
 Thrust can verify a wide range of programs without explicit annotations, but you can use `#[thrust_macros::requires(expr)]` and `#[thrust_macros::ensures(expr)]` to annotate the precondition and postcondition of a function, aiding in verification or specifying the intended behavior. Here, `expr` is an ordinary Rust expression that Thrust interprets as a logical formula. It supports the usual integer, boolean, and comparison operators, calls to functions declared with `#[thrust_macros::predicate]`, and the model operations described below.

tests/cargo.rs

@@ -0,0 +1,38 @@
+use std::process::{Command, Output};
+
+fn cargo_check(fixture: &str) -> Output {
+    let target_dir = tempfile::tempdir().unwrap();
+    let fixture = std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
+        .join("tests/cargo")
+        .join(fixture);
+    Command::new(env!("CARGO"))
+        .args(["check", "--offline", "--locked", "--manifest-path"])
+        .arg(fixture.join("Cargo.toml"))
+        .env("RUSTC", env!("CARGO_BIN_EXE_thrust-rustc"))
+        .env("RUSTFLAGS", "-C debug-assertions=false")
+        .env("CARGO_TARGET_DIR", target_dir.path())
+        .env_remove("CARGO_ENCODED_RUSTFLAGS")
+        .env_remove("RUSTC_WRAPPER")
+        .env_remove("RUSTC_WORKSPACE_WRAPPER")
+        .env_remove("THRUST_OUTPUT_DIR")
+        .output()
+        .unwrap()
+}
+
+#[test]
+fn cargo_check_passes_verification() {
+    let output = cargo_check("pass");
+    assert!(
+        output.status.success(),
+        "{}",
+        String::from_utf8_lossy(&output.stderr)
+    );
+}
+
+#[test]
+fn cargo_check_reports_verification_failure() {
+    let output = cargo_check("fail");
+    let stderr = String::from_utf8_lossy(&output.stderr);
+    assert!(!output.status.success(), "{stderr}");
+    assert!(stderr.contains("verification error: Unsat"), "{stderr}");
+}

tests/cargo/fail/Cargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "thrust-cargo-test"
+version = "0.1.0"
+edition = "2021"
+
+[workspace]

tests/cargo/fail/src/arithmetic.rs

@@ -0,0 +1,3 @@
+mod add;
+
+pub use add::add;

tests/cargo/fail/src/arithmetic/add.rs

@@ -0,0 +1,3 @@
+pub fn add(x: i64, y: i64) -> i64 {
+    x + y
+}

tests/cargo/fail/src/main.rs

@@ -0,0 +1,5 @@
+mod arithmetic;
+
+fn main() {
+    assert!(arithmetic::add(1, 2) == 2);
+}

tests/cargo/pass/Cargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "thrust-cargo-test"
+version = "0.1.0"
+edition = "2021"
+
+[workspace]

tests/cargo/pass/src/arithmetic.rs

@@ -0,0 +1,3 @@
+mod add;
+
+pub use add::add;

tests/cargo/pass/src/arithmetic/add.rs

@@ -0,0 +1,3 @@
+pub fn add(x: i64, y: i64) -> i64 {
+    x + y
+}

tests/cargo/pass/src/main.rs

@@ -0,0 +1,5 @@
+mod arithmetic;
+
+fn main() {
+    assert!(arithmetic::add(1, 2) == 3);
+}