kdrag.contrib.pcode.asmspec.execute_spec_stmts

kdrag.contrib.pcode.asmspec.execute_spec_stmts(stmts: list[SpecStmt], tracestate: TraceState, ctx: BinaryContext, verbose=True) → tuple[TraceState | None, list[VerificationCondition]]

Execute a list of spec statements on a given trace state.

Parameters:

• stmts (list[SpecStmt])

• tracestate (TraceState)

• ctx (BinaryContext)

Return type:

tuple[TraceState | None, list[VerificationCondition]]