Thanks a lot Cristian. Appreciate your help.
On 01/08/2014 12:19 PM, Cristian Cadar wrote:
Indeed. You have a double-dereference there, and KLEE cannot reason symbolically about this, so it's forking into all possible cases (alternatively it could choose only one option). There is a discussion about double-dereferences in the paper describing KLEE's predecessor EXE (http://www.doc.ic.ac.uk/~cristic/papers/exe-tissec-08.pdf).Cristian On 08/01/14 17:54, Paul Marinescu wrote:As Cristian pointed in the previous reply, the answer lies in object resolution. klee does not report 3 paths, it reports 3 possible executions, all of which follow the same path. What differs between these 3 executions is the value of ptr, i.e. the object it points to. Paul On 8 Jan 2014, at 18:48, Sandeep <[email protected] <mailto:[email protected]>> wrote:Hello Cristian, I am the original author of the code that you looked at. Let me explain my intention of the code (pasted below). I am intentionally storing the addresses of xi's in a array of pointers. Also I am constraining x to take values 1,2 and 3. My expectation is that only one path of the if condition got explored as all possible values of the symbolic variable x will make *temp > 0. int foo(int x, int x1, int x2, int x3, int x4) { int **array = (int **) malloc(4*sizeof(int *)); array[0] = &x1; array[1] = &x2; array[2] = &x3; array[3] = &x4; int **ptr = array + x; int* temp = *ptr; if(*temp > 0) { assert(1); } else { assert(0); } return *temp; } int main() { int x; klee_make_symbolic(&x, sizeof(x), "x"); klee_assume((x > 0) & (x < 4)); return foo(x,10,20,30,40); } But Klee is reporting three paths. Also ktest-tool gives the following information: ktest file : 'klee-last/test000002.ktest' args : ['kleetest_5.o'] num objects: 1 object 0: name: 'x' object 0: size: 4 object 0: data: 2 ktest file : 'klee-last/test000003.ktest' args : ['kleetest_5.o'] num objects: 1 object 0: name: 'x' object 0: size: 4 object 0: data: 3 ktest file : 'klee-last/test000001.ktest' args : ['kleetest_5.o'] num objects: 1 object 0: name: 'x' object 0: size: 4 object 0: data: 1 Can you please explain why I am getting this result. With Thanks Sandeep On 1/7/2014 12:32 PM, Cristian Cadar wrote:See http://www.mail-archive.com/[email protected]/msg00891.html Cristian On 07/01/14 18:26, Pablo González de Aledo wrote:I'm sorry, I'm not the original author but I've faced the same problembefore and I also don't understand why Klee does what it does. May be the next code is simpler, and still explains the issue. int main() { int a; int array[] = {1,2,3,4,5}; klee_make_symbolic(&a, sizeof(a), "a"); if(array[a] == 3) return 0; else return 1; } Why does Klee generate 17 solutions when only one is possible (a == 2) ? Thanks. 2014/1/7 Cristian Cadar <[email protected] <mailto:[email protected]>> I only had a brief look at your code, but it looks like you arestoring the addresses of the x_i variables into the array, which islikely not what you intended. Cristian On 18/12/13 06:39, Sandeep wrote: Hello All, Please consider the following program.The intension of the program is to let KLEE choose a value of xso that the path (*temp <= 0) is explored and KLEE is able to figure out the value of x (= 3) for that to happen. Butin addition it is reporting two other paths for x = 1 and x =2,despite of the fact that there are only 2 possible paths. Also to add, if I call foo with foo(x, 10,20,30,40) then KLEE report 3 paths (for x = 1 ,2 ,3 ) instead of 1 path (as the path (*temp > 0) is not feasible for any value of x) Can anybody please give me some insight.int foo(int x, int x1, int x2, intx3, int x4) { int **array = (int **) malloc(4*sizeof(int *)); array[0] = &x1; array[1] = &x2; array[2] = &x3; array[3] = &x4; int **ptr = array + x; int* temp = *ptr; if(*temp > 0) { assert(1); } else { assert(0); } return *temp; } int main() { int x; klee_make_symbolic(&x, sizeof(x), "x"); klee_assume((x > 0) & (x < 4)); // To allow valid memory access on 'array' return foo(x,10,20,30,-1); } -- *With Thanks and Regards,* Sandeep Dasgupta Graduate ( PhD ) in Computer Science Room : 1218 Siebel Center for Computer Science _________________________________________________ klee-dev mailing list [email protected] <mailto:[email protected]> https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev> _________________________________________________ klee-dev mailing list [email protected] <mailto:[email protected]> https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev> _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev-- *With Thanks and Regards,* Sandeep Dasgupta Graduate ( PhD ) in Computer Science Room : 1218 Siebel Center for Computer Science _______________________________________________ klee-dev mailing list [email protected] <mailto:[email protected]> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
-- *With Thanks and Regards,* Sandeep Dasgupta Graduate ( PhD ) in Computer Science Room : 1218 Siebel Center for Computer Science
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
