Enum Attribute 

pub enum Attribute {
    Opaque,
    Exclude,
    Rename(String),
    VariantsPrefix(String),
    VariantsSuffix(String),
    Transparent,
    IsPrecondition(ItemId),
    IsPostcondition(ItemId),
    HasPrecondition(FunDeclId),
    HasPostcondition(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].

IsPrecondition(ItemId)

An item annotated with #[charon::precondition]. This makes it a precondition for its parent item.

IsPostcondition(ItemId)

An item annotated with #[charon::postcondition]. This makes it a postcondition for its parent item.

HasPrecondition(FunDeclId)

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

HasPostcondition(FunDeclId)

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

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_precondition(&self) -> bool

pub fn is_is_postcondition(&self) -> bool

pub fn is_has_precondition(&self) -> bool

pub fn is_has_postcondition(&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_precondition(&self) -> Option<&ItemId>

pub fn as_is_postcondition(&self) -> Option<&ItemId>

pub fn as_has_precondition(&self) -> Option<&FunDeclId>

pub fn as_has_postcondition(&self) -> Option<&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_precondition_mut(&mut self) -> Option<&mut ItemId>

pub fn as_is_postcondition_mut(&mut self) -> Option<&mut ItemId>

pub fn as_has_precondition_mut(&mut self) -> Option<&mut FunDeclId>

pub fn as_has_postcondition_mut(&mut self) -> Option<&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_precondition(self) -> Option<ItemId>

pub fn to_is_postcondition(self) -> Option<ItemId>

pub fn to_has_precondition(self) -> Option<FunDeclId>

pub fn to_has_postcondition(self) -> Option<FunDeclId>

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

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

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

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, ItemId> + 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, ItemId> + 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, ItemId> + 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 PartialEq for Attribute

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

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 Eq for Attribute

impl StructuralPartialEq for Attribute