Struct TranslatedCrate 

pub struct TranslatedCrate {

    pub crate_name: String,
    pub options: CliOpts,
    pub target_information: SeqHashMap<TargetTriple, TargetInfo>,
    pub files: IndexVec<FileId, File>,
    pub item_names: SeqHashMap<ItemId, Name>,
    pub assoc_item_names: IndexMap<TraitDeclId, AssocItemNames>,
    pub short_names: SeqHashMap<ItemId, Name>,
    pub type_decls: IndexMap<TypeDeclId, TypeDecl>,
    pub fun_decls: IndexMap<FunDeclId, FunDecl>,
    pub global_decls: IndexMap<GlobalDeclId, GlobalDecl>,
    pub trait_decls: IndexMap<TraitDeclId, TraitDecl>,
    pub trait_impls: IndexMap<TraitImplId, TraitImpl>,
    pub ordered_decls: Option<DeclarationsGroups>,
}

The complete data of a Rust crate.

A crate is mainly composed of 5 kinds of items:

• Functions;
• Type definitions;
• Globals (constants and statics);
• Trait declarations;
• Trait implementations.

These can each be found in the corresponding IndexVec. They are in an unspecified (though deterministic) order. If you need a more robust order, see ordered_decls.

To get a TranslatedCrate, run charon cargo inside a Rust crate, then deserialize the resulting crate_name.llbc file using crate::deserialize_llbc.

Fields

crate_name: String

The name of the crate.

options: CliOpts

The options used when calling Charon. Can be used to check that Charon was called with the options that a given consumer requires.

target_information: SeqHashMap<TargetTriple, TargetInfo>

Information about each target platform for which the crate was translated. When translating a crate normally this will have a single entry; when using --targets this will have one entry per chosen target.

files: IndexVec<FileId, File>

The source files composing the crate and its dependencies. Each Span refers to a byte range within one of these files.

item_names: SeqHashMap<ItemId, 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 ItemId must have an associated name, even if the corresponding item wasn’t translated.

assoc_item_names: IndexMap<TraitDeclId, AssocItemNames>

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

short_names: SeqHashMap<ItemId, Name>

Short names, for items whose last PathElem is unique.

type_decls: IndexMap<TypeDeclId, TypeDecl>

The type definitions (structs, enums, …).

fun_decls: IndexMap<FunDeclId, FunDecl>

The function definitions.

Each item with a body becomes a function: actual functions, methods, and unevaluated consts/statics.

global_decls: IndexMap<GlobalDeclId, GlobalDecl>

The global definitions, which are constants, statics, and thread locals.

trait_decls: IndexMap<TraitDeclId, TraitDecl>

The trait declarations.

trait_impls: IndexMap<TraitImplId, TraitImpl>

The trait implementations.

ordered_decls: Option<DeclarationsGroups>

This contains a list of all the reachable items in the crate in a stable, logical order based on crate and file order, then further grouped and sorted such that every item comes after the items it depends on. Mutually-dependent groups of items are identified as such. This is meant for code-generation tools that want a stable output order.

Not all the items in the TranslatedCrate are included: some trait impls are never referred to by reachable items so could in principle be removed from the crate, but we keep them around to be able to tell method implementations apart.

Always Some after translation.

Implementations

impl TranslatedCrate

pub fn item_name(&self, id: impl Into<ItemId>) -> &Name

pub fn assoc_item_name( &self, trait_id: TraitDeclId, id: impl Into<AssocItemId>, ) -> TraitItemName

pub fn item_short_name(&self, id: impl Into<ItemId>) -> &Name

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

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

pub fn remove_item(&mut self, trans_id: ItemId) -> Option<ItemByVal>

Remove this item from the crate, including the name information about it.

See also TranslatedCrate::remove_item_temporarily.

pub fn set_new_item_slot(&mut self, id: ItemId, item: impl Into<ItemByVal>)

