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 <[email protected]>: > 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. >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
