Struct TranslatedCrate

pub struct TranslatedCrate {
    pub crate_name: String,
    pub real_crate_name: String,
    pub options: CliOpts,
    pub all_ids: IndexSet<AnyTransId>,
    pub item_names: HashMap<AnyTransId, Name>,
    pub files: Vector<FileId, File>,
    pub type_decls: Vector<TypeDeclId, TypeDecl>,
    pub fun_decls: Vector<FunDeclId, FunDecl>,
    pub global_decls: Vector<GlobalDeclId, GlobalDecl>,
    pub trait_decls: Vector<TraitDeclId, TraitDecl>,
    pub trait_impls: Vector<TraitImplId, TraitImpl>,
    pub ordered_decls: Option<DeclarationsGroups>,
}

The data of a translated crate.

Fields

crate_name: String

The name that the user requested for the crate. This may differ from what rustc reports as the name of the crate.

real_crate_name: String

The name of the crate according to rustc.

options: CliOpts

The options used when calling Charon. It is useful for the applications which consumed the serialized code, to check that Charon was called with the proper options.

all_ids: IndexSet<AnyTransId>

All the item ids, in the order in which we encountered them

item_names: HashMap<AnyTransId, Name>

The names of all registered items. Available so we can know the names even of items that failed to translate. Invariant: after translation, any existing AnyTransId must have an associated name, even if the corresponding item wasn’t translated.

files: Vector<FileId, File>

The translated files.

type_decls: Vector<TypeDeclId, TypeDecl>

The translated type definitions

fun_decls: Vector<FunDeclId, FunDecl>

The translated function definitions

global_decls: Vector<GlobalDeclId, GlobalDecl>

The translated global definitions

trait_decls: Vector<TraitDeclId, TraitDecl>

The translated trait declarations

trait_impls: Vector<TraitImplId, TraitImpl>

The translated trait declarations

ordered_decls: Option<DeclarationsGroups>

The re-ordered groups of declarations, initialized as empty.

Implementations

impl TranslatedCrate

pub fn item_name(&self, trans_id: impl Into<AnyTransId>) -> Option<&Name>

pub fn get_item( &self, trans_id: impl Into<AnyTransId>, ) -> Option<AnyTransItem<'_>>

pub fn get_item_mut( &mut self, trans_id: AnyTransId, ) -> Option<AnyTransItemMut<'_>>

pub fn all_items(&self) -> impl Iterator<Item = AnyTransItem<'_>>

pub fn all_items_with_ids( &self, ) -> impl Iterator<Item = (AnyTransId, AnyTransItem<'_>)>

pub fn all_items_mut(&mut self) -> impl Iterator<Item = AnyTransItemMut<'_>>

Trait Implementations

impl AstVisitable for TranslatedCrate

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 TranslatedCrate

fn clone(&self) -> TranslatedCrate

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Default for TranslatedCrate

fn default() -> TranslatedCrate

Returns the “default value” for a type.

impl<'de> Deserialize<'de> for TranslatedCrate

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for TranslatedCrate

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

Formats the value using the given formatter.

impl<'s, V> Drive<'s, V> for TranslatedCrate

where V: Visitor + Visit<'s, HashMap<AnyTransId, Name>> + Visit<'s, Vector<TypeDeclId, TypeDecl>> + Visit<'s, Vector<FunDeclId, FunDecl>> + Visit<'s, Vector<GlobalDeclId, GlobalDecl>> + Visit<'s, Vector<TraitDeclId, TraitDecl>> + Visit<'s, Vector<TraitImplId, TraitImpl>>,

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 TranslatedCrate

where V: Visitor + VisitMut<'s, HashMap<AnyTransId, Name>> + VisitMut<'s, Vector<TypeDeclId, TypeDecl>> + VisitMut<'s, Vector<FunDeclId, FunDecl>> + VisitMut<'s, Vector<GlobalDeclId, GlobalDecl>> + VisitMut<'s, Vector<TraitDeclId, TraitDecl>> + VisitMut<'s, Vector<TraitImplId, TraitImpl>>,

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

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

impl HasVectorOf<FunDeclId> for TranslatedCrate

fn get_vector(&self) -> &Vector<FunDeclId, Self::Output>

fn get_vector_mut(&mut self) -> &mut Vector<FunDeclId, Self::Output>

impl HasVectorOf<GlobalDeclId> for TranslatedCrate

fn get_vector(&self) -> &Vector<GlobalDeclId, Self::Output>

fn get_vector_mut(&mut self) -> &mut Vector<GlobalDeclId, Self::Output>

impl HasVectorOf<TraitDeclId> for TranslatedCrate

fn get_vector(&self) -> &Vector<TraitDeclId, Self::Output>

fn get_vector_mut(&mut self) -> &mut Vector<TraitDeclId, Self::Output>

impl HasVectorOf<TraitImplId> for TranslatedCrate

fn get_vector(&self) -> &Vector<TraitImplId, Self::Output>

fn get_vector_mut(&mut self) -> &mut Vector<TraitImplId, Self::Output>

impl HasVectorOf<TypeDeclId> for TranslatedCrate

fn get_vector(&self) -> &Vector<TypeDeclId, Self::Output>

fn get_vector_mut(&mut self) -> &mut Vector<TypeDeclId, Self::Output>

impl Index<FunDeclId> for TranslatedCrate

type Output = FunDecl

The returned type after indexing.

fn index(&self, index: FunDeclId) -> &Self::Output

Performs the indexing (container[index]) operation.

impl Index<GlobalDeclId> for TranslatedCrate

type Output = GlobalDecl

The returned type after indexing.

fn index(&self, index: GlobalDeclId) -> &Self::Output

Performs the indexing (container[index]) operation.

impl Index<TraitDeclId> for TranslatedCrate

type Output = TraitDecl

The returned type after indexing.

fn index(&self, index: TraitDeclId) -> &Self::Output

Performs the indexing (container[index]) operation.

impl Index<TraitImplId> for TranslatedCrate

type Output = TraitImpl

The returned type after indexing.

fn index(&self, index: TraitImplId) -> &Self::Output

Performs the indexing (container[index]) operation.

impl Index<TypeDeclId> for TranslatedCrate

type Output = TypeDecl

The returned type after indexing.

fn index(&self, index: TypeDeclId) -> &Self::Output

Performs the indexing (container[index]) operation.

impl IndexMut<FunDeclId> for TranslatedCrate

fn index_mut(&mut self, index: FunDeclId) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl IndexMut<GlobalDeclId> for TranslatedCrate

fn index_mut(&mut self, index: GlobalDeclId) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl IndexMut<TraitDeclId> for TranslatedCrate

fn index_mut(&mut self, index: TraitDeclId) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl IndexMut<TraitImplId> for TranslatedCrate

fn index_mut(&mut self, index: TraitImplId) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl IndexMut<TypeDeclId> for TranslatedCrate

fn index_mut(&mut self, index: TypeDeclId) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl<'tcx, 'ctx, 'a> IntoFormatter for &'a TranslatedCrate

type C = FmtCtx<'a>

fn into_fmt(self) -> Self::C

impl Serialize for TranslatedCrate

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

where __S: Serializer,

Serialize this value into the given Serde serializer.