List of all items

Structs

• driver::CharonCallbacks
• driver::RunCompilerNormallyCallbacks
• hax::Adt
• hax::AdtTy
• hax::Alias
• hax::Align
• hax::ArrayTy
• hax::AssocConst
• hax::AssocFn
• hax::AssocItem
• hax::AssocTy
• hax::Binder
• hax::BoundRegion
• hax::BoundTy
• hax::BoundTyRef
• hax::ByteSymbol
• hax::Canonical
• hax::CanonicalUserTypeAnnotation
• hax::Clause
• hax::Closure
• hax::ClosureTy
• hax::CoercePredicate
• hax::Const
• hax::ConstOperand
• hax::ConstantExpr
• hax::ConstantFieldExpr
• hax::CoroutineTy
• hax::Ctor
• hax::DefId
• hax::DefIdContents
• hax::DisambiguatedDefPathItem
• hax::DiscriminantValue
• hax::DynBinder
• hax::DynTraitTy
• hax::EarlyParamRegion
• hax::ElaborationCtx
• hax::ExistentialProjection
• hax::ExistentialTraitRef
• hax::FieldDef
• hax::FieldIdx
• hax::Fn
• hax::FnDefTy
• hax::FnPointer
• hax::FnPtrShape
• hax::FnPtrTy
• hax::FnTraitImpls
• hax::ForeignMod
• hax::ForeignTy
• hax::FullDef
• hax::GenericParamDef
• hax::GenericPredicate
• hax::GenericPredicates
• hax::ImplAssocItem
• hax::ImplAssocItemValue
• hax::IndexVec
• hax::InherentImpl
• hax::ItemPredicate
• hax::ItemPredicates
• hax::ItemRef
• hax::ItemRefContents
• hax::LateParamRegion
• hax::MacroKinds
• hax::Mod
• hax::OutlivesPredicate
• hax::ParamConst
• hax::ParamEnv
• hax::ParamTy
• hax::PatTy
• hax::PathBuf
• hax::Placeholder
• hax::Predicate
• hax::ProjectionPredicate
• hax::PromotedId
• hax::RAllocId
• hax::RDefId
• hax::RawPtrTy
• hax::Rc
• hax::RefTy
• hax::Region
• hax::ReprFlags
• hax::ReprOptions
• hax::SliceTy
• hax::Span
• hax::Spanned
• hax::Static
• hax::StrTy
• hax::SubtypePredicate
• hax::Symbol
• hax::SyntheticItemData
• hax::Trait
• hax::TraitAlias
• hax::TraitImpl
• hax::TraitItemBinder
• hax::TraitPredicate
• hax::TraitProof
• hax::TraitProofContents
• hax::TupleTy
• hax::Ty
• hax::TyAlias
• hax::TyFnSig
• hax::TyGenerics
• hax::TypeAndMut
• hax::UserArgs
• hax::UserSelfTy
• hax::VariantDef
• hax::VariantIdx
• hax::VirtualImplAssocItem
• hax::VirtualTraitImpl
• hax::VirtualTraitMethod
• hax::constant_utils::ConstantExpr
• hax::constant_utils::ConstantFieldExpr
• hax::constant_utils::VariantIdx
• hax::mir_kinds::CTFE
• hax::mir_kinds::Optimized
• hax::mir_kinds::Unknown
• hax::options::BoundsOptions
• hax::options::Options
• hax::prelude::IndexVec
• hax::prelude::PathBuf
• hax::prelude::RDefId
• hax::prelude::Rc
• hax::state::Base
• hax::state::GlobalCache
• hax::state::ItemCache
• hax::state::LocalContextS
• hax::state::State
• hax::state::base::Base
• hax::state::base::GlobalCache
• hax::state::base::ItemCache
• hax::state::base::LocalContextS
• hax::traits::ElaborationCtx
• hax::traits::ItemPredicate
• hax::traits::ItemPredicates
• hax::traits::TraitProof
• hax::traits::TraitProofContents
• hax::types::Span
• hax::types::Spanned
• hax::types::adt::Align
• hax::types::adt::DiscriminantValue
• hax::types::adt::FieldDef
• hax::types::adt::ReprFlags
• hax::types::adt::ReprOptions
• hax::types::adt::VariantDef
• hax::types::def_id::ByteSymbol
• hax::types::def_id::DefId
• hax::types::def_id::DefIdContents
• hax::types::def_id::DisambiguatedDefPathItem
• hax::types::def_id::MacroKinds
• hax::types::def_id::PromotedId
• hax::types::def_id::RAllocId
• hax::types::def_id::Symbol
• hax::types::def_id::VirtualImplAssocItem
• hax::types::mir::ConstOperand
• hax::types::mir::FieldIdx
• hax::types::mir::mir_kinds::CTFE
• hax::types::mir::mir_kinds::Optimized
• hax::types::mir::mir_kinds::Unknown
• hax::types::new::full_def::Adt
• hax::types::new::full_def::AssocConst
• hax::types::new::full_def::AssocFn
• hax::types::new::full_def::AssocTy
• hax::types::new::full_def::Closure
• hax::types::new::full_def::Const
• hax::types::new::full_def::Ctor
• hax::types::new::full_def::Fn
• hax::types::new::full_def::FnPointer
• hax::types::new::full_def::FnTraitImpls
• hax::types::new::full_def::ForeignMod
• hax::types::new::full_def::FullDef
• hax::types::new::full_def::ImplAssocItem
• hax::types::new::full_def::ImplAssocItemValue
• hax::types::new::full_def::InherentImpl
• hax::types::new::full_def::Mod
• hax::types::new::full_def::ParamEnv
• hax::types::new::full_def::Static
• hax::types::new::full_def::Trait
• hax::types::new::full_def::TraitAlias
• hax::types::new::full_def::TraitImpl
• hax::types::new::full_def::TraitItemBinder
• hax::types::new::full_def::TyAlias
• hax::types::new::full_def::VirtualTraitImpl
• hax::types::new::full_def::VirtualTraitMethod
• hax::types::new::item_ref::ItemRef
• hax::types::new::item_ref::ItemRefContents
• hax::types::new::synthetic_items::FnPtrShape
• hax::types::new::synthetic_items::GenericParamDefIds
• hax::types::new::synthetic_items::SyntheticItemData
• hax::types::predicates::Clause
• hax::types::predicates::CoercePredicate
• hax::types::predicates::ExistentialProjection
• hax::types::predicates::ExistentialTraitRef
• hax::types::predicates::GenericPredicate
• hax::types::predicates::GenericPredicates
• hax::types::predicates::OutlivesPredicate
• hax::types::predicates::Predicate
• hax::types::predicates::ProjectionPredicate
• hax::types::predicates::SubtypePredicate
• hax::types::predicates::TraitPredicate
• hax::types::traits::AssocItem
• hax::types::ty::AdtTy
• hax::types::ty::Alias
• hax::types::ty::ArrayTy
• hax::types::ty::CanonicalUserTypeAnnotation
• hax::types::ty::ClosureTy
• hax::types::ty::CoroutineTy
• hax::types::ty::DynTraitTy
• hax::types::ty::FnDefTy
• hax::types::ty::FnPtrTy
• hax::types::ty::ForeignTy
• hax::types::ty::PatTy
• hax::types::ty::RawPtrTy
• hax::types::ty::RefTy
• hax::types::ty::SliceTy
• hax::types::ty::StrTy
• hax::types::ty::TupleTy
• hax::types::ty::Ty
• hax::types::ty::TyFnSig
• hax::types::ty::TypeAndMut
• hax::types::ty::UserArgs
• hax::types::ty::UserSelfTy
• hax::types::vars::Binder
• hax::types::vars::BoundRegion
• hax::types::vars::BoundTy
• hax::types::vars::BoundTyRef
• hax::types::vars::Canonical
• hax::types::vars::DynBinder
• hax::types::vars::EarlyParamRegion
• hax::types::vars::GenericParamDef
• hax::types::vars::LateParamRegion
• hax::types::vars::ParamConst
• hax::types::vars::ParamTy
• hax::types::vars::Placeholder
• hax::types::vars::Region
• hax::types::vars::TyGenerics
• toolchain::Toolchain
• toolchain::ToolchainFile
• translate::translate_bodies::BlockTransCtx
• translate::translate_bodies::BodyTransCtx
• translate::translate_closures::Callable
• translate::translate_closures::CallableFnImpls
• translate::translate_crate::TransItemSource
• translate::translate_ctx::DepSource
• translate::translate_ctx::ErrorCtx
• translate::translate_ctx::ItemTransCtx
• translate::translate_ctx::Level
• translate::translate_ctx::TranslateCtx
• translate::translate_generics::BindingLevel
• translate::translate_generics::LifetimeMutabilityComputer
• translate::translate_trait_objects::VTableData
• translate::translate_trait_objects::VTableInstanceData
• translate::user_type_annotations::UserTypeAnnotation
• translate::user_type_annotations::UserTypeAnnotations

