kdrag.contrib.pcode.asmspec.run_all_paths

kdrag.contrib.pcode.asmspec.run_all_paths(ctx: BinaryContext, spec: AsmSpec, mem=None, verbose=True, max_insns=None) → list[VerificationCondition]

Initialize queue with all stated entry points, and then symbolically execute all paths, collecting verification conditions (VCs) along the way. This interleaves executions of actual assembly instructions with spec statements.

Parameters:
Return type:

list[VerificationCondition]