eval.rs::call_main entry signature and lang_start queries. Original bound variables, return type and Ty::new_fn_ptr identity are retained. Resolution is keyed by the exact start DefId and complete source generic argument vector. Link-section static reading remains a separate stateful global-memory query.

structure Miri.Input.CompilerMain.Entry : Type

• definition : MIR.DefId
• parameters : Array Interpreter.MainGenericParameter
• signature : Except String Interpreter.MainSignature
• start : Except String (Option Interpreter.CallInstance)

structure Miri.Input.CompilerMain.Section : Type

• definition : MIR.DefId
• span : MIR.SpanRef
• ty : MIR.TyId
• allocation : AllocationId

structure Miri.Input.CompilerMain.SectionQuery : Type

• name : String
• result : Except String Section

structure Miri.Input.CompilerMain.Prepared : Type

• program : LoweredProgram
• runtime : RuntimeMetadata
• start : Option MIR.DefId
• compilerEntry : Option MIR.DefId
• compilerEntryType : Except String (Option (MIR.DefId × Interpreter.MainEntryType))

  Exact rustc EntryFnType attached to tcx.entry_fn. When absent, the compiler did not select a Rust main and the source may use Miri's separately selected miri_start entry.

• entries : Array Entry
• sections : Except String (Array SectionQuery)

def Miri.Input.CompilerMain.prepare (runtime : RuntimeMetadata) (program : LoweredProgram) (sourceEquality : Option (RuntimeMetadata.JsonReflexivity runtime.source.raw) := none) : Except String Prepared

Equations

• One or more equations did not get rendered due to their size.

def Miri.Input.CompilerMain.resolve (p : Prepared) (definition : MIR.DefId) (args : Array MIR.GenericArg) : Except String (Option Interpreter.CallInstance)

Equations

• One or more equations did not get rendered due to their size.

def Miri.Input.CompilerMain.sourceCompilerEntry (p : Prepared) : Except String (Option (MIR.DefId × Interpreter.MainEntryType))

Exact compiler-selected ordinary entry metadata for the source startup factory. none is retained for the separate MiriStart entry path.

Equations

• Miri.Input.CompilerMain.sourceCompilerEntry p = p.compilerEntryType

def Miri.Input.CompilerMain.hooks {U C O F A Aff P : Type} (p : Prepared) (base : Interpreter.MainMachine.Hooks U C O ABI.ExternAbi F A Aff P) : Interpreter.MainMachine.Hooks U C O ABI.ExternAbi F A Aff P

Equations

• One or more equations did not get rendered due to their size.