Enums

• CharonFailure
• hax::AdtKind
• hax::AliasKind
• hax::AssocItemContainer
• hax::AssocItemResolution
• hax::AssocKind
• hax::AssocTypeData
• hax::BoundRegionKind
• hax::BoundTyKind
• hax::BoundVarIndexKind
• hax::BoundVariableKind
• hax::BuiltinTraitData
• hax::ClauseKind
• hax::ClosureKind
• hax::ConstKind
• hax::ConstOperandKind
• hax::ConstSource
• hax::ConstantByte
• hax::ConstantByteProvenance
• hax::ConstantExprKind
• hax::ConstantInt
• hax::ConstantLiteral
• hax::ConstantProjectionElem
• hax::ConstantPtrBase
• hax::CtorKind
• hax::CtorOf
• hax::DefIdBase
• hax::DefKind
• hax::DefPathItem
• hax::DestructData
• hax::DiscriminantDefinition
• hax::ErrorGuaranteed
• hax::ExistentialPredicate
• hax::ExternAbi
• hax::FloatTy
• hax::FnPtrTarget
• hax::FullDefKind
• hax::GenericArg
• hax::GenericParamDefKind
• hax::GenericPredicateId
• hax::GlobalRef
• hax::HostEffectClause
• hax::ImplTraitInTraitData
• hax::InferTy
• hax::InlineAttr
• hax::IntTy
• hax::ItemPredicateId
• hax::LateParamRegionKind
• hax::LitIntType
• hax::Mutability
• hax::NormalizesTo
• hax::Pattern
• hax::PredicateDirection
• hax::PredicateKind
• hax::RDefKind
• hax::ReadMode
• hax::RegionKind
• hax::Safety
• hax::SolverTraitLangItem
• hax::SyntheticItem
• hax::Term
• hax::TraitProofImpliedPredicate
• hax::TraitProofKind
• hax::TyKind
• hax::UintTy
• hax::UnsizingMetadata
• hax::UserType
• hax::Variance
• hax::VariantKind
• hax::Visibility
• hax::constant_utils::ConstSource
• hax::constant_utils::ConstantByte
• hax::constant_utils::ConstantByteProvenance
• hax::constant_utils::ConstantExprKind
• hax::constant_utils::ConstantInt
• hax::constant_utils::ConstantLiteral
• hax::constant_utils::ConstantProjectionElem
• hax::constant_utils::ConstantPtrBase
• hax::constant_utils::FnPtrTarget
• hax::constant_utils::GlobalRef
• hax::constant_utils::ReadMode
• hax::constant_utils::VariantKind
• hax::prelude::RDefKind
• hax::traits::AssocItemResolution
• hax::traits::BuiltinTraitData
• hax::traits::DestructData
• hax::traits::ItemPredicateId
• hax::traits::PredicateDirection
• hax::traits::SolverTraitLangItem
• hax::traits::TraitProofImpliedPredicate
• hax::traits::TraitProofKind
• hax::types::ErrorGuaranteed
• hax::types::adt::AdtKind
• hax::types::adt::DiscriminantDefinition
• hax::types::adt::Visibility
• hax::types::def_id::CtorKind
• hax::types::def_id::CtorOf
• hax::types::def_id::DefIdBase
• hax::types::def_id::DefKind
• hax::types::def_id::DefPathItem
• hax::types::def_id::Mutability
• hax::types::def_id::Safety
• hax::types::mir::ConstOperandKind
• hax::types::new::full_def::ConstKind
• hax::types::new::full_def::FullDefKind
• hax::types::new::full_def::InlineAttr
• hax::types::new::synthetic_items::SyntheticItem
• hax::types::predicates::ClauseKind
• hax::types::predicates::ExistentialPredicate
• hax::types::predicates::GenericPredicateId
• hax::types::predicates::HostEffectClause
• hax::types::predicates::NormalizesTo
• hax::types::predicates::PredicateKind
• hax::types::predicates::Term
• hax::types::traits::AssocItemContainer
• hax::types::traits::AssocKind
• hax::types::traits::AssocTypeData
• hax::types::traits::ImplTraitInTraitData
• hax::types::ty::AliasKind
• hax::types::ty::ClosureKind
• hax::types::ty::ExternAbi
• hax::types::ty::FloatTy
• hax::types::ty::IntTy
• hax::types::ty::LitIntType
• hax::types::ty::Pattern
• hax::types::ty::TyKind
• hax::types::ty::UintTy
• hax::types::ty::UnsizingMetadata
• hax::types::ty::UserType
• hax::types::vars::BoundRegionKind
• hax::types::vars::BoundTyKind
• hax::types::vars::BoundVarIndexKind
• hax::types::vars::BoundVariableKind
• hax::types::vars::GenericArg
• hax::types::vars::GenericParamDefKind
• hax::types::vars::InferTy
• hax::types::vars::LateParamRegionKind
• hax::types::vars::RegionKind
• hax::types::vars::Variance
• translate::translate_closures::CallableKind
• translate::translate_crate::RustcItem
• translate::translate_crate::TransImplSource
• translate::translate_crate::TransItemSourceKind
• translate::translate_ctx::ContainmentNode
• translate::translate_ctx::ItemOrModuleId
• translate::translate_ctx::MethodStatus
• translate::translate_items::TraitItemSource
• translate::translate_meta::ContractTarget
• translate::translate_trait_objects::TrVTableField
• translate::translate_trait_objects::VTableMethodSource
• translate::translate_trait_objects::VtableMethodValue

