Struct ItemMeta

pub struct ItemMeta {
    pub name: Name,
    pub span: Span,
    pub source_text: Option<String>,
    pub attr_info: AttrInfo,
    pub is_local: bool,
    pub opacity: ItemOpacity,
}

Meta information about an item (function, trait decl, trait impl, type decl, global).

Fields

name: Name

span: Span

source_text: Option<String>

The source code that corresponds to this item.

attr_info: AttrInfo

Attributes and visibility.

is_local: bool

true if the type decl is a local type decl, false if it comes from an external crate.

opacity: ItemOpacity

Whether this item is considered opaque. For function and globals, this means we don’t translate the body (the code); for ADTs, this means we don’t translate the fields/variants. For traits and trait impls, this doesn’t change anything. For modules, this means we don’t explore its contents (we still translate any of its items mentioned from somewhere else).

This can happen either if the item was annotated with #[charon::opaque] or if it was declared opaque via a command-line argument.

Implementations

impl ItemMeta

pub fn renamed_name(&self) -> Name

Trait Implementations

impl AstVisitable for ItemMeta

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 name(&self) -> &'static str

The name of the type, used for debug logging.

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

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

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

impl Clone for ItemMeta

fn clone(&self) -> ItemMeta

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for ItemMeta

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ItemMeta

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 ItemMeta

where V: Visitor + Visit<'s, Name> + Visit<'s, Span>,

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 ItemMeta

where V: Visitor + VisitMut<'s, Name> + VisitMut<'s, Span>,

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

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

impl Serialize for ItemMeta

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

where __S: Serializer,

Serialize this value into the given Serde serializer.