verus_pptr_example.rs

use vstd::prelude::*;

verus! {

use vstd::ptr::PPtr;

// ** each executable line is preceded by a comment with the equivalent regular rust unsafe code **

fn main() {
    // let ptr = std::alloc::alloc(std::alloc::Layout::new:: <u64>()) as *mut u64;
    let (pptr, Tracked(perm), Tracked(dealloc)) = PPtr::<u64>::empty();

    assert(perm@.pptr == pptr.id());
    assert(perm@.value == None::<u64>);

    // *ptr = 5;
    pptr.put(Tracked(&mut perm), 5);

    assert(perm@.value == Some::<u64>(5));

    // let x: u64 = *ptr;
    let x: u64 = *pptr.borrow(Tracked(&perm));
    assert(x == 5);

    // std::alloc::dealloc(ptr as *mut u8, std::alloc::Layout::new::<u64>());
    let _ = pptr.into_inner(Tracked(perm), Tracked(dealloc));

    // let z: u64 = *ptr;
    // let z: u64 = *pptr.borrow(Tracked(&perm)); would fail because `perm` was moved
}

} // verus!