[klee-dev] KLEE function: markBranchVisited

[Super Zhang]

To be specific, after seeding stage of KLEE, the constraints in the
remaining states(to be explored further) are definitely will be true or
just possibly be true?

Thanks,
Chaoqiang


On Tue, Dec 24, 2013 at 11:49 AM, Super Zhang <chaoqiang.zhang at gmail.com>wrote:

> Hi all,
>
> In KLEE, markBranchVisited is called whenever a branch
> is visited through fork/branch. My question is that can we say this branch
> is definitely reachable if it ever has been marked as visited?
>
> Thanks,
> Chaoqiang
>
-------------- next part --------------
HTML attachment scrubbed and removed