Hi Giuseppe, you have a bug in your code:
assert(rba = rga) should be
assert(rba == rga)
Once you fix that, KLEE works as expected.
Best,
Cristian
On 26/04/10 08:08, Giuseppe Di Guglielmo wrote:
> 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
>
