Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081// rust_verify/tests/example.rs expect-failuresuse verus_builtin::*;use verus_builtin_macros::*;
verus! {
fn main() {}
/*fn test_params(i: int, n: nat, u: u8) { assert(n >= 5);}
fn test_mutation(i: int, n: nat, u: u8) { let mut x = 5; x = x + i; x = x + n; x = x + u; assert(x >= 5);}*/
spec fn add_one(i: int) -> int { i + 1}
fn very_simple(z: int) { let mut x = z; // 1_mutation assert(add_one(x) < 3);}
// fn test_if_else(b:bool, z:int) {// let mut x : int;// let mut y : int = z; // 0_entry// let mut f : int;// x = x + y; // 1_mutation// if b {// x = 2*x; // 2_mutation// y = x + 1; // 3_mutation// } else {// let mut dd : int;// if b {// let mut ddd : int;// assert(true);// x = 2*x; // 4_mutation// y = x + 1; // 5_mutation// } // 6_join// x = y + 1; // 7_mutation// y = 7; // 8_mutation// f = 34; // 9_mutation// } // 10_join// assert(x + y > 5);// }/*fn test_loop() { let mut i: u64 = 10; let mut b1: u8 = 20; let mut b2: u8 = 200; let mut b3: u8 = 30; // 0_entry i = i + 1; // 1_mutation i = i - 1; // 2_mutation
while i < 100 { invariant([ 10 <= i, i <= 100, b1 as u64 == i * 2, ]); // 3_while_begin assert(b1 == 5); i = i + 1; // 4_mutation b1 = b1 + 2; // 5_mutation b2 = b2 + 1; // 6_mutation } // 5_while_end
assert(true); // 7_while_end}*/} // verus!