Enum ItemOpacity 

pub enum ItemOpacity {
    Transparent,
    Foreign,
    Opaque,
    Invisible,
}

How much to translate for a given item.

Variants

Transparent

Translate the item fully.

Foreign

Translate the item depending on the normal rust visibility of its contents: for types, we translate fully if it is a struct with public fields or an enum; for other items this is equivalent to Opaque.

Opaque

Translate the item name and signature, but not its contents. 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.

Invisible

Translate nothing of this item. The corresponding map will not have an entry for the ItemId. Useful when even the signature of the item causes errors.

Implementations

impl ItemOpacity

pub fn is_transparent(&self) -> bool

pub fn is_foreign(&self) -> bool

pub fn is_opaque(&self) -> bool

pub fn is_invisible(&self) -> bool

impl ItemOpacity

pub fn with_content_visibility(self, contents_are_public: bool) -> Self

pub fn with_private_contents(self) -> Self

Trait Implementations

impl AstVisitable for ItemOpacity

where ItemOpacity: PartialEq,

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 ItemOpacity

fn clone(&self) -> ItemOpacity

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for ItemOpacity

impl Debug for ItemOpacity

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ItemOpacity

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 ItemOpacity

where V: Visitor,

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 ItemOpacity

where V: Visitor,

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 ItemOpacity

where V: Visitor<Break: Default>,

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 ItemOpacity

impl Ord for ItemOpacity

fn cmp(&self, other: &ItemOpacity) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl PartialEq for ItemOpacity

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

Equality operator ==.

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

Inequality operator !=.

impl PartialOrd for ItemOpacity

fn partial_cmp(&self, other: &ItemOpacity) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

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

Tests less than (for self and other) and is used by the < operator.

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

Tests less than or equal to (for self and other) and is used by the <= operator.

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

Tests greater than (for self and other) and is used by the > operator.

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

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl Serialize for ItemOpacity

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 ItemOpacity