Traits

• hax::IsMirKind
• hax::ItemId
• hax::SInto
• hax::SubstBinder
• hax::ToPolyTraitRef
• hax::mir_kinds::IsMirKind
• hax::rustc::SubstBinder
• hax::rustc_utils::SubstBinder
• hax::sinto::SInto
• hax::state::BaseState
• hax::state::UnderOwnerState
• hax::traits::ItemId
• hax::traits::ToPolyTraitRef
• hax::types::mir::mir_kinds::rustc::IsMirKind
• hax::types::vars::BinderVariances

Macros

• hax::sinto::sinto_clone
• hax::sinto_as_usize
• hax::sinto_reexport
• hax::sinto_todo
• sinto_as_usize
• sinto_reexport
• sinto_todo
• translate::translate_ctx::error_assert
• translate::translate_ctx::raise_error
• translate::translate_ctx::register_error

Derive Macros

• hax::AdtInto

Functions

• driver::check_late_rustc_errors
• driver::def_id_debug
• driver::precheck_rustc_errors
• driver::run_compiler_with_callbacks
• driver::run_rustc_driver
• driver::set_mir_options
• driver::set_parallel_frontend
• driver::set_skip_borrowck
• driver::setup_compiler
• driver::skip_borrowck_if_set
• hax::alias_ty_kind_def_id
• hax::assoc_tys_for_trait
• hax::closure_once_shim
• hax::closure_sig
• hax::compute_unsizing_metadata
• hax::constant_utils::uneval::bits_and_type_to_float_constant_literal
• hax::constant_utils::uneval::const_reader
• hax::constant_utils::uneval::read_const
• hax::constant_utils::uneval::scalar_int_to_constant_literal
• hax::constant_utils::uneval::unsizing_metadata
• hax::drop_glue_shim
• hax::dyn_self_ty
• hax::erase_and_norm
• hax::erase_free_regions
• hax::fn_sig_bound_region_variances
• hax::get_foreign_mod_children
• hax::get_method_sig
• hax::get_mod_children
• hax::identity_args_with_inferred
• hax::inst_binder
• hax::name_of_local
• hax::normalize
• hax::read_const
• hax::rustc::assoc_tys_for_trait
• hax::rustc::closure_once_shim
• hax::rustc::drop_glue_shim
• hax::rustc::dyn_self_ty
• hax::rustc::fn_sig_bound_region_variances
• hax::rustc::get_foreign_mod_children
• hax::rustc::get_method_sig
• hax::rustc::get_mod_children
• hax::rustc::identity_args_with_inferred
• hax::rustc::inst_binder
• hax::rustc::substitute
• hax::rustc::translate_user_annotation
• hax::rustc::unerase_lifetimes
• hax::rustc_utils::assoc_tys_for_trait
• hax::rustc_utils::can_have_generics
• hax::rustc_utils::closure_once_shim
• hax::rustc_utils::drop_glue_shim
• hax::rustc_utils::dyn_self_ty
• hax::rustc_utils::fn_sig_bound_region_variances
• hax::rustc_utils::get_foreign_mod_children
• hax::rustc_utils::get_method_sig
• hax::rustc_utils::get_mod_children
• hax::rustc_utils::get_variant_kind
• hax::rustc_utils::identity_args_with_inferred
• hax::rustc_utils::inst_binder
• hax::rustc_utils::substitute
• hax::rustc_utils::translate_user_annotation
• hax::rustc_utils::unerase_lifetimes
• hax::self_clause_for_item
• hax::self_predicate
• hax::solve_copy
• hax::solve_destruct
• hax::solve_item_implied_traits
• hax::solve_sized
• hax::solve_trait
• hax::substitute
• hax::super_clause_to_clause_and_trait_proof
• hax::traits::erase_and_norm
• hax::traits::erase_free_regions
• hax::traits::normalize
• hax::traits::self_clause_for_item
• hax::traits::self_predicate
• hax::traits::solve_copy
• hax::traits::solve_destruct
• hax::traits::solve_item_implied_traits
• hax::traits::solve_item_traits_inner
• hax::traits::solve_sized
• hax::traits::solve_trait
• hax::traits::super_clause_to_clause_and_trait_proof
• hax::traits::translate_item_ref
• hax::translate_item_ref
• hax::translate_user_annotation
• hax::types::def_id::get_def_kind
• hax::types::mir::name_of_local
• hax::types::mir::translate_mir_const
• hax::types::new::full_def::adjust_by_value_vtable_receiver
• hax::types::new::full_def::assoc_items_of
• hax::types::new::full_def::callable_trait_impls
• hax::types::new::full_def::fn_def_trait_impls
• hax::types::new::full_def::gen_vtable_sig
• hax::types::new::full_def::get_implied_predicates
• hax::types::new::full_def::get_param_env
• hax::types::new::full_def::get_self_predicate
• hax::types::new::full_def::get_trait_decl_dyn_self_ty
• hax::types::new::full_def::late_bound_for_def
• hax::types::new::full_def::self_trait_ref
• hax::types::new::full_def::translate_full_def
• hax::types::new::full_def::translate_full_def_kind
• hax::types::new::full_def::virtual_impl_for
• hax::types::new::full_def::vtable_receiver_is_by_value
• hax::types::new::full_def::vtable_sig_with_dyn_self
• hax::types::new::synthetic_items::lifetime_param_name
• hax::types::new::synthetic_items::type_param_name
• hax::types::predicates::resolve_for_dyn
• hax::types::ty::alias_ty_kind_def_id
• hax::types::ty::closure_sig
• hax::types::ty::compute_unsizing_metadata
• hax::unerase_lifetimes
• hax::vtable_receiver_is_by_value
• main
• run_charon
• toolchain::driver_cmd
• toolchain::driver_path
• toolchain::get_pinned_toolchain
• toolchain::in_toolchain
• toolchain::miri_sysroot_cache_dir
• toolchain::setup_miri_sysroot
• toolchain::sysroot_has_target
• toolchain::toolchain_path
• toolchain::toolchain_version
• translate::get_mir::get_mir_for_def_id_and_level
• translate::resolve_path::def_path_def_ids
• translate::resolve_path::find_primitive_impls
• translate::translate_closures::callable_virtual_impl
• translate::translate_closures::recognize_fn_trait_impl_proof
• translate::translate_closures::translate_closure_kind
• translate::translate_crate::translate
• translate::translate_ctx::catch_sinto
• translate::translate_generics::translate_region_name
• translate::translate_generics::translate_variance
• translate::translate_trait_objects::dynify
• translate::user_type_annotations::translate_user_annotation

