Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412#![feature(rustc_private)]#[macro_use]mod common;use common::*;
test_verify_one_file! { #[test] recursive_exec_function_with_decreases_clause verus_code! { fn a(i: u64) -> (r: u64) ensures r == i decreases i { if i == 0 { return 0; } else { return 1 + a(i - 1); } } } => Ok(())}
test_verify_one_file_with_options! { #[test] recursive_exec_function_with_decreases_clause_exec_allows_no_decreases_clause ["exec_allows_no_decreases_clause"] => verus_code! { fn a(i: u64) -> (r: u64) ensures r == i decreases i { if i == 0 { return 0; } else { return 1 + a(i - 1); } } } => Ok(err) => assert!(err.warnings.iter().find(|x| x.message.contains("if `exec_allows_no_decreases_clause` is set, decreases checks in exec functions do not guarantee termination of functions with loops")).is_some())}
test_verify_one_file_with_options! { #[test] recursive_exec_function_with_decreases_clause_exec_allows_no_decreases_clause_no_warning ["exec_allows_no_decreases_clause"] => verus_code! { #[verifier::allow(decreases_when_exec_allows_no_decreases_clause)] fn a(i: u64) -> (r: u64) ensures r == i decreases i { if i == 0 { return 0; } else { return 1 + a(i - 1); } } } => Ok(())}
test_verify_one_file_with_options! { #[test] recursive_exec_function_with_decreases_clause_exec_allows_no_decreases_clause_fails ["exec_allows_no_decreases_clause"] => verus_code! { fn a(i: u64) -> (r: u64) ensures r == i decreases i { if i == 0 { return 0; } else { return a(i); // FAILS } } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] recursive_exec_function_needs_decreases_clause verus_code! { fn a(i: u64) -> (r: u64) ensures r == i { if i == 0 { return 0; } else { return 1 + a(i - 1); } } } => Err(err) => assert_vir_error_msg(err, "recursive function must have a `decreases` clause")}
test_verify_one_file! { #[test] mutually_recursive_exec_functions_need_decreases_clause verus_code! { fn dec1(i: u64) { if 0 < i { dec2(i, 100 * i); } // FAIL } fn dec2(j: u64, k: u64) decreases j, k { if 0 < k { dec2(j, k - 1); } if 0 < j { dec2(j - 1, 100 * j + k); dec1(j - 1); } } } => Err(err) => assert_vir_error_msg(err, "recursive function must have a `decreases` clause")}
test_verify_one_file! { #[test] mutually_recursive_exec_functions_with_extra_dependency_need_decreases_clause verus_code! { fn dec1b(i: u64) { dec2b(i); // FAIL } #[verifier(external_body)] fn dec2b(i: u64) { extra_dependency(dec1b); unimplemented!(); } } => Err(err) => assert_vir_error_msg(err, "recursive function must have a `decreases` clause")}
test_verify_one_file! { #[test] mutually_recursive_exec_functions_in_different_modules_need_decreases_clause verus_code! { mod M1 { use verus_builtin::*; pub(crate) fn f1(i: u64) -> u64 { crate::M2::f2(i - 1) } // FAIL } mod M2 { use verus_builtin::*; pub(crate) fn f2(i: u64) -> u64 { crate::M1::f1(i - 1) } } } => Err(err) => { assert_eq!(err.errors.len(), 2); assert!(err.errors[0].code.is_none()); assert!(err.errors[1].code.is_none()); assert!(err.errors[0].message.contains("recursive function must have a `decreases` clause")); assert!(err.errors[1].message.contains("recursive function must have a `decreases` clause")); }}
test_verify_one_file! { #[test] while_loop_needs_decreases_clause verus_code! { fn a() { let mut i = 0; while i < 10 // FAIL invariant i <= 10 { i = i + 1; } } } => Err(err) => assert_vir_error_msg(err, "loop must have a `decreases` clause")}
test_verify_one_file! { #[test] nested_while_loops_need_decreases_clauses verus_code! { fn a() { let mut i = 0; let mut j = 0; while i < 10 invariant i <= 10, j <= 5 decreases 10 - i, { i = i + 1; while j < 5 // FAIL invariant j <= 5 { j = j + 1; } } } } => Err(err) => assert_vir_error_msg(err, "loop must have a `decreases` clause")}
test_verify_one_file! { #[test] loop_with_break_with_decreases_clause verus_code! { fn a() { let mut i: i8 = 0; loop invariant_except_break i <= 9 invariant 0 <= i <= 10 ensures 1 <= i decreases 10 - i { i = i + 1; if i == 10 { break; } } } } => Ok(())}
test_verify_one_file! { #[test] loop_with_break_need_decreases_clause verus_code! { fn a() { let mut i: i8 = 0; loop // FAIL invariant_except_break i <= 9 invariant 0 <= i <= 10 ensures 1 <= i { i = i + 1; if i == 10 { break; } } } } => Err(err) => assert_vir_error_msg(err, "loop must have a `decreases` clause")}
test_verify_one_file! { #[test] for_loop_with_decreases_clause verus_code! { use vstd::prelude::*; fn a() { let mut i: i8 = 0; for x in iter: 0..10 invariant i == x * 3, decreases 10 - iter.index() { i += 3; } } } => Ok(())}
test_verify_one_file! { #[test] for_loop_2_with_decreases_clause verus_code! { use vstd::prelude::*; fn a() { let mut i: i8 = 0; #[verifier::loop_isolation(false)] for x in 0..10 invariant i == x * 3, decreases 10 - x { i += 3; } } } => Ok(())}
test_verify_one_file! { #[test] for_loop_doesnt_need_explicit_decreases_clause verus_code! { use vstd::prelude::*; fn a() { let mut i: i8 = 0; // syntax macro inserts decreases clause automatically for x in iter: 0..10 invariant i == x * 3, { i += 3; } } } => Ok(())}
test_verify_one_file_with_options! { #[test] nontermination_infinite_loop_allowed_with_attribute ["exec_allows_no_decreases_clause"] => verus_code! { fn a(i: u64) -> (r: u64) ensures false { loop {} } } => Ok(())}
test_verify_one_file_with_options! { #[test] nontermination_infinite_loop_with_ghost_allowed_with_attribute ["exec_allows_no_decreases_clause"] => verus_code! { use vstd::modes::*; fn a() { let ghost mut a: int = 5; loop invariant a > 0 { proof { a = a + 1; } } } } => Ok(())}
test_verify_one_file! { #[test] exec_recursive_function_with_while_loop_with_loop_isolation_false verus_code! { #[verifier::loop_isolation(false)] fn a(mut i: u64) requires i <= 10, decreases i, { let ghost initial_i = i; while 0 < i && i <= 10 invariant 0 <= i <= 10, i <= initial_i, decreases i, { a(i - 1); i -= 1; } } } => Ok(())}
test_verify_one_file! { #[test] exec_recursive_function_with_while_loop_assume_termination verus_code! { #[verifier::assume_termination] fn a(mut i: u64) requires i <= 10, { let ghost initial_i = i; while 0 < i && i <= 10 invariant 0 <= i <= 10, i <= initial_i, { a(i - 1); i -= 1; } } } => Ok(())}
test_verify_one_file! { #[test] exec_terminating_function_can_call_nonterminating_function verus_code! { fn a(mut i: u64) { while i > 0 invariant 0 <= i, decreases i, { b(); i -= 1; } }
#[verifier::exec_allows_no_decreases_clause] fn b() { loop { } } } => Ok(())}
test_verify_one_file! { #[test] exec_termination_flag_1 verus_code! { fn a<AA: A>(mut i: u64) { while i > 0 invariant 0 <= i, decreases i, { AA::b(); i -= 1; } }
trait A { #[verifier::exec_allows_no_decreases_clause] fn b(); } } => Err(err) => assert_vir_error_msg(err, "trait method declaration cannot declare `exec_allows_no_decreases_clause`")}
test_verify_one_file! { #[test] exec_termination_flag_2 verus_code! { trait A { fn b(); }
struct X { }
impl A for X { #[verifier::exec_allows_no_decreases_clause] fn b() { loop { } } } } => Ok(())}
test_verify_one_file_with_options! { #[test] exec_termination_flag_3 ["exec_allows_no_decreases_clause"] => verus_code! { trait A { fn b(); }
struct X { }
impl A for X { fn b() { loop { } } } } => Ok(())}
test_verify_one_file! { #[test] exec_termination_flag_4 verus_code! { trait A { fn b(); }
struct X { }
impl A for X { fn b() { loop { } } } } => Err(err) => assert_vir_error_msg(err, "loop must have a `decreases` clause")}
test_verify_one_file! { #[test] exec_termination_flag_5 verus_code! { trait A { #[verifier::exec_allows_no_decreases_clause] fn b() { loop { } } } } => Ok(())}