Dear all,
I hereby attach a small example for using KLEE as a equivalence checker.
In the example I am providing two different implementation of an ABS
function (good_abs and a bad_abs), and I want to retrieve the testcase which
identifies a not equivalent behaviours (e.g. x = 1234).
int bad_abs (int x)
{
if (x < 0)
return -x;
if (x == 1234)
return -x;
return x;
}
int good_abs (int x)
{
if (x < 0)
return -x;
return x;
}
I compare the two implementation results with an assert statement:
int p;
klee_make_symbolic (&p, sizeof p, "p");
int rba = bad_abs (p);
int rga = good_abs (p);
assert (rba = rga);
I compiled the code by means of the 'kc' script, just (e.g. clang
-emit-llvm -O1 -c -I ${KLEE_DIR}/include abs.c -o abs.bc)
$ kc abs.c
(please set the KLEE_DIR and PATH for pointing to the KLEE installation dir
and to clang compiler)
I run the code by means of 'kr' script, just (e.g. klee klee
--only-output-states-covering-new abs.bc)
$ kr abc.bc
The result is something like:
KLEE: output directory = "klee-out-2"
WARNING: Linking two modules of different data layouts!
WARNING: Linking two modules of different data layouts!
WARNING: Linking two modules of different data layouts!
KLEE: ERROR: ASSERTION FAIL: rba = rga
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 13
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2
How can I dump the testcase which identify the error?
In the klee-last directory there is the file:
test000002.assert.err
but the testcase is not the expected x = 1234:
# $ ktest-tool --write-ints klee-last/test000002.ktest
ktest file : 'klee-last/test000002.ktest'
args : ['abs.bc']
num objects: 1
object 0: name: 'p'
object 0: size: 4
object 0: data: 0
What am I mistaken?
Best regards,
Giuseppe
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100426/2004b375/attachment.html
-------------- next part --------------
A non-text attachment was scrubbed...
Name: abs.tgz
Type: application/octet-stream
Size: 820 bytes
Desc: not available
Url :
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100426/2004b375/attachment.obj
