Unfortunately no. KLEE has no way to limit it's search to paths which (will
eventually) satisfy the predicates.
Ideally a very smart search strategy would handle this automatically as part of
trying to get code coverage, but it is a very hard problem.
- Daniel
On Apr 28, 2010, at 6:02, Heinz Riener <hriener at student.tugraz.at> wrote:
> Dear all,
>
> Currently I'm using KLEE to check whether a program fulfills certain
> properties. Consider the following pseudo code example, where f is a
> function and p1, p2, and p3 are predicates using global variables or
> values returned from f.
>
> // a very large program
> f(/* symbolic args */);
>
> // predicate checks
> if (p1) {
> printf("Property #1 satisfied.");
> }
> if (p2) {
> printf("Property #2 satisfied.");
> }
> if (p3) {
> printf("Property #3 satisfied.");
> }
>
> The properties are exclusive such that only one property is true at a
> time. I'm only interested if there is one path that fulfills property
> p1, one path that fulfills property p2 and one path that fulfills
> property p3. However, KLEE searches for all feasible execution paths
> and thus fulfills each property multiple times, which is a huge
> computational waste in my case. I'm looking for a way to tell KLEE that
> each property should be checked only once.
>
> Is there some kind of KLEE instrumentation trick that could assist me?
> Can you give me some other advice to make my search task more efficient?
>
> Regards,
> Heinz
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
