ravencheck 0.5.0

Decidable verification of Rust code using relational abstraction.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14

#[crate::check_module(crate)]
#[declare_types(u32)]
#[allow(dead_code)]
mod bool_fun {
    #[declare]
    fn foo(_b: bool) -> u32 {
        0
    }

    #[falsify]
    fn prop1(n: u32) -> bool {
        n == foo(n == n)
    }
}