kdrag.contrib.pcode.asmspec.execute_spec_and_insn

kdrag.contrib.pcode.asmspec.execute_spec_and_insn(tracestate0: TraceState, spec: AsmSpec, ctx: BinaryContext, verbose=True) → tuple[list[TraceState], list[VerificationCondition]]

Execute spec statements and then one instruction.

Parameters:

• tracestate0 (TraceState)

• spec (AsmSpec)

• ctx (BinaryContext)

Return type:

tuple[list[TraceState], list[VerificationCondition]]