pub enum Attr {
Trusted(Trusted),
TrustedImpl(Trusted),
Ignore(Ignored),
ProvenExternally,
ShouldFail,
Qualifiers(Vec<Ident>),
Reveal(Vec<Ident>),
InferOpts(PartialInferOpts),
}
Expand description
An attribute attaches metadata to an item.
Note that some of these attributes correspond to a Rust attribute, but some don’t. For example,
when annotating a function, a #[flux::trusted]
is mapped to Attr::Trusted
because it
corresponds to metadata associated to the function, however, a #[flux::spec(...)]
doesn’t
map to any Attr
because that’s considered to be part of the refined syntax of the item.
Note that these attributes can also originate from detached specs.
Variants§
Trusted(Trusted)
A #[trusted(...)]
attribute
TrustedImpl(Trusted)
A #[trusted_impl(...)]
attribute
Ignore(Ignored)
A #[ignore(...)]
attribute
ProvenExternally
A #[proven_externally]
attribute
ShouldFail
A #[should_fail]
attribute
Qualifiers(Vec<Ident>)
A #[qualifiers(...)]
attribute
Reveal(Vec<Ident>)
A #[reveal(...)]
attribute
InferOpts(PartialInferOpts)
A #[opts(...)]
attribute
Trait Implementations§
Auto Trait Implementations§
impl Freeze for Attr
impl RefUnwindSafe for Attr
impl Send for Attr
impl Sync for Attr
impl Unpin for Attr
impl UnwindSafe for Attr
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more