Skip to content

Commit

Permalink
fix a few tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@tjhance
tjhance committed Mar 23, 2023
1 parent 868d364 commit 5060d0b
Show file tree
Hide file tree
Showing 2 changed files with 30 additions and 19 deletions.
1 change: 1 addition & 0 deletions source/rust_verify/example/verified_vec.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ use vstd::*;
use vstd::modes::*;
use vstd::ptr::*;
use vstd::prelude::*;
use vstd::layout::*;

verus!{

Expand Down
48 changes: 29 additions & 19 deletions source/rust_verify_test/tests/cell_lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ test_verify_one_file! {
}

const PTR_TEST: &str = code_str! {
let (ptr, Tracked(mut token)) = PPtr::<u32>::empty();
let (ptr, Tracked(mut token), Tracked(dealloc)) = PPtr::<u32>::empty();
assert(equal(token.view().pptr, ptr.id()));
assert(equal(token.view().value, option::Option::None));

Expand All @@ -76,7 +76,7 @@ const PTR_TEST: &str = code_str! {
assert(equal(token.view().value, option::Option::None));
assert(equal(x, 7));

ptr.dispose(Tracked(token));
ptr.dispose(Tracked(token), Tracked(dealloc));
};

test_verify_one_file! {
Expand Down Expand Up @@ -173,8 +173,8 @@ test_verify_one_file! {
test_verify_one_file! {
#[test] ptr_mismatch_put IMPORTS.to_string() + verus_code_str! {
pub fn f() {
let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
let (ptr2, Tracked(mut token2)) = PPtr::<u32>::empty();
let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
let (ptr2, Tracked(mut token2), Tracked(dealloc)) = PPtr::<u32>::empty();
ptr1.put(Tracked(&mut token2), 5); // FAILS
}
} => Err(err) => assert_one_fails(err)
Expand All @@ -183,8 +183,8 @@ test_verify_one_file! {
test_verify_one_file! {
#[test] ptr_mismatch_take IMPORTS.to_string() + verus_code_str! {
pub fn f() {
let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
let (ptr2, Tracked(mut token2)) = PPtr::<u32>::empty();
let (ptr1, Tracked(mut token1), Tracked(dealloc1)) = PPtr::<u32>::empty();
let (ptr2, Tracked(mut token2), Tracked(dealloc2)) = PPtr::<u32>::empty();
ptr1.put(Tracked(&mut token1), 5);
ptr2.put(Tracked(&mut token2), 5);
let x = ptr1.take(Tracked(&mut token2)); // FAILS
Expand All @@ -195,8 +195,8 @@ test_verify_one_file! {
test_verify_one_file! {
#[test] ptr_mismatch_replace IMPORTS.to_string() + verus_code_str! {
pub fn f() {
let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
let (ptr2, Tracked(mut token2)) = PPtr::<u32>::empty();
let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
let (ptr2, Tracked(mut token2), Tracked(dealloc)) = PPtr::<u32>::empty();
ptr1.put(Tracked(&mut token1), 5);
ptr2.put(Tracked(&mut token2), 5);
let x = ptr1.replace(Tracked(&mut token2), 7); // FAILS
Expand All @@ -207,8 +207,8 @@ test_verify_one_file! {
test_verify_one_file! {
#[test] ptr_mismatch_borrow IMPORTS.to_string() + verus_code_str! {
pub fn f() {
let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
let (ptr2, Tracked(mut token2)) = PPtr::<u32>::empty();
let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
let (ptr2, Tracked(mut token2), Tracked(dealloc)) = PPtr::<u32>::empty();
ptr1.put(Tracked(&mut token1), 5);
ptr2.put(Tracked(&mut token2), 5);
let x = ptr1.borrow(Tracked(&token2)); // FAILS
Expand All @@ -219,17 +219,27 @@ test_verify_one_file! {
test_verify_one_file! {
#[test] ptr_mismatch_dispose IMPORTS.to_string() + verus_code_str! {
pub fn f() {
let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
let (ptr2, Tracked(mut token2)) = PPtr::<u32>::empty();
ptr1.dispose(Tracked(token2)); // FAILS
let (ptr1, Tracked(mut token1), Tracked(dealloc1)) = PPtr::<u32>::empty();
let (ptr2, Tracked(mut token2), Tracked(dealloc2)) = PPtr::<u32>::empty();
ptr1.dispose(Tracked(token2), Tracked(dealloc1)); // FAILS
}
} => Err(err) => assert_one_fails(err)
}

test_verify_one_file! {
#[test] ptr_mismatch_dispose2 IMPORTS.to_string() + verus_code_str! {
pub fn f() {
let (ptr1, Tracked(mut token1), Tracked(dealloc1)) = PPtr::<u32>::empty();
let (ptr2, Tracked(mut token2), Tracked(dealloc2)) = PPtr::<u32>::empty();
ptr1.dispose(Tracked(token1), Tracked(dealloc2)); // FAILS
}
} => Err(err) => assert_one_fails(err)
}

test_verify_one_file! {
#[test] ptr_some_put IMPORTS.to_string() + verus_code_str! {
pub fn f() {
let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
ptr1.put(Tracked(&mut token1), 7);
ptr1.put(Tracked(&mut token1), 5); // FAILS
}
Expand All @@ -239,7 +249,7 @@ test_verify_one_file! {
test_verify_one_file! {
#[test] ptr_none_take IMPORTS.to_string() + verus_code_str! {
pub fn f() {
let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
let x = ptr1.take(Tracked(&mut token1)); // FAILS
}
} => Err(err) => assert_one_fails(err)
Expand All @@ -248,7 +258,7 @@ test_verify_one_file! {
test_verify_one_file! {
#[test] ptr_none_replace IMPORTS.to_string() + verus_code_str! {
pub fn f() {
let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
let x = ptr1.replace(Tracked(&mut token1), 7); // FAILS
}
} => Err(err) => assert_one_fails(err)
Expand All @@ -257,7 +267,7 @@ test_verify_one_file! {
test_verify_one_file! {
#[test] ptr_none_borrow IMPORTS.to_string() + verus_code_str! {
pub fn f() {
let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
let x = ptr1.borrow(Tracked(&token1)); // FAILS
}
} => Err(err) => assert_one_fails(err)
Expand All @@ -266,9 +276,9 @@ test_verify_one_file! {
test_verify_one_file! {
#[test] ptr_some_dispose IMPORTS.to_string() + verus_code_str! {
pub fn f() {
let (ptr1, Tracked(mut token1)) = PPtr::<u32>::empty();
let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::<u32>::empty();
ptr1.put(Tracked(&mut token1), 5);
ptr1.dispose(Tracked(token1)); // FAILS
ptr1.dispose(Tracked(token1), Tracked(dealloc)); // FAILS
}
} => Err(err) => assert_one_fails(err)
}
Expand Down

0 comments on commit 5060d0b

Please sign in to comment.