List of all items

Structs

• driver::CharonCallbacks
• driver::RunCompilerNormallyCallbacks
• hax::Alias
• hax::Align
• hax::AssocItem
• hax::Binder
• hax::BoundRegion
• hax::BoundTy
• hax::ByteSymbol
• hax::Canonical
• hax::CanonicalUserTypeAnnotation
• hax::Clause
• hax::ClosureArgs
• hax::CoercePredicate
• hax::ConstOperand
• hax::ConstantFieldExpr
• hax::Decorated
• hax::DefId
• hax::DefIdContents
• hax::DisambiguatedDefPathItem
• hax::DiscriminantValue
• hax::DynBinder
• hax::EarlyParamRegion
• hax::ExistentialProjection
• hax::ExistentialTraitRef
• hax::FieldDef
• hax::FieldIdx
• hax::FullDef
• hax::GenericParamDef
• hax::GenericPredicate
• hax::GenericPredicates
• hax::HashMap
• hax::ImplAssocItem
• hax::ImplExprContents
• hax::IndexVec
• hax::ItemPredicate
• hax::ItemPredicates
• hax::ItemRef
• hax::ItemRefContents
• hax::LateParamRegion
• hax::MacroKinds
• hax::OutlivesPredicate
• hax::ParamConst
• hax::ParamEnv
• hax::ParamTy
• hax::PathBuf
• hax::Placeholder
• hax::Predicate
• hax::PredicateSearcher
• hax::ProjectionPredicate
• hax::PromotedId
• hax::RDefId
• hax::Rc
• hax::Region
• hax::ReprFlags
• hax::ReprOptions
• hax::Span
• hax::Spanned
• hax::SubtypePredicate
• hax::Symbol
• hax::TraitPredicate
• hax::Ty
• hax::TyFnSig
• hax::TyGenerics
• hax::TypeAndMut
• hax::TypeMap
• hax::UserArgs
• hax::UserSelfTy
• hax::VariantDef
• hax::VariantIdx
• hax::VirtualTraitImpl
• hax::constant_utils::ConstantFieldExpr
• hax::constant_utils::VariantIdx
• hax::index_vec::IndexVec
• hax::mir_kinds::CTFE
• hax::mir_kinds::Optimized
• hax::mir_kinds::Unknown
• hax::options::BoundsOptions
• hax::options::Options
• hax::prelude::HashMap
• hax::prelude::PathBuf
• hax::prelude::RDefId
• hax::prelude::Rc
• hax::rustc::TypeMap
• hax::state::Base
• hax::state::GlobalCache
• hax::state::ItemCache
• hax::state::LocalContextS
• hax::state::State
• hax::state::types::Base
• hax::state::types::GlobalCache
• hax::state::types::ItemCache
• hax::state::types::LocalContextS
• hax::traits::ImplExprContents
• hax::traits::ItemPredicate
• hax::traits::ItemPredicates
• hax::traits::PredicateSearcher
• hax::types::Span
• hax::types::Spanned
• 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::Symbol
• 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::FullDef
• hax::types::new::full_def::ImplAssocItem
• hax::types::new::full_def::ParamEnv
• hax::types::new::full_def::VirtualTraitImpl
• hax::types::new::item_ref::ItemRef
• hax::types::ty::Alias
• hax::types::ty::Align
• hax::types::ty::AssocItem
• hax::types::ty::Binder
• hax::types::ty::BoundRegion
• hax::types::ty::BoundTy
• hax::types::ty::Canonical
• hax::types::ty::CanonicalUserTypeAnnotation
• hax::types::ty::Clause
• hax::types::ty::ClosureArgs
• hax::types::ty::CoercePredicate
• hax::types::ty::Decorated
• hax::types::ty::DiscriminantValue
• hax::types::ty::DynBinder
• hax::types::ty::EarlyParamRegion
• hax::types::ty::ExistentialProjection
• hax::types::ty::ExistentialTraitRef
• hax::types::ty::FieldDef
• hax::types::ty::GenericParamDef
• hax::types::ty::GenericPredicate
• hax::types::ty::GenericPredicates
• hax::types::ty::ItemRefContents
• hax::types::ty::LateParamRegion
• hax::types::ty::OutlivesPredicate
• hax::types::ty::ParamConst
• hax::types::ty::ParamTy
• hax::types::ty::Placeholder
• hax::types::ty::Predicate
• hax::types::ty::ProjectionPredicate
• hax::types::ty::Region
• hax::types::ty::ReprFlags
• hax::types::ty::ReprOptions
• hax::types::ty::SubtypePredicate
• hax::types::ty::TraitPredicate
• hax::types::ty::Ty
• hax::types::ty::TyFnSig
• hax::types::ty::TyGenerics
• hax::types::ty::TypeAndMut
• hax::types::ty::UserArgs
• hax::types::ty::UserSelfTy
• hax::types::ty::VariantDef
• hax::utils::error_macros::s_expect_impls::Dummy
• hax::utils::type_map::TypeMap
• translate::translate_bodies::BlockTransCtx
• translate::translate_bodies::BodyTransCtx
• 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

