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]> 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 problem >>> before 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 are >>> storing the addresses of the x_i variables into the array, which is >>> likely 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 x >>> so that >>> the path (*temp <= 0) is explored and >>> KLEE is able to figure out the value of x (= 3) for that to >>> happen. But >>> in 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, 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)); // 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] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
