Daniel,

Thanks for the fixes and the link to a x86_64-compatible version of uClibc!

I successfully built LLVM (revision 102924) and klee (revision 102924)
using the x86_64 version of klee-uclibc
(http://www.doc.ic.ac.uk/~cristic/klee-uclibc-0.01-x64.tgz):

    llvm: ./configure --enable-optimized --enable-targets=host
--with-built-clang
    klee: ./configure --with-llvm=/usr/local/src/llvm
--with-uclibc=/usr/local/src/klee-uclibc \
                      --enable-posix-runtime

but I get the following failures when running Klee's `make check':

FAIL: /src/klee/test/CXX/SimpleVirtual.cpp
Failed with signal(SIGABRT) at line 2
while running: klee --no-output --exit-on-error --no-externals
SimpleVirtual.cpp.tmp1.bc
KLEE: output directory = "klee-out-2"
KLEE: WARNING: undefined reference to function: _Unwind_Resume_or_Rethrow
KLEE: WARNING: undefined reference to function: __gxx_personality_v0
klee: Executor.cpp:961: const klee::Cell&
klee::Executor::eval(klee::KInstruction*, unsigned int,
klee::ExecutionState&) const: Assertion `vnumber != -1 && "Invalid
operand to eval(), not a value or constant!"' failed.
0  klee            0x0000000000c508cf
1  klee            0x0000000000c527ba
2  libpthread.so.0 0x00000033f400f0f0
3  libc.so.6       0x00000033f34326d5 gsignal + 53
4  libc.so.6       0x00000033f3433eb5 abort + 373
5  libc.so.6       0x00000033f342b7c5 __assert_fail + 245
6  klee            0x00000000005274e1
7  klee            0x000000000053aa22
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 7042
8  klee            0x000000000053ddfe
klee::Executor::run(klee::ExecutionState&) + 1774
9  klee            0x000000000053e79e
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**)
+ 1774
10 klee            0x0000000000523d76 main + 10918
11 libc.so.6       0x00000033f341eb1d __libc_start_main + 253
12 klee            0x000000000051bc19

FAIL: /src/klee/test/regression/2008-02-11-phi-nodes-after-invoke.ll
Failed with signal(SIGABRT) at line 1
while running: llvm-as -f
/src/klee/test/regression/2008-02-11-phi-nodes-after-invoke.ll -o - |
klee --no-output --exit-on-error
KLEE: output directory = "klee-out-12"
klee: Executor.cpp:961: const klee::Cell&
klee::Executor::eval(klee::KInstruction*, unsigned int,
klee::ExecutionState&) const: Assertion `vnumber != -1 && "Invalid
operand to eval(), not a value or constant!"' failed.
0  klee            0x0000000000c508cf
1  klee            0x0000000000c527ba
2  libpthread.so.0 0x00000033f400f0f0
3  libc.so.6       0x00000033f34326d5 gsignal + 53
4  libc.so.6       0x00000033f3433eb5 abort + 373
5  libc.so.6       0x00000033f342b7c5 __assert_fail + 245
6  klee            0x00000000005274e1
7  klee            0x000000000053aa22
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 7042
8  klee            0x000000000053ddfe
klee::Executor::run(klee::ExecutionState&) + 1774
9  klee            0x000000000053e79e
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**)
+ 1774
10 klee            0x0000000000523d76 main + 10918
11 libc.so.6       0x00000033f341eb1d __libc_start_main + 253
12 klee            0x000000000051bc19


The rest of `make check' completes without error and returns:

        ===  Summary ===

# of expected passes        102
# of unexpected failures    2
# of unexpected successes    1
# of expected failures        2
FAIL: /src/klee/test/CXX/SimpleVirtual.cpp
XFAIL: /src/klee/test/Expr/Evaluate2.pc
XFAIL: /src/klee/test/Programs/pcregrep.c

`make unittests' is successful.

--- Vladimir

BTW, LLVM's `make check' has 6 unexpected failures. I don't know if
these affect Klee.

FAIL: /usr/local/src/llvm/test/Bindings/Ocaml/vmcore.ml
Failed with exit(10) at line 2
while running: ./vmcore.ml.tmp vmcore.ml.tmp.bc
FAILED: builder/builder/dbg #1

FAIL: /usr/local/src/llvm/test/FrontendC/crash-invalid-array.c for PR6913
Failed with exit(1) at line 1
while running: not
/usr/local/llvm-gcc4.2-2.7-x86_64-linux/bin/llvm-gcc   -emit-llvm -w -O1
/usr/local/src/llvm/test/FrontendC/crash-invalid-array.c -S |& /bin/grep
{error: invalid use of array with unspecified bounds}
child process exited abnormally

FAIL: /usr/local/src/llvm/test/FrontendC/inline-asm-function.c
Failed with exit(1) at line 1
while running: /usr/local/llvm-gcc4.2-2.7-x86_64-linux/bin/llvm-gcc  
-emit-llvm -w -S
/usr/local/src/llvm/test/FrontendC/inline-asm-function.c -fasm-blocks -o
- -O | /bin/grep naked
child process exited abnormally
Running /usr/local/src/llvm/test/FrontendC++/dg.exp ...

FAIL: /usr/local/src/llvm/test/FrontendC++/2010-02-17-DbgArtificialArg.cpp
Failed with exit(1) at line 1
while running: /usr/local/llvm-gcc4.2-2.7-x86_64-linux/bin/llvm-gcc  
-emit-llvm -w -g -S
/usr/local/src/llvm/test/FrontendC++/2010-02-17-DbgArtificialArg.cpp -o
- | /bin/grep DW_TAG_pointer_type |  /bin/grep "i32 524303, metadata ..,
metadata ..., metadata .., i32 ., i64 .., i64 .., i64 0, i32 64,
metadata ..."
child process exited abnormally

FAIL: /usr/local/src/llvm/test/FrontendC++/2010-03-22-empty-baseclass.cpp
Failed with exit(1) at line 1
while running: /usr/local/llvm-gcc4.2-2.7-x86_64-linux/bin/llvm-gcc  
-emit-llvm -w -S -emit-llvm
/usr/local/src/llvm/test/FrontendC++/2010-03-22-empty-baseclass.cpp -o -
-O2 | FileCheck
/usr/local/src/llvm/test/FrontendC++/2010-03-22-empty-baseclass.cpp
/usr/local/src/llvm/test/FrontendC++/2010-03-22-empty-baseclass.cpp:134:11:
error: expected string not found in input
// CHECK: ret i32
          ^
<stdin>:1:1: note: scanning from here
; ModuleID =
'/usr/local/src/llvm/test/FrontendC++/2010-03-22-empty-baseclass.cpp'
^
<stdin>:14:5: note: possible intended match here
declare i32 @puts(i8* nocapture) nounwind
    ^

FAIL:
/usr/local/src/llvm/test/FrontendC++/2010-04-30-OptimizedMethod-Dbg.cpp
Failed with exit(1) at line 2
while running: grep "i1 false, i1 true. . . DW_TAG_subprogram"
2010-04-30-OptimizedMethod-Dbg.cpp.tmp | count 2
Expected 2 lines, got 0.

Vladimir G. Ivanovic                            http://www.leonora.org
+1 650 450 4101                                       vladimir at acm.org


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
Url : 
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100503/1fb2c4fc/attachment.bin
 

Reply via email to