Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337#![feature(rustc_private)]#[macro_use]mod common;use common::*;
const STRUCT: &str = verus_code_str! { #[derive(PartialEq, Eq)] struct Bike { hard_tail: bool, }};
test_verify_one_file! { #[test] test_impl_1 STRUCT.to_string() + verus_code_str! { impl Bike { pub closed spec fn is_hard_tail(&self) -> bool { self.hard_tail } }
fn test_impl_1(b: Bike) requires b.is_hard_tail() { assert(b.hard_tail); }
fn test_impl_2(b: &Bike) requires b.is_hard_tail() { assert(b.hard_tail); }
} => Ok(())}
test_verify_one_file! { #[test] test_impl_no_self STRUCT.to_string() + verus_code_str! { impl Bike { fn new() -> Bike { ensures(|result: Bike| result.hard_tail); Bike { hard_tail: true } } } } => Ok(())}
test_verify_one_file! { #[test] test_impl_no_self_fail_pub_private STRUCT.to_string() + verus_code_str! { impl Bike { pub fn new() -> Bike { ensures(|result: Bike| result.hard_tail); Bike { hard_tail: true } } } } => Err(err) => assert_vir_error_msg(err, "disallowed: field expression for a non-visible datatype")}
test_verify_one_file! { #[test] test_impl_mod_1 verus_code! { mod M1 { use verus_builtin::*;
#[derive(PartialEq, Eq)] pub struct Bike { pub hard_tail: bool, }
impl Bike { pub open spec fn is_hard_tail(&self) -> bool { self.hard_tail }
pub fn new() -> Bike { ensures(|result: Bike| result.hard_tail); Bike { hard_tail: true } } } }
mod M2 { use super::M1::Bike; use verus_builtin::*;
fn test_impl_1(b: Bike) requires b.is_hard_tail() { assert(b.is_hard_tail()); }
fn test_impl_2() { let b = Bike::new(); assert(b.is_hard_tail()); } } } => Ok(())}
test_verify_one_file! { #[test] test_impl_mod_priv_field verus_code! { mod M1 { #[derive(PartialEq, Eq)] pub struct Bike { hard_tail: bool, }
impl Bike { pub closed spec fn is_hard_tail(&self) -> bool { self.hard_tail } } }
mod M2 { use super::M1::Bike; use verus_builtin::*;
fn test_impl_1(b: Bike) requires b.is_hard_tail() { assert(b.is_hard_tail()); } } } => Ok(())}
const IMPL_GENERIC_SHARED: &str = verus_code_str! { #[derive(PartialEq, Eq)] struct Wrapper<A> { v: A, }
impl<A> Wrapper<A> { pub closed spec fn take(self) -> A { self.v } }};
test_verify_one_file! { #[test] test_impl_generic_pass IMPL_GENERIC_SHARED.to_string() + verus_code_str! { proof fn test_impl_1(a: int) { let w = Wrapper { v: a }; assert(w.take() == a); } } => Ok(())}
test_verify_one_file! { #[test] test_impl_generic_fail IMPL_GENERIC_SHARED.to_string() + verus_code_str! { proof fn test_impl_1(a: int) { let w = Wrapper { v: a }; assert(w.take() != a); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test_impl_generic_param verus_code! { #[derive(PartialEq, Eq, Structural)] struct Two<A, B> { a: A, b: B, }
#[derive(PartialEq, Eq)] struct Wrapper<A> { v: A, }
impl<A> Wrapper<A> { pub closed spec fn take<B>(self, b: B) -> Two<A, B> { Two { a: self.v, b: b } } }
proof fn test_impl_1(a: int) { let w = Wrapper { v: a }; assert(w.take(12i32) == Two { a: a, b: 12i32 }); } } => Ok(())}
test_verify_one_file! { #[test] test_impl_with_self verus_code! { #[derive(PartialEq, Eq, Structural)] struct Bike { hard_tail: bool, }
impl Bike { spec fn id(self) -> Self { self } } } => Ok(())}
test_verify_one_file! { #[test] test_illegal_trait_impl verus_code! { #[verifier::external] trait T { fn f() -> bool; }
struct S;
impl T for S { spec fn f() -> bool { true } } } => Err(err) => assert_vir_error_msg(err, "function for external trait must have mode `exec`")}
test_verify_one_file! { #[test] test_illegal_trait_impl_2 verus_code! { struct V { }
impl std::ops::Index<usize> for V { type Output = bool; fn index(&self, #[verifier::spec]idx: usize) -> &bool { &true } } } => Err(err) => assert_vir_error_msg(err, "function for external trait must have all parameters have mode `exec`")}
test_verify_one_file! { #[test] test_generic_struct verus_code! { #[derive(PartialEq, Eq)] struct TemplateCar<V> { four_doors: bool, passengers: u64, the_v: V, }
impl<V> TemplateCar<V> { fn template_new(v: V) -> (result: TemplateCar<V>) ensures equal(result.passengers, 205), equal(result.the_v, v), { TemplateCar::<V> { four_doors: false, passengers: 205, the_v: v } }
fn template_get_passengers(&self) -> (result: u64) ensures result == self.passengers { self.passengers }
fn template_get_v(self) -> (result: V) ensures equal(result, self.the_v) { self.the_v } }
fn test1() { let c3 = TemplateCar::<u64>::template_new(5); let p3 = c3.template_get_passengers(); assert(p3 == 205); let v = c3.template_get_v(); assert(v == 5); } } => Ok(())}
test_verify_one_file! { #[ignore] #[test] test_erased_assoc_type_param verus_code! { struct Foo<V> { v: V }
impl<V> Foo<V> { fn bar<F: Fn(V) -> bool>(f: Ghost<F>, v: Ghost<V>) -> Ghost<bool> { Ghost(f.requires((v,))) }
fn bar2<F: Fn(V) -> bool>(self, f: Ghost<F>) -> Ghost<bool> { Ghost(f.requires((self.v,))) } }
fn test() { let x: Ghost<u64> = Ghost(0u64); let z = |y: u64| true; Foo::<u64>::bar(Ghost(z), x);
let f = Foo::<u64> { v: 17 }; let w = |y: u64| true; let b: Ghost<bool> = f.bar2(Ghost(w)); } } => Ok(())}
test_verify_one_file! { #[test] test_resolve_self_ty verus_code! { struct Foo<V> { x: V, }
impl<V> Foo<V> { fn bar(self) -> (s: Self) ensures equal(self, s) { self }
fn bar2(self) -> (s: Self) ensures equal(self, s) { Self::bar(self) } } } => Ok(())}
test_verify_one_file! { #[test] unsafe_impl_fail_send verus_code! { struct Foo { x: u32, }
unsafe impl Send for Foo { } } => Err(e) => assert_vir_error_msg(e, "unsafe impl for `Send` is not allowed")}
test_verify_one_file! { #[test] unsafe_impl_fail_sync verus_code! { struct Foo { x: u32, }
unsafe impl Sync for Foo { } } => Err(e) => assert_vir_error_msg(e, "unsafe impl for `Sync` is not allowed")}