Hi James,
It doesn't seem like what you're trying to do is sound. Take this slightly
modified example:
#include <klee/klee.h>
void f(int c) {
if(c==1) {printf("Do A\n");}
if(c==2) {printf("Do B\n");}
}
int main() {
int c;
klee_make_symbolic(&c, sizeof(c), "input");
klee_assume(c == 1 || c == 2);
f(c);
}
If you don't consider !(c==1), you'll end up saying that a path which doesn't
print anything is feasible. Perhaps you need to explain in more detail what you
want to do.
Paul
On 31 Jan 2012, at 02:06, James Hongyi Zeng wrote:
> Hi all,
>
> I am wondering whether I can explicitly tell KLEE that a set of
> if-statements are mutually exclusive. In the following example, KLEE
> generates 3 STP queries. Since c==2 and c==1 are mutually exclusive, I would
> like klee not to include !(c==1) in c==2 STP query. Is it possible?
>
> Thanks,
> James
>
> #include <klee/klee.h>
>
> void f(int c) {
> if(c==1) {printf("Do A\n");}
> if(c==2) {printf("Do B\n");}
> }
>
> int main() {
> int c;
> klee_make_symbolic(&c, sizeof(c), "input");
> f(c);
> }
>
>
>
> _______________________________________________
> klee-dev mailing list
> [email protected]
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
