[klee-dev] Need to understand how klee_assume() works

[General Email]

Hello,

I have the following program and I want to create the set of test cases and their corresponding constraints that only satisfy the conditions included in the klee_assume() expression.

#include <klee/klee.h>

int main()
{
  int c,d,e,f;
  klee_make_symbolic(&c, sizeof(c), "c");
  klee_make_symbolic(&d, sizeof(d), "d");
  klee_make_symbolic(&e, sizeof(e), "e");
  klee_make_symbolic(&f, sizeof(f), "f");
  
  
  klee_assume((((c==2)||(d==1))&&((e>=2)||((f<600)&&(e>=1))))||(((c == 1)||(d == 0))&&((e>=3)||((f<600)&&(e>=2)))));

  return 0;
}

When I run this program, klee gives me the following:

KLEE: output directory = "klee-out-14"
KLEE: ERROR: /home/pgbovine/klee/examples/exploringAssume/t1.c:12: invalid klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 242
KLEE: done: completed paths = 21
KLEE: done: generated tests = 9

My question is why only 9 tests are generated however there are 21 paths? And if klee generates tests for only satisfiable paths, why the message "KLEE: ERROR: /home/pgbovine/klee/examples/exploringAssume/t1.c:12: invalid klee_assume call (provably false)" is generated and what does it indicate?

As you notice I used the junction operators && and ||, are these operators the right ones to use? I guess I have some misunderstanding of the use of klee_assume() function, so can I have more explanation of its usage?

Thanks
AKhalil
-------------- next part --------------
HTML attachment scrubbed and removed