machine.rs::check_fn_target_features exact compiler attributes/session. Feature order and all Enabled/Forced/Implied kinds are retained in input. The source driver performs the initial guard, diagnostic filtering and wasm abort.

def Miri.Input.CompilerTargetFeatures.required (p : CompilerIntrinsicFacts.Prepared) (callee : Interpreter.CallInstance) : Except String (Array Interpreter.ExecutionCallLeaves.TargetFeature)

Equations

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

def Miri.Input.CompilerTargetFeatures.available (p : CompilerIntrinsicFacts.Prepared) (name : String) : Except String Bool

Equations

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

def Miri.Input.CompilerTargetFeatures.isLikeWasm (p : CompilerIntrinsicFacts.Prepared) : Except String Bool

Equations

• Miri.Input.CompilerTargetFeatures.isLikeWasm p = do let session ← p.program.input.raw.getObjVal? "compiler_session_queries" let __do_lift ← session.getObjVal? "is_like_wasm" __do_lift.getBool?

def Miri.Input.CompilerTargetFeatures.dictionary {S : Type} (p : CompilerIntrinsicFacts.Prepared) : Interpreter.ExecutionCallLeaves.TargetFeatures S

Equations

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