Hi,
This was the simplest way to implement --max-forks. I agree you could
improve this, depending also on what you want to achieve.
Best,
Cristian
On 25/05/2020 10:31, XIE Xuan wrote:
Hi all,
I am reading KLEE’s source code and find that if I set “-max-fork=n”
when KLEE reach its fork limit n, it will still symbolic executing the
program. In my understanding, when KLEE stops forking, there is no need
to invoke SMT solver to check which branch is reachable or not,
therefore it is also unnecessary to symbolic executing the program in
order to set up more constraints. Thus I would like to know why KLEE not
concretely running the program after reaching fork limit?
Thanks!
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