Enums

• CharonFailure
• hax::AdtFlags
• hax::AdtKind
• hax::AliasKind
• hax::AliasRelationDirection
• hax::AssocItemContainer
• hax::AssocKind
• hax::AssocTypeData
• hax::BoundRegionKind
• hax::BoundTyKind
• hax::BoundVarIndexKind
• hax::BoundVariableKind
• hax::BuiltinTraitData
• hax::ClauseKind
• hax::ClosureKind
• hax::ConstKind
• hax::ConstOperandKind
• hax::ConstantExprKind
• hax::ConstantInt
• hax::ConstantLiteral
• hax::CtorKind
• hax::CtorOf
• hax::DefIdBase
• hax::DefKind
• hax::DefPathItem
• hax::DestructData
• hax::DiscriminantDefinition
• hax::ErrorGuaranteed
• hax::ExistentialPredicate
• hax::ExternAbi
• hax::FloatTy
• hax::FullDefKind
• hax::GenericArg
• hax::GenericParamDefKind
• hax::GenericPredicateId
• hax::HostEffectPredicate
• hax::ImplAssocItemValue
• hax::ImplExprAtom
• hax::ImplExprPathChunk
• hax::ImplTraitInTraitData
• hax::InferTy
• hax::InlineAttr
• hax::IntTy
• hax::ItemPredicateId
• hax::LateParamRegionKind
• hax::LitIntType
• hax::Mutability
• hax::NormalizesTo
• hax::PredicateKind
• hax::RDefKind
• hax::RegionKind
• hax::Safety
• hax::SyntheticItem
• hax::Term
• hax::TyKind
• hax::UintTy
• hax::UnsizingMetadata
• hax::UserType
• hax::Variance
• hax::VariantKind
• hax::Visibility
• hax::constant_utils::ConstantExprKind
• hax::constant_utils::ConstantInt
• hax::constant_utils::ConstantLiteral
• hax::constant_utils::VariantKind
• hax::prelude::RDefKind
• hax::traits::BuiltinTraitData
• hax::traits::DestructData
• hax::traits::ImplExprAtom
• hax::traits::ImplExprPathChunk
• hax::traits::ItemPredicateId
• hax::types::ErrorGuaranteed
• 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::ImplAssocItemValue
• hax::types::new::full_def::InlineAttr
• hax::types::new::synthetic_items::SyntheticItem
• hax::types::ty::AdtFlags
• hax::types::ty::AdtKind
• hax::types::ty::AliasKind
• hax::types::ty::AliasRelationDirection
• hax::types::ty::AssocItemContainer
• hax::types::ty::AssocKind
• hax::types::ty::AssocTypeData
• hax::types::ty::BoundRegionKind
• hax::types::ty::BoundTyKind
• hax::types::ty::BoundVarIndexKind
• hax::types::ty::BoundVariableKind
• hax::types::ty::ClauseKind
• hax::types::ty::ClosureKind
• hax::types::ty::DiscriminantDefinition
• hax::types::ty::ExistentialPredicate
• hax::types::ty::ExternAbi
• hax::types::ty::FloatTy
• hax::types::ty::GenericArg
• hax::types::ty::GenericParamDefKind
• hax::types::ty::GenericPredicateId
• hax::types::ty::HostEffectPredicate
• hax::types::ty::ImplTraitInTraitData
• hax::types::ty::InferTy
• hax::types::ty::IntTy
• hax::types::ty::LateParamRegionKind
• hax::types::ty::LitIntType
• hax::types::ty::NormalizesTo
• hax::types::ty::PredicateKind
• hax::types::ty::RegionKind
• hax::types::ty::Term
• hax::types::ty::TyKind
• hax::types::ty::UintTy
• hax::types::ty::UnsizingMetadata
• hax::types::ty::UserType
• hax::types::ty::Variance
• hax::types::ty::Visibility
• translate::translate_crate::RustcItem
• translate::translate_crate::TraitImplSource
• translate::translate_crate::TransItemSourceKind
• translate::translate_ctx::MethodStatus
• translate::translate_trait_objects::TrVTableField
• translate::translate_trait_objects::VtableMethodValue

