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
> <http://test.minormatter.com/~ddunbar/klee-doxygen/classklee_1_1Executor.html#355442daa3f4d14e11b6acebaa821fdd>->getValue
>
> <http://test.minormatter.com/~ddunbar/klee-doxygen/classklee_1_1TimingSolver.html#9f22c857ea8bffe800cef76c3b7eae65>(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
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
