Validated installation of the optional prepared post-export rustc allocation-ID world. This keeps exporter graph IDs, dense Lean runtime IDs, and raw rustc IDs as three separate namespaces.
def
Miri.Input.CompilerAllocIdWorld.install
{P E K : Type}
(raw : Lean.Json)
(world? : Option CompilerAllocIdWorld)
(nodes : Array AllocationNode)
(memory : Memory.MemoryState P E K)
:
Except String (Memory.MemoryState P E K)
Equations
- One or more equations did not get rendered due to their size.
- Miri.Input.CompilerAllocIdWorld.install raw world? nodes memory = do Miri.Input.validateCompilerAllocIdWorldRaw raw nodes world? pure memory