Hello Xiangyu,
Look at the kTest_fromFile function in lib/Basic/KTest.cpp and
tools/klee/main.cpp for an usage example.
Paul
On 15 Aug 2012, at 15:01, zhangxy wrote:
> Hi all,
> I'm trying to substitute concrete values (in a ktest file) into the path
> condition when encounter a branch, to guide Klee to choose an appropriate
> path. In the "seed" mode of Klee, it seems that the function
> SeedInfo.Assignment.evaluate() can do this.
> for (std::vector<SeedInfo>::iterator siit = seeds.begin(), siie =
> seeds.end(); siit != siie; ++siit) {
> ......
> solver->getValue(current, siit->assignment.evaluate(condition), res);
> But I don't know how to construct the class of SeedInfo or Assignment by a
> ktest file. Could you show me the steps to substitute concrete values into
> the condition?
> Thank you,
> Xiangyu Zhang
> _______________________________________________
> klee-dev mailing list
> klee-dev@keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@keeda.stanford.edu
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
