kdrag.contrib.pcode.asmspec.substitute_state

kdrag.contrib.pcode.asmspec.substitute_state(e: ExprRef, ctx: BinaryContext, memstate: MemState, ghost_env: dict[str, ExprRef]) → ExprRef

Substitute both ghost state and context state (ram / registers). Converts an expression in state variables to one that one that extracts those values from the given memstate and ghost_env.

Parameters:

• e (ExprRef)

• ctx (BinaryContext)

• memstate (MemState)

• ghost_env (dict[str, ExprRef])

Return type:

ExprRef