[klee-dev] how to get an new assignment without invoke solver

[Jingde Liu]

Hi,
I know what happened now. All of the assignments are generated by invoking
solver, but some of them can satisfy several query. What's more, maybe some
of the solver queries in KLEE are unnecessary. The evaluating process is
very complicated to me.
Thanks for your reading.


2014-05-07 23:26 GMT+08:00 Jingde Liu <liujingde2008 at gmail.com>:

> Hi everyone,
>
> I encounter the following question when hacking KLEE.
>
> I want to know whether all assignments are generated by invoke STP solver.
> Can I get an new assignment by call cache.findSuperset()/cache.findSubset()
> ?
> For example as bellow:
> ________________________________________
> int test(int x) {
>   if (x > 0)
>     if(x > 10)
>           return 0;
>     else
>        return 1;
>   else
>     return 2;
> }
> _________________________________________
> as far as know, first, KLEE compute the validity of (x > 0), in this step,
> it do getAssignment(null. false) and getAssignment(null, x <= 0) by invoke
> solver. Second, KLEE compute the validity of (x > 10), I'm not clear about
> how to getAssignment(x > 0, false) without invoking solver.
> Any help is truly appreciated.
>
-------------- next part --------------
HTML attachment scrubbed and removed