Skip to main content

FunEnv

flux_infer::fixpoint_encoding

Struct FunEnv 

Source 
struct FunEnv {
    reveals: UnordSet<FluxDefId>,
    hides: UnordSet<FluxDefId>,
    proven_externally: bool,
}
Expand description

Determines which Flux functions are uninterpreted in the constraint generated for an item.

Fields§

§reveals: UnordSet<FluxDefId>§hides: UnordSet<FluxDefId>

Functions hidden for the item (with #[hide] on the item)

§proven_externally: bool

Implementations§

Source§

impl FunEnv

Source

fn new(genv: GlobalEnv<'_, '_>, def_id: MaybeExternId) -> Self

Source

fn is_uninterpreted(&self, genv: GlobalEnv<'_, '_>, did: FluxDefId) -> bool

A function is uninterpreted if it has no definition, or if it is hidden (either at its definition or for the item) and it is not revealed for the item, unless the item is proven externally.

Auto Trait Implementations§

§

impl DynSend for FunEnv

§

impl DynSync for FunEnv

§

impl Freeze for FunEnv

§

impl RefUnwindSafe for FunEnv

§

impl Send for FunEnv

§

impl Sync for FunEnv

§

impl Unpin for FunEnv

§

impl UnsafeUnpin for FunEnv

§

impl UnwindSafe for FunEnv

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T> Instrument for T

§

fn instrument(self, span: Span) -> Instrumented<Self> ⓘ

Instruments this type with the provided [Span], returning an Instrumented wrapper. Read more
§

fn in_current_span(self) -> Instrumented<Self> ⓘ

Instruments this type with the current Span, returning an Instrumented wrapper. Read more
Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T> IntoEither for T

Source§

fn into_either(self, into_left: bool) -> Either<Self, Self> ⓘ

Converts self into a Left variant of Either<Self, Self> if into_left is true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more
Source§

fn into_either_with<F>(self, into_left: F) -> Either<Self, Self> ⓘ
where F: FnOnce(&Self) -> bool,

Converts self into a Left variant of Either<Self, Self> if into_left(&self) returns true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more
Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = !

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, !>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T> WithSubscriber for T

§

fn with_subscriber<S>(self, subscriber: S) -> WithDispatch<Self> ⓘ
where S: Into<Dispatch>,

Attaches the provided Subscriber to this type, returning a [WithDispatch] wrapper. Read more
§

fn with_current_subscriber(self) -> WithDispatch<Self> ⓘ

Attaches the current default Subscriber to this type, returning a [WithDispatch] wrapper. Read more