[klee-dev] Query: Klee behavior with pointer de-referencing
Sandeep
sdasgup3 at illinois.edu
Wed Jan 8 16:58:33 GMT 2014
Hello Tomasz,
Thanks a lot for the try.
As you said the test case that you are getting is for failed external
assert call.
But what is expected in this case is *one *testcase for the path
(*temp > 0) (as all values of the symbolic variable x will suggest that
path only).
Can you please add #include<assert.h> and run it again. (I am also
getting the same behavior if I omit #include<assert.h> ).
Thanks
Sandeep
On 12/18/2013 3:53 PM, Kuchta, Tomasz wrote:
> Hi Sandeep,
>
> For foo (x, 10, 20, 30, 40) the result is the following:
>
> tk2512:/data/temp$ /data/temp/klee/Release+Asserts/bin/klee test.bc
>
> KLEE: output directory = "klee-out-4"
>
> KLEE: WARNING: undefined reference to function: assert
>
> KLEE: WARNING ONCE: calling external: assert(1)
>
> KLEE: ERROR: /data/temp/test.c:13: failed external call: assert
>
> KLEE: NOTE: now ignoring this error at this location
>
>
> KLEE: done: total instructions = 69
>
> KLEE: done: completed paths = 3
>
> KLEE: done: generated tests = 1
>
>
> 1 test file is generated (this is for failed external call assert and
> x == 1):
>
>
> ktest-tool --write-ints test000001.ktest
>
> ktest file : 'test000001.ktest'
>
> args : ['test.bc']
>
> num objects: 1
>
> object 0: name: 'x'
>
> object 0: size: 4
>
> object 0: data: 1
>
>
> Best regards,
>
> Tomek
>
> From: Sandeep <sdasgup3 at illinois.edu <mailto:sdasgup3 at illinois.edu>>
> Date: Wednesday, 18 December 2013 20:29
> To: "Kuchta, Tomasz" <t.kuchta12 at imperial.ac.uk
> <mailto:t.kuchta12 at imperial.ac.uk>>, "klee-dev-bounces at imperial.ac.uk
> <mailto:klee-dev-bounces at imperial.ac.uk>"
> <klee-dev-bounces at imperial.ac.uk <mailto:klee-dev-bounces at imperial.ac.uk>>
> Subject: Re: [klee-dev] Query: Klee behavior with pointer de-referencing
>
> Thanks a lot Tomasz.
> I two believe that only two paths should get reported. But I am
> getting 3 (with one abort)
>
> Can you please confirm the number of paths that you are getting with
> the following call to foo
>
> return foo(x,10,20,30,40);
>
> I believe it is just 1 in your case.
>
>
> Thanks
> Sandeep
>
>
>
> On 12/18/2013 01:41 AM, Kuchta, Tomasz wrote:
>> Hello Sandeep,
>>
>> It seems to me that both paths are possible here.
>> We first constraint x to be 1, 2 or 3 by doing klee_assume((x > 0) &
>> (x < 4)).
>> Then we will have the following values for the corresponding indices
>> in the “array”,
>> if we call foo() with arguments x1 = 10, x2 = 20, x3 = 30, x4 = -1:
>>
>> array[1] == 20
>> array[2] == 30
>> array[3] == -1
>>
>> Both: array[1] and array[2] will exercise the path leading to
>> assert(1), because their values are greater than 0.
>> On the other hand, array[3] will exercise the path leading to
>> assert(0), because its value is –1.
>>
>> I’ve run the test on the current latest version of KLEE and two
>> *.ktest files were created:
>>
>> ktest-tool --write-ints test000001.ktest
>>
>> ktest file : 'test000001.ktest'
>>
>> args : ['test.bc']
>>
>> num objects: 1
>>
>> object 0: name: 'x'
>>
>> object 0: size: 4
>>
>> object 0: data: 1
>>
>>
>> ktest-tool --write-ints test000002.ktest
>>
>> ktest file : 'test000002.ktest'
>>
>> args : ['test.bc']
>>
>> num objects: 1
>>
>> object 0: name: 'x'
>>
>> object 0: size: 4
>>
>> object 0: data: 3
>>
>>
>> The first file corresponds to the path exercised by value 20 of
>> array[1] (x == 1, which transforms to array[1]).
>>
>> The second file corresponds to the path exercised by value –1 of
>> array[3] (x == 3, which transforms to array[3]).
>>
>>
>> Hope that helps,
>>
>> Best regards
>>
>> Tomek
>>
>>
>> From: Sandeep <sdasgup3 at illinois.edu <mailto:sdasgup3 at illinois.edu>>
>> Date: Wednesday, 18 December 2013 06:39
>> To: klee-dev <klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>>
>> Subject: [klee-dev] Query: Klee behavior with pointer de-referencing
>>
>> 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
>
>
> --
> *With Thanks and Regards,*
> Sandeep Dasgupta
> Graduate ( PhD ) in Computer Science
> Room : 1218 Siebel Center for Computer Science
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list