kdrag.contrib.pcode.asmspec.init_trace_states

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

Initialize all trace states from the entry points in the spec. This will run the spec statements after the entry statement and also the first actual instruction.

Parameters:

• ctx (BinaryContext)

• mem (MemState)

• spec (AsmSpec)

Return type:

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