Actual compiler GlobalAlloc queries and shared definition identities. Missing evidence is an error; initializer bytes do not establish declaration mutability, foreignness or layout.

def Miri.Input.CompilerGlobals.staticInfo (source : StaticAllocation) : Except String AllocationImage.StaticInfo

Equations

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

def Miri.Input.CompilerGlobals.queries : AllocationImage.Queries

Equations

• Miri.Input.CompilerGlobals.queries = { staticInfo := Miri.Input.CompilerGlobals.staticInfo }

def Miri.Input.CompilerGlobals.prepareProgram (program : LoweredProgram) : LoweredProgram

Append graph identities without changing any existing dense ID. Every body uses the final shared table, including statics with no selected MIR root.

Equations

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

def Miri.Input.CompilerGlobals.importGraph {K P E : Type} [DecidableEq K] (target : ABI.RuntimeTargetDataLayout) (program : LoweredProgram) (initial : Memory.MemoryState P E K) : AllocationImage.ImportResult P E K

Equations

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