Struct GhostShared 

pub struct GhostShared<T>(/* private fields */);

A type for sharing ghost data immutably.

Implementations

impl<T> GhostShared<T>

pub fn new(val: Ghost<T>) -> Ghost<Self>

Create a new shared ghost value.

Note that the original value can never be retrieved, which allows this function to resolve it (in GhostShared’s type invariant).

ghost

ensures

result@ == *val

impl<T> GhostShared<T>

pub fn val(self) -> T

The logical value contained in this GhostShared.

logic

pub fn to_ref<'a>(self) -> &'a T

Access the value of the GhostShared immutably.

Note on lifetimes

Note that this function returns a borrow at an arbitrary lifetime 'a. This is possible because GhostShared is a ghost-only type: the underlying T object is ‘magically’ made to live at least as long as 'a.

ghost

ensures

*result == self.val()

Trait Implementations

impl<T> AsRef<T> for GhostShared<T>

fn as_ref(&self) -> &T

ghost

ensures

*result == self.val()

impl<T> Clone for GhostShared<T>

fn clone(&self) -> Self

ghost

ensures

result == *self

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<T> Copy for GhostShared<T>

impl<T> Deref for GhostShared<T>

fn deref(&self) -> &T

ghost

ensures

*result == self.val()

type Target = T

The resulting type after dereferencing.

impl<T> Invariant for GhostShared<T>

fn invariant(self) -> bool

logic(open, prophetic)

resolve(self.val()) && inv(self.val())

impl<T: Sync> Send for GhostShared<T>

impl<T: Sync> Sync for GhostShared<T>

impl<T> View for GhostShared<T>

fn view(self) -> T

logic(open, inline)

self.val()

type ViewTy = T