I tried several different version of LLVM and klee but I always run into
this problem. It seems that the solver returns incorrect results but
all solver related unit tests pass. So, what's actually wrong? Have I
forgotten some settings in the configuration/building process?
$ cat test.c
#include <klee/klee.h>
int main(int argc, char *argv[]) {
int c;
klee_make_symbolic(&c, sizeof c, "c");
if (c > 10)
return 1;
return 0;
}
$ llvm-gcc -c -g -emit-llvm -I$KLEE_DIR/include test.c
$ klee -use-stp-query-pc-log test.o; cat klee-out-0/stp-queries.qlog
KLEE: done: total instructions = 19
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
# Query 0 -- Type: InitialValues, Instructions: 13
(query [] false)
# OK -- Elapsed: 0.000226092
# Solvable: true
# Query 1 -- Type: InitialValues, Instructions: 13
array arr1[4] : w32 -> w8 = symbolic
(query [] (Eq false
(Slt 10
(ReadLSB w32 0 arr1))) []
[arr1])
# OK -- Elapsed: 0.00159706
# Solvable: false
$ klee -debug-validate-solver test.o
KLEE: output directory = "klee-out-1"
klee: Solver.cpp:302: virtual bool
ValidatingSolver::computeValidity(const klee::Query&,
klee::Solver::Validity&): Assertion `0 && "invalid solver result
(computeValidity)"' failed.
0 klee 0x08a468e8
zsh: abort klee -debug-validate-solver test.o
Heinz
On 05/19/2010 01:22 AM, Heinz Riener wrote:
> Dear all,
>
> I've updated (yesterday night) to the head SVN revisions of LLVM and
> Klee. Now, for every program Klee completes only one path. For instance,
> running Klee on the example of tutorial one, gives me the following output:
>
> $ llvm-gcc -c -g -emit-llvm islower.c
> $ klee islower.o
> KLEE: output directory = "klee-out-0"
>
> KLEE: done: total instructions = 27
> KLEE: done: completed paths = 1
> KLEE: done: generated tests = 1
>
> $ ktest-tool klee-last/test000001.ktest
> ktest file : 'klee-last/test000001.ktest'
> args : ['islower.o']
> num objects: 1
> object 0: name: 'input'
> object 0: size: 1
> object 0: data: '\x00'
>
> For all other programs, it's absolutely the same: the state set is
> always empty (except the initial state) and the data is always zero.
>
> I followed exactly the steps on the homepage[1] to build Klee with
> uclibc support. I'm currently at revision 103959 and created Release
> builds of LLVM and Klee. All unit tests pass but I see lots of fails in
> the check summary. (The whole output of make check is attached.)
>
> === Summary ===
>
> # of expected passes 62
> # of unexpected failures 43
> # of expected failures 2
>
> My previous versions of LLVM and Klee were several weeks old but worked
> fine.
>
> [1] http://klee.llvm.org/GetStarted.html
>
> Heinz
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
