[klee-dev] Mutually Exclusive if-statements

[James Hongyi Zeng]

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
klee-dev@keeda.stanford.edu
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev