Enum Attribute

pub enum Attribute {
    Opaque,
    Rename(String),
    VariantsPrefix(String),
    VariantsSuffix(String),
    DocComment(String),
    Unknown(RawAttribute),
}

Attributes (#[...]).

Variants

Opaque

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

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.

DocComment(String)

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

Unknown(RawAttribute)

A non-charon-specific attribute.

Implementations

impl Attribute

pub fn is_opaque(&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_doc_comment(&self) -> bool

pub fn is_unknown(&self) -> bool

impl Attribute

pub fn as_opaque(&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_doc_comment(&self) -> Option<&String>

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

impl Attribute

pub fn as_opaque_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_doc_comment_mut(&mut self) -> Option<&mut String>

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

impl Attribute

pub fn to_opaque(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_doc_comment(self) -> Option<String>

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

impl Attribute

pub fn parse_from_raw(raw_attr: RawAttribute) -> Result<Self, String>

Parse a raw attribute to recognize our special charon::* and aeneas::* attributes.

fn parse_special_attr( attr_name: &str, args: Option<&str>, ) -> Result<Option<Self>, String>

Parse a charon::* or aeneas::* attribute.

Trait Implementations

impl Clone for Attribute

fn clone(&self) -> Attribute

Returns a copy 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 Drive for Attribute

fn drive<V: Visitor>(&self, visitor: &mut V)

impl DriveMut for Attribute

fn drive_mut<V: VisitorMut>(&mut self, visitor: &mut V)

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