Source helpers.rs frame_in_std/user_relevance and thread.rs relevance cache. Compiler crate identity, inline scopes and caller attributes remain required queries.

structure Miri.Interpreter.FrameMetadata.CompilerHooks (K User : Type) : Type

• requiresCallerLocation : CallInstance → MachineHooks.M K User Bool
• isLocalDefinition : CallInstance → MachineHooks.M K User Bool
• definitionCrate : CallInstance → MachineHooks.M K User Nat
• userRelevantCrate : Nat → MachineHooks.M K User Bool
• crateName : Nat → MachineHooks.M K User String
• sourceScope : BodyIdentity → CallInstance → MIR.Body → Nat → MachineHooks.M K User VirtualCalls.CallerScope

def Miri.Interpreter.FrameMetadata.userRelevance {K User P E : Type} (h : CompilerHooks K User) (frame : Frame P LocalLayout E) : MachineHooks.M K User UInt8

Equations

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

def Miri.Interpreter.FrameMetadata.frameInStd {K User : Type} (h : CompilerHooks K User) : MachineHooks.M K User Bool

Equations

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