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 <[email protected] <mailto:[email protected]>>
Date: Wednesday, 18 December 2013 20:29
To: "Kuchta, Tomasz" <[email protected]
<mailto:[email protected]>>, "[email protected]
<mailto:[email protected]>"
<[email protected] <mailto:[email protected]>>
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 <[email protected] <mailto:[email protected]>>
Date: Wednesday, 18 December 2013 06:39
To: klee-dev <[email protected] <mailto:[email protected]>>
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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
