[klee-dev] Why KLEE still symbolic executing program after reaching max-fork?

[Cristian Cadar]

I've just remembered that we have a PR that implements the behaviour 
that you want.  Unfortunately it wasn't merged into the mainline, but 
you might be able to revive it:
https://github.com/klee/klee/pull/203

Cristian

On 27/05/2020 10:49, Cristian Cadar wrote:
> 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 at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev