[klee-dev] How to limit unrolling loops times

Chengyu Zhang dale.chengyu.zhang at gmail.com
Sun Jan 15 12:37:48 GMT 2017


Hi Cristian,
    Thanks for your suggestion, I will try to make a heuristics searcher to
solve the problem.

Best,
Chengyu

2017-01-11 6:28 GMT+08:00 Cristian Cadar <c.cadar at imperial.ac.uk>:

> Hi Chengyu, KLEE is not aware of loops per se, so there's no easy way to
> achieve what you want.  You might want to look instead at the search
> heuristics that KLEE provides, to see if they are good enough for your
> purposes.
>
> Best,
> Cristian
>
>
> On 04/01/2017 11:50, Chengyu Zhang wrote:
>
>> Hi all,
>>    I want KLEE stops unrolling loop when meet the unrolling loop limit
>> (For example, 10 times). I used "-max-depth" option to deal with the
>> problem, but it can't be suitable for every program and it's not a good
>> solution.
>>    I have found the "-unroll-threshold" option in "-help-hidden" can
>> deal with the problem (maybe), but it seems doesn't work. Is there any
>> options could deal with the problem? Or if anyone could tell me how to
>> use "-unroll-threshold" option?
>>
>> Thanks forward,
>> Chengyu
>>
>> --
>> 张枨宇   Chengyu Zhang
>> East China Normal University
>> School of Computer Science and Software Engineering
>> Tel: +86 18685412181
>> Mail: dale.chengyu.zhang at gmail.com <mailto:dale.chengyu.zhang at gmail.com>
>>
>>
>> _______________________________________________
>> 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
>



-- 
张枨宇   Chengyu Zhang
East China Normal University
School of Computer Science and Software Engineering
Tel: +86 18685412181
Mail: dale.chengyu.zhang at gmail.com
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list