Re: [klee-dev] Why KLEE still symbolic executing program after reaching max-fork?
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
Re: [klee-dev] Why KLEE still symbolic executing program after reaching max-fork?
More specifically, in Executor.cpp function fork() line 941(https://github.com/klee/klee/blob/fc50ab32349a4cc61980ba5b97bfa7c3961ce964/lib/Core/Executor.cpp#L941) KLEE will always check the satisfiability at first, then KLEE check whether reach max fork limit until line 975(https://github.com/klee/klee/blob/fc50ab32349a4cc61980ba5b97bfa7c3961ce964/lib/Core/Executor.cpp#L975) That is the point I don’t understand. Thanks for any help! From: on behalf of XIE Xuan Date: Monday, May 25, 2020 at 11:32 AM To: "klee-dev@imperial.ac.uk" Subject: [klee-dev] Why KLEE still symbolic executing program after reaching max-fork? 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] Why KLEE still symbolic executing program after reaching max-fork?
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
