Enum Attr 

pub enum Attr {
    Trusted(Trusted),
    TrustedImpl(Trusted),
    Ignore(Ignored),
    ProvenExternally(Span),
    ShouldFail,
    Qualifiers(Vec<Ident>),
    Reveal(Vec<Ident>),
    InferOpts(PartialInferOpts),
    NoPanic,
    AssumeParametric(Vec<Ident>),
    NoSuggestions,
}

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(Span)

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

NoPanic

A #[no_panic] attribute

AssumeParametric(Vec<Ident>)

A #[assume_parametric(...)] attribute

NoSuggestions

A #[no_suggestions] attribute

Trait Implementations

impl Debug for Attr

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.