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
