how to get an new assignment without invoke solver

[Jingde Liu]

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.

[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.

Post by Jingde Liu
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()
?
________________________________________
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.