Entire mkstemp source algorithm. Random choice uses actual machine RNG; exclusive host creation and open flags are explicit typed effects.

@[reducible, inline]

abbrev Miri.Interpreter.UnixTempFile.M (σ α : Type) : Type

Equations

• Miri.Interpreter.UnixTempFile.M = EStateM Miri.Interpreter.StepError

inductive Miri.Interpreter.UnixTempFile.HostOptions : Type

• unix : HostOptions

  read+write+create_new, mode0600 and host O_EXCL.

• windows : HostOptions

  read+write+create_new, share_mode(0).

structure Miri.Interpreter.UnixTempFile.Hooks (S F D Path HM Time E Kind H : Type) : Type

• paths : UnixFsPaths.Hooks S F D Path HM Time E Kind
• choose : Nat → M S Nat

  Actual uniform IndexedRandom.choose index from canonical machine RNG.

• openExclusive : Path → HostOptions → M S (Except (IoError.HostError E) H)
• insertFile : H → Bool → Bool → M S Int32
• attemptBudget : Nat

  Explicit runner bound, independent of compiler TMP_MAX.

def Miri.Interpreter.UnixTempFile.mkstemp {S F D P HM T E K H : Type} (h : Hooks S F D P HM T E K H) (template : OpTy Memory.Provenance) : M S Int32

Equations

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