Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307#![feature(rustc_private)]#[macro_use]mod common;use common::*;
test_verify_one_file! { #[test] test_ignorable_items verus_code! { mod m { // Verus can ignore 'use' item use super::*;
pub open spec fn test() -> bool { true } }
fn test_use_item() { use m::test as test2; assert(test2()); }
fn test_macro_item() { let mut x = 1;
// Verus can ignore 'macro' item macro_rules! add_1 { () => { x = x + 1; } }
add_1!();
assert(x == 2); } } => Ok(())}
// TODO: spec fn, broadcast, etc.// TODO: ownership check
test_verify_one_file! { #[test] test_attr_syntax_items_without_nested_spec code! { #[verus_spec(requires 1 + 1 == 2)] fn test() { const fn f1(i: u64) -> u64 { i / 2 } fn f2(i: u64) -> u64 { i / 2 } const C: u64 = 4 + 5;
let x = f1(10); let y = f2(10); let z = C; proof! { assert(z == 9); assert(y == 5); // FAILS } } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test_attr_syntax_items_with_nested_spec code! { #[verus_spec(requires 1 + 1 == 2)] fn test() { #[verus_spec(r => ensures r == i / 2)] const fn f1(i: u64) -> u64 { i / 2 } #[verus_spec(r => ensures r == i / 2)] fn f2(i: u64) -> u64 { i / 2 } #[verus_spec()] const C: u64 = 4 + 5;
let x = f1(10); let y = f2(10); let z = C; proof! { assert(x == 5); assert(y == 5); assert(z == 9); } } } => Ok(())}
test_verify_one_file! { #[test] test_attr_syntax_items_ownership code! { struct S;
verus! { #[verifier::external_body] proof fn produce() -> tracked S { panic!() }
proof fn consume(tracked s: S) { } }
#[verus_spec(requires 1 + 1 == 2)] fn test() { const C: u64 = { proof! { let s = produce(); consume(s); consume(s); } 4 + 5 };
let z = C; } } => Err(err) => assert_rust_error_msg(err, "use of moved value")}
test_verify_one_file! { #[test] test_verus_items_without_nested_spec verus_code! { fn test() { const fn f1(i: u64) -> u64 { i / 2 } fn f2(i: u64) -> u64 { i / 2 } const C: u64 = 4 + 5;
let x = f1(10); let y = f2(10); let z = C; assert(z == 9); assert(y == 5); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test_verus_items_with_nested_spec verus_code! { fn test() { const fn f1(i: u64) -> (r: u64) ensures r == i / 2 { i / 2 } fn f2(i: u64) -> (r: u64) ensures r == i / 2 { i / 2 } const C: u64 = 4 + 5;
let x = f1(10); let y = f2(10); let z = C; assert(x == 5); assert(y == 5); assert(z == 9); } } => Ok(())}
test_verify_one_file! { #[test] test_verus_items_ownership verus_code! { struct S;
#[verifier::external_body] proof fn produce() -> tracked S { panic!() }
proof fn consume(tracked s: S) { }
fn test() { const C: u64 = { let s = produce(); consume(s); consume(s); 4 + 5 };
let z = C; } } => Err(err) => assert_rust_error_msg(err, "use of moved value")}
test_verify_one_file! { #[test] test_verus_items_ownership_nested verus_code! { fn test() { struct S;
#[verifier::external_body] proof fn produce() -> tracked S { panic!() }
proof fn consume(tracked s: S) { }
const C: u64 = { let s = produce(); consume(s); consume(s); 4 + 5 };
let z = C; } } => Err(err) => assert_rust_error_msg(err, "use of moved value")}
test_verify_one_file! { #[test] test_ghost_items verus_code! { proof fn test() { spec fn f(i: int) -> int decreases i { if i <= 0 { 0 } else { f(i - 1) + 1 } }
broadcast proof fn p(i: int) ensures #[trigger] f(i) >= 0 decreases i { if i > 0 { p(i - 1); } }
assert(f(200) >= 0) by { broadcast use p; } assert(f(100) >= 0); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] nested_items_in_spec_and_proof_fns_issue3134 verus_code! { #[verifier::external] fn ext(a: u8) -> u8 { a }
spec fn nested_fn(x: u8) -> int { fn e() { } x + 1 }
spec fn nested_const(x: u8) -> int { const C: u8 = 0; x + 1 }
spec fn nested_assume_specification(x: u8) -> int { pub assume_specification[ ext ](a: u8) -> u8; x + 1 }
proof fn nested_fn_in_proof_fn(x: u8) -> (r: int) ensures r == x + 1, { fn e() { } x + 1 }
proof fn test() { assert(nested_fn(255) == 256); assert(nested_const(255) == 256); assert(nested_assume_specification(255) == 256); } } => Ok(())}
test_verify_one_file! { #[test] nested_proof_fn_then_proof_block_in_exec_fn_issue3134 verus_code! { fn test() { proof fn p() { } proof { p(); } } } => Ok(())}
test_verify_one_file! { #[test] nested_exec_fn_in_proof_block_issue3134 verus_code! { fn test() { proof { fn e() { } } } } => Ok(())}