[klee-dev] Connection between CFG and execution state

[Frank Busse]

Dear Adarsh,


On Wed, 21 Feb 2024 07:33:09 +0530
Adarsh Sudheer <adarshs2023 at gmail.com> wrote:

> Is there any parameter in the Execution state that links the CFG to the
> ExecutionSt ate. To be particular, I want to access all ExecutionState
> nodes generated from a CFG?

You can't really map a state to the CFG (unless you track re-execution
as a seed). What you can do is a) investigating branch points via a
process/execution tree traversal (the "AnnotatedExecutionTreeNode"
tracks bitcode lines (asmLine)) or b) look into the tracked coverage
information in an execution state (where you can't see loops of course).


Kind regards,

Frank