Documentation

Miri.Input.CompilerSignatureAbi

helpers.rs:427–444 constructs mk_fn_sig/Binder::dummy then queries fn_abi_of_fn_ptr with an empty extra-argument list. Match the complete source request, never a callee ABI or a same-layout function signature. The finite compiler catalog does not claim to answer arbitrary runtime constructors.

source
def Miri.Input.CompilerSignatureAbi.queryWithIndex {raw : Lean.Json} (runtime : RuntimeMetadata) (index : CompilerQueryIndices.SignatureAbi runtime raw) (request : Interpreter.FunctionCalls.SignatureRequest ABI.ExternAbi) :
Except String (ABI.FnAbi MIR.TyId)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Miri.Input.CompilerSignatureAbi.query (p : CompilerProviders.Prepared) (request : Interpreter.FunctionCalls.SignatureRequest ABI.ExternAbi) :
    Except String (ABI.FnAbi MIR.TyId)
    Equations
    Instances For
      source
      def Miri.Input.CompilerSignatureAbi.hook {C : Sort u_1} {S : Type} (p : CompilerProviders.Prepared) :
      C → (request : Interpreter.FunctionCalls.SignatureRequest ABI.ExternAbi) → EStateM Interpreter.StepError S (ABI.FnAbi MIR.TyId)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For