Documentation

Miri.Input.CompilerRetagOptions

Tree Borrows machine parameters and the exact protected-frame attribute query from tree_borrows/mod.rs:143–148,329. Missing evidence fails on demand. The omitted CreatedPointerTag emission is diagnostics.rs::emit_diagnostic, which returns unit and changes no interpreter state. Tag allocation and protector registration remain in the actual retag implementation.

source
structure Miri.Input.CompilerRetagOptions.Options :
Type

These are the two actual TreeBorrowsParams, fixed for an execution.

  • implicitWrites : Bool
  • preciseInteriorMut : Bool
Instances For
    source
    def Miri.Input.CompilerRetagOptions.rustcNoWritable (p : CompilerProviders.Prepared) (id : MIR.DefId) :
    Except String Bool
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Miri.Input.CompilerRetagOptions.make {K U : Type} (p : CompilerProviders.Prepared) (options : Options) :
      EvalRetagMachine.Leaves K U
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For