Traits

• hax::HasParamEnv
• hax::IsMirKind
• hax::SExpect
• hax::SInto
• hax::SubstBinder
• hax::ToPolyTraitRef
• hax::TypeMapper
• hax::mir_kinds::IsMirKind
• hax::rustc::HasParamEnv
• hax::rustc::SExpect
• hax::rustc::SubstBinder
• hax::rustc::TypeMapper
• hax::rustc_utils::HasParamEnv
• hax::rustc_utils::SubstBinder
• hax::sinto::SInto
• hax::state::BaseState
• hax::state::HasBase
• hax::state::HasBinder
• hax::state::HasOwner
• hax::state::UnderOwnerState
• hax::state::WithGlobalCacheExt
• hax::state::WithItemCacheExt
• hax::traits::ToPolyTraitRef
• hax::types::mir::mir_kinds::rustc::IsMirKind
• hax::utils::error_macros::SExpect
• hax::utils::type_map::TypeMapper

Macros

• hax::sinto::sinto_clone
• hax::sinto_as_usize
• hax::sinto_reexport
• hax::sinto_todo
• hax::state::__inner_helper
• hax::state::mk
• hax::state::mk_aux
• hax::utils::error_macros::fatal
• hax::utils::error_macros::format_with_context
• hax::utils::error_macros::internal_helpers::_span_verb_base
• hax::utils::error_macros::internal_helpers::_verb
• hax::utils::error_macros::report
• hax::utils::error_macros::supposely_unreachable_fatal
• hax::utils::error_macros::supposely_unreachable_message
• hax::utils::error_macros::warning
• 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::def_id_debug
• driver::run_compiler_with_callbacks
• driver::run_rustc_driver
• driver::set_mir_options
• driver::set_no_codegen
• driver::set_skip_borrowck
• driver::setup_compiler
• driver::skip_borrowck_if_set
• hax::assoc_tys_for_trait
• hax::closure_once_shim
• hax::compute_unsizing_metadata
• hax::const_value_to_constant_expr
• hax::constant_utils::uneval::bits_and_type_to_float_constant_literal
• hax::constant_utils::uneval::const_value_to_constant_expr
• hax::constant_utils::uneval::eval_ty_constant
• hax::constant_utils::uneval::is_anon_const
• hax::constant_utils::uneval::op_to_const
• hax::constant_utils::uneval::scalar_int_to_constant_literal
• hax::constant_utils::uneval::valtree_to_constant_expr
• hax::drop_glue_shim
• hax::dyn_self_ty
• hax::erase_and_norm
• hax::erase_free_regions
• hax::eval_ty_constant
• hax::get_foreign_mod_children
• hax::get_method_sig
• hax::get_mod_children
• hax::get_promoted_mir
• hax::inst_binder
• hax::name_of_local
• hax::normalize
• hax::rustc::assoc_tys_for_trait
• hax::rustc::closure_once_shim
• hax::rustc::drop_glue_shim
• hax::rustc::dyn_self_ty
• hax::rustc::get_foreign_mod_children
• hax::rustc::get_method_sig
• hax::rustc::get_mod_children
• hax::rustc::inst_binder
• hax::rustc::substitute
• 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::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::inst_binder
• hax::rustc_utils::substitute
• hax::self_clause_for_item
• hax::self_predicate
• hax::solve_destruct
• hax::solve_item_implied_traits
• hax::solve_item_required_traits
• hax::solve_sized
• hax::solve_trait
• hax::substitute
• hax::super_clause_to_clause_and_impl_expr
• 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_destruct
• hax::traits::solve_item_implied_traits
• hax::traits::solve_item_required_traits
• hax::traits::solve_item_traits_inner
• hax::traits::solve_sized
• hax::traits::solve_trait
• hax::traits::super_clause_to_clause_and_impl_expr
• hax::traits::translate_item_ref
• hax::translate_item_ref
• hax::types::def_id::get_def_kind
• hax::types::mir::get_promoted_mir
• hax::types::mir::name_of_local
• hax::types::mir::translate_mir_const
• hax::types::new::full_def::const_value
• hax::types::new::full_def::gen_closure_sig
• 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::translate_full_def
• hax::types::new::full_def::translate_full_def_kind
• hax::types::new::full_def::virtual_impl_for
• hax::types::ty::compute_unsizing_metadata
• hax::types::ty::resolve_for_dyn
• hax::utils::error_macros::s_expect_impls::s_expect_error
• main
• run_charon
• transformation_passes
• 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_bodies::translate_borrow_kind
• translate::translate_bodies::translate_field_id
• translate::translate_bodies::translate_variant_id
• translate::translate_closures::translate_closure_kind
• translate::translate_crate::translate
• translate::translate_ctx::catch_sinto
• translate::translate_generics::translate_region_name
• translate::translate_trait_objects::dynify
• translate::translate_trait_objects::usize_ty

