Enum ItemOpacity

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

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 functions and globals this is equivalent to Opaque; for trait decls and impls this is equivalent to Transparent.

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 AnyTransId. 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 Clone for ItemOpacity

fn clone(&self) -> ItemOpacity

Returns a copy of the value.

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

Performs copy-assignment from source.

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 Drive for ItemOpacity

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

impl DriveMut for ItemOpacity

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

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

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 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 Copy for ItemOpacity

impl Eq for ItemOpacity

impl StructuralPartialEq for ItemOpacity