Enum Attribute 

pub enum Attribute {
    Opaque,
    Exclude,
    Rename(String),
    VariantsPrefix(String),
    VariantsSuffix(String),
    Transparent,
    IsContract {
        kind: String,
        target: MaybeAssocItemId,
    },
    HasContract {
        kind: String,
        contract: FunDeclId,
    },
    DocComment(String),
    Builtin(AttributeKind),
    Unknown(RawAttribute),
}

Attributes (#[...]).

Variants

Opaque

Do not translate the body of this item. Written #[charon::opaque]

Exclude

Do not translate this item at all. Written #[charon::exclude]

Rename(String)

Provide a new name that consumers of the llbc can use. Written #[charon::rename("new_name")]

VariantsPrefix(String)

For enums only: rename the variants by pre-pending their names with the given prefix. Written #[charon::variants_prefix("prefix_")].

VariantsSuffix(String)

Same as VariantsPrefix, but appends to the name instead of pre-pending.

Transparent

The structure is treated as a transparent wrapper around its sole field. Written #[charon::transparent].

IsContract

An item annotated with #[charon::contract(kind = "...", parent)] or #[charon::contract(kind = "...", for = "...")]. This makes it a contract for the target item.

Fields

kind: String

target: MaybeAssocItemId

HasContract

An item that has a contract that applies to it. The referenced item is the function that specifies the contract.

Fields

kind: String

contract: FunDeclId

DocComment(String)

A doc-comment such as /// ....

Builtin(AttributeKind)

A built-in attribute.

Unknown(RawAttribute)

None of the above.

Implementations

impl Attribute

pub fn is_opaque(&self) -> bool

pub fn is_exclude(&self) -> bool

pub fn is_rename(&self) -> bool

pub fn is_variants_prefix(&self) -> bool

pub fn is_variants_suffix(&self) -> bool

pub fn is_transparent(&self) -> bool

pub fn is_is_contract(&self) -> bool

pub fn is_has_contract(&self) -> bool

pub fn is_doc_comment(&self) -> bool

pub fn is_builtin(&self) -> bool

pub fn is_unknown(&self) -> bool

impl Attribute

pub fn as_opaque(&self) -> Option<()>

pub fn as_exclude(&self) -> Option<()>

pub fn as_rename(&self) -> Option<&String>

pub fn as_variants_prefix(&self) -> Option<&String>

pub fn as_variants_suffix(&self) -> Option<&String>

pub fn as_transparent(&self) -> Option<()>

pub fn as_is_contract(&self) -> Option<(&String, &MaybeAssocItemId)>

pub fn as_has_contract(&self) -> Option<(&String, &FunDeclId)>

pub fn as_doc_comment(&self) -> Option<&String>

pub fn as_builtin(&self) -> Option<&AttributeKind>

pub fn as_unknown(&self) -> Option<&RawAttribute>

impl Attribute

pub fn as_opaque_mut(&mut self) -> Option<()>

pub fn as_exclude_mut(&mut self) -> Option<()>

pub fn as_rename_mut(&mut self) -> Option<&mut String>

pub fn as_variants_prefix_mut(&mut self) -> Option<&mut String>

pub fn as_variants_suffix_mut(&mut self) -> Option<&mut String>

pub fn as_transparent_mut(&mut self) -> Option<()>

pub fn as_is_contract_mut( &mut self, ) -> Option<(&mut String, &mut MaybeAssocItemId)>

pub fn as_has_contract_mut(&mut self) -> Option<(&mut String, &mut FunDeclId)>

pub fn as_doc_comment_mut(&mut self) -> Option<&mut String>

pub fn as_builtin_mut(&mut self) -> Option<&mut AttributeKind>

pub fn as_unknown_mut(&mut self) -> Option<&mut RawAttribute>

impl Attribute

pub fn to_opaque(self) -> Option<()>

pub fn to_exclude(self) -> Option<()>

pub fn to_rename(self) -> Option<String>

pub fn to_variants_prefix(self) -> Option<String>

pub fn to_variants_suffix(self) -> Option<String>

pub fn to_transparent(self) -> Option<()>

pub fn to_is_contract(self) -> Option<(String, MaybeAssocItemId)>

pub fn to_has_contract(self) -> Option<(String, FunDeclId)>

pub fn to_doc_comment(self) -> Option<String>

pub fn to_builtin(self) -> Option<AttributeKind>

pub fn to_unknown(self) -> Option<RawAttribute>

impl Attribute

fn fmt_unindented<C: AstFormatter>(&self, ctx: &C, f: &mut impl Write) -> Result

Trait Implementations

impl AstVisitable for Attribute

fn drive<V: VisitAst>(&self, v: &mut V) -> ControlFlow<V::Break>

Recursively visit this type with the provided visitor. This calls the visitor’s visit_$any method if it exists, otherwise visit_inner.

fn drive_mut<V: VisitAstMut>(&mut self, v: &mut V) -> ControlFlow<V::Break>

Recursively visit this type with the provided visitor. This calls the visitor’s visit_$any method if it exists, otherwise visit_inner.

fn drive_two<V: ZipAst>(&self, other: &Self, v: &mut V) -> ControlFlow<V::Break>

Recursively visit this type with the provided visitor. This calls the visitor’s visit_$any method if it exists, otherwise visit_inner.

fn name(&self) -> &'static str

The name of the type, used for debug logging.

fn dyn_visit<T: AstVisitable>(&self, f: impl FnMut(&T))

where Self: Sized,

Visit all occurrences of that type inside self, in pre-order traversal.

fn dyn_visit_mut<T: AstVisitable>(&mut self, f: impl FnMut(&mut T))

where Self: Sized,

Visit all occurrences of that type inside self, in pre-order traversal.

impl Clone for Attribute

fn clone(&self) -> Attribute

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Attribute

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Attribute

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl<'s, V> Drive<'s, V> for Attribute

where V: Visitor + Visit<'s, String> + Visit<'s, MaybeAssocItemId> + Visit<'s, FunDeclId> + Visit<'s, RawAttribute>,

fn drive_inner(&'s self, visitor: &mut V) -> ControlFlow<V::Break>

Call v.visit() on the immediate contents of self.

impl<'s, V> DriveMut<'s, V> for Attribute

where V: Visitor + VisitMut<'s, String> + VisitMut<'s, MaybeAssocItemId> + VisitMut<'s, FunDeclId> + VisitMut<'s, RawAttribute>,

fn drive_inner_mut(&'s mut self, visitor: &mut V) -> ControlFlow<V::Break>

Call v.visit() on the immediate contents of self.

impl<'s, V> DriveTwo<'s, V> for Attribute

where V: Visitor<Break: Default> + VisitTwo<'s, String> + VisitTwo<'s, MaybeAssocItemId> + VisitTwo<'s, FunDeclId> + VisitTwo<'s, RawAttribute>,

fn drive_two_inner( &'s self, other: &'s Self, visitor: &mut V, ) -> ControlFlow<V::Break>

Call v.visit() on the immediate contents of self and other, if they correspond. If the values don’t match up, this returns Break(Default::default()).

impl Eq for Attribute

impl<C: AstFormatter> FmtWithCtx<C> for Attribute

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

fn with_ctx<'a>(&'a self, ctx: &'a C) -> WithCtx<'a, C, Self>

Returns a struct that implements Display. This allows the following:

fn to_string_with_ctx(&self, ctx: &C) -> String

impl PartialEq for Attribute

fn eq(&self, other: &Attribute) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl Serialize for Attribute

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for Attribute