Type Aliases

• hax::BoundVar
• hax::CanonicalUserType
• hax::ConstantExpr
• hax::ConstantKind
• hax::DebruijnIndex
• hax::Ident
• hax::ImplExpr
• hax::PlaceholderConst
• hax::PlaceholderRegion
• hax::PlaceholderType
• hax::PolyFnSig
• hax::RegionOutlivesPredicate
• hax::RegionVid
• hax::TraitRef
• hax::TypeOutlivesPredicate
• hax::constant_utils::ConstantExpr
• hax::constant_utils::ConstantKind
• hax::state::StateWithBase
• hax::state::StateWithBinder
• hax::state::StateWithOwner
• hax::state::UnitBinder
• hax::state::types::UnitBinder
• hax::traits::ImplExpr
• hax::types::Ident
• hax::types::ty::BoundVar
• hax::types::ty::CanonicalUserType
• hax::types::ty::DebruijnIndex
• hax::types::ty::PlaceholderConst
• hax::types::ty::PlaceholderRegion
• hax::types::ty::PlaceholderType
• hax::types::ty::PolyFnSig
• hax::types::ty::RegionOutlivesPredicate
• hax::types::ty::RegionVid
• hax::types::ty::TraitRef
• hax::types::ty::TypeOutlivesPredicate

Trait Aliases

• hax::TypeMappable
• hax::rustc::TypeMappable
• hax::state::UnderBinderState
• hax::utils::type_map::TypeMappable

Statics

• driver::SKIP_BORROWCK

Constants

• hax::types::def_id::SYNTHETIC_CRATE_NAME