[klee-dev] 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.
-------------- next part --------------
HTML attachment scrubbed and removed