Type Aliases

• hax::BoundVar
• hax::CanonicalUserType
• hax::DebruijnIndex
• hax::HashMap
• hax::Ident
• hax::PlaceholderConst
• hax::PlaceholderRegion
• hax::PlaceholderTy
• hax::PolyFnSig
• hax::PredicateSearcher
• hax::RegionOutlivesPredicate
• hax::RegionVid
• hax::TraitRef
• hax::TypeOutlivesPredicate
• hax::UnitBinder
• hax::UserAnnotation
• hax::UserAnnotationData
• hax::UserAnnotationProj
• hax::prelude::HashMap
• hax::rustc::UserAnnotation
• hax::rustc::UserAnnotationData
• hax::rustc::UserAnnotationProj
• hax::rustc_utils::UserAnnotation
• hax::rustc_utils::UserAnnotationData
• hax::rustc_utils::UserAnnotationProj
• hax::state::StateWithBase
• hax::state::StateWithOwner
• hax::traits::PredicateSearcher
• hax::types::Ident
• hax::types::predicates::RegionOutlivesPredicate
• hax::types::predicates::TypeOutlivesPredicate
• hax::types::traits::TraitRef
• hax::types::ty::PolyFnSig
• hax::types::vars::BoundVar
• hax::types::vars::CanonicalUserType
• hax::types::vars::DebruijnIndex
• hax::types::vars::PlaceholderConst
• hax::types::vars::PlaceholderRegion
• hax::types::vars::PlaceholderTy
• hax::types::vars::RegionVid
• hax::types::vars::UnitBinder

Statics

• driver::SKIP_BORROWCK
• toolchain::PINNED_TOOLCHAIN

Constants

• hax::types::def_id::SYNTHETIC_CRATE_NAME
• toolchain::CHARON_SYSROOT_VAR