Insert a new item into a slot, and record its name in the name map.

pub fn remove_item_temporarily(&mut self, trans_id: ItemId) -> Option<ItemByVal>

Remove this item from the crate without touching the name maps. Useful for modifying items whilst being able to access the rest of the crate. Put the item back using TranslatedCrate::put_item_back.

See also TranslatedCrate::remove_item.

pub fn put_item_back(&mut self, id: ItemId, item: impl Into<ItemByVal>)

Insert the item into the corresponding slot without recording its name in the name map. Only use if the item already has its name registered, e.g. if you got it using TranslatedCrate::remove_item_temporarily.

pub fn all_ids(&self) -> impl Iterator<Item = ItemId> + use<>

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

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

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

pub fn the_target_information(&self) -> &TargetInfo

When translating without --target, there’s only one target information; this method retrieves it. Panics if this crate was translated in multi-target mode.

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 duplicate 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, __State: ?Sized + HashConsSerializerState> DeserializeState<'de, __State> for TranslatedCrate

fn deserialize_state<__D>( __state: &__State, __deserializer: __D, ) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

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, IndexVec<FileId, File>> + Visit<'s, SeqHashMap<ItemId, Name>> + Visit<'s, IndexMap<TraitDeclId, AssocItemNames>> + Visit<'s, IndexMap<TypeDeclId, TypeDecl>> + Visit<'s, IndexMap<FunDeclId, FunDecl>> + Visit<'s, IndexMap<GlobalDeclId, GlobalDecl>> + Visit<'s, IndexMap<TraitDeclId, TraitDecl>> + Visit<'s, IndexMap<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, IndexVec<FileId, File>> + VisitMut<'s, SeqHashMap<ItemId, Name>> + VisitMut<'s, IndexMap<TraitDeclId, AssocItemNames>> + VisitMut<'s, IndexMap<TypeDeclId, TypeDecl>> + VisitMut<'s, IndexMap<FunDeclId, FunDecl>> + VisitMut<'s, IndexMap<GlobalDeclId, GlobalDecl>> + VisitMut<'s, IndexMap<TraitDeclId, TraitDecl>> + VisitMut<'s, IndexMap<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 HasIdxMapOf<FunDeclId> for TranslatedCrate

fn get_idx_map(&self) -> &IndexMap<FunDeclId, Self::Output>

fn get_idx_map_mut(&mut self) -> &mut IndexMap<FunDeclId, Self::Output>

impl HasIdxMapOf<GlobalDeclId> for TranslatedCrate

fn get_idx_map(&self) -> &IndexMap<GlobalDeclId, Self::Output>

fn get_idx_map_mut(&mut self) -> &mut IndexMap<GlobalDeclId, Self::Output>

impl HasIdxMapOf<TraitDeclId> for TranslatedCrate

fn get_idx_map(&self) -> &IndexMap<TraitDeclId, Self::Output>

fn get_idx_map_mut(&mut self) -> &mut IndexMap<TraitDeclId, Self::Output>

impl HasIdxMapOf<TraitImplId> for TranslatedCrate

fn get_idx_map(&self) -> &IndexMap<TraitImplId, Self::Output>

fn get_idx_map_mut(&mut self) -> &mut IndexMap<TraitImplId, Self::Output>

impl HasIdxMapOf<TypeDeclId> for TranslatedCrate

fn get_idx_map(&self) -> &IndexMap<TypeDeclId, Self::Output>

fn get_idx_map_mut(&mut self) -> &mut IndexMap<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<'a> IntoFormatter for &'a TranslatedCrate

type C = FmtCtx<'a>

fn into_fmt(self) -> Self::C

impl<__State: ?Sized + HashConsSerializerState> SerializeState<__State> for TranslatedCrate

fn serialize_state<__S>( &self, __state: &__State, __serializer: __S, ) -> Result<__S::Ok, __S::Error>

where __S: Serializer,