Trait DerefLogic 

pub trait DerefLogic: Deref {
    // Required method
    fn deref_logic(&self) -> &Self::Target;
}

Trait for dereference in logic.

Implementing this trait does not automatically unlock dereference syntax (&*x); you also need to have a logical alias:

use creusot_std::{logic::ops::DerefLogic, prelude::*};
use std::ops::Deref;

struct MyInt(Int);

impl DerefLogic for MyInt {
    #[logic]
    fn deref_logic(&self) -> &Self::Target {
        &self.0
    }
}

impl Deref for MyInt {
    type Target = Int;
    #[check(ghost)]
    #[logic_alias(self.deref_logic())]
    fn deref(&self) -> &Self::Target {
        &self.0
    }
}

#[requires(*x == 1int)]
fn foo(x: MyInt) {}

Required Methods

fn deref_logic(&self) -> &Self::Target

logic

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl<T, A: Allocator> DerefLogic for Box<T, A>

Available on crate feature nightly only.

fn deref_logic(&self) -> &T

logic

impl<T: ?Sized, A: Allocator> DerefLogic for Arc<T, A>

Available on crate feature nightly only.

fn deref_logic(&self) -> &T

logic(opaque)

impl<T: ?Sized, A: Allocator> DerefLogic for Rc<T, A>

Available on crate feature nightly only.

fn deref_logic(&self) -> &T

logic(opaque)

Implementors

impl<T: ?Sized> DerefLogic for Ghost<T>

impl<T: ?Sized> DerefLogic for Snapshot<T>

Available on creusot only.

impl<T> DerefLogic for GhostShared<T>