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
//! Example demonstrating Kani contract verification for tool chains.
//!
//! This example shows how to:
//! 1. Define tools with formal contracts
//! 2. Compose tools into chains
//! 3. Verify chain compatibility with Kani
//!
//! Run with:
//! ```bash
//! cargo run --example kani_example --features verify-kani
//! ```
//!
//! Verify with Kani:
//! ```bash
//! cargo kani --example kani_example
//! ```
#[cfg(not(feature = "verify-kani"))]
fn main() {
eprintln!("This example requires the verify-kani feature.");
eprintln!("Run with: cargo run --example kani_example --features verify-kani");
}
#[cfg(feature = "verify-kani")]
mod kani_enabled {
// Domain types and implementations would go here
// For now, just a simple main that exits
pub fn run_main() {
println!("Kani example - feature enabled but implementation TBD");
}
}
#[cfg(feature = "verify-kani")]
fn main() {
kani_enabled::run_main();
}