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

[Urmas Repinski]

Hi, AKhalil.

I suggest to try instead of using of logical 'and - &&' and 'or - ||' use bitwise 'and - &' and 'or - |'.

Difference practically between them is following: if logical && is used , a && b as example, and if a is false, then whole expression is false and b is not checked at all.
If to use bitwise &, then second parameter is checked too.

Practically in this case there is no difference what form to use, but i have no idea how klee_assume() function exactly is implemented and it is safer to use bitwise 'and' and 'or' operators instead of logical ones. 
 
There is no misunderstanding, simply i suggest to use safer condition form, try to replace &&-s with &-s, and ||-s with |-s.

Urmas Repinski. 
Date: Mon, 11 Nov 2013 06:27:30 -0800
From: general_mail2011 at yahoo.com
To: klee-dev at imperial.ac.uk
Subject: [klee-dev] Need to understand how klee_assume() works

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?
ThanksAKhalil



_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev 		 	   		  
-------------- next part --------------
HTML attachment scrubbed and removed