I knew where was a reason why I abandoned Fedora 14 in favor of Fedora 13.
During my rebuild of Fedora 14 distributions (both 32 bit and 64 bit) I
observed the following. I am in over my head, so if it is worth trouble
shooting I will have to be guided thru it.
I should note that for other systems (ptxdist in particular) it has been
observed that the latest tools (make in particular) are not necessarily
backward compatible with the development build process. That is not to say
that the tools are fault, just not consistent with a successful build.
dbl
For the 32 bit distribution
llvm[0]: Running test suite
make[1]: Entering directory
`/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/test'
Making a new site.exp file...
( ulimit -t 600 ; ulimit -d 512000 ; \
PATH="/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/Release/bin:/home/dbl/
Source/LLVM/llvm-2.7/suite/llvm-2.7/object-llvm-bootstrap/Release/bin:/home/
dbl/Source/LLVM/llvm-2.7/suite/llvm-2.7/test/Scripts:/home/dbl/Source/LLVM/l
lvm-2.7/llvm-gcc-bootstrap/llvm-gcc-4.2-2.7-i686-linux/bin:/usr/local/bin:/u
sr/bin:/bin:/usr/local/sbin:/usr/sbin:/sbin:/home/dbl/bin" \
/usr/bin/runtest ; \
! grep FAIL testrun.log; ! grep -q ^FAIL testrun.log; )
WARNING: Couldn't find the global config file.
WARNING: No tool specified
Test Run By dbl on Tue Mar 1 08:17:03 2011
Native configuration is i686-pc-linux-gnu
=== tests ===
Schedule of variations:
unix
Running target unix
Using /usr/share/dejagnu/baseboards/unix.exp as board description file for
target.
Using /usr/share/dejagnu/config/unix.exp as generic interface file for
target.
WARNING: Couldn't find tool config file for unix, using default.
Running /home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/CXX/dg.exp
...
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Coverage/dg.exp ...
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Dogfood/dg.exp ...
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Dogfood/ImmutableSet
.cpp
Failed with exit(1) at line 2
while running: klee --libc=klee --max-forks=200 --no-output --exit-on-error
--optimize --disable-inlining --use-non-uniform-random-search
--use-cex-cache ImmutableSet.cpp.tmp1.bc
KLEE: output directory = "klee-out-2"
KLEE: WARNING: undefined reference to function: pthread_cancel
KLEE: WARNING: undefined reference to function: pthread_create
KLEE: WARNING: undefined reference to function: pthread_getspecific
KLEE: WARNING: undefined reference to function: pthread_key_create
KLEE: WARNING: undefined reference to function: pthread_key_delete
KLEE: WARNING: undefined reference to function: pthread_mutex_init
KLEE: WARNING: undefined reference to function: pthread_mutex_lock
KLEE: WARNING: undefined reference to function: pthread_mutex_trylock
KLEE: WARNING: undefined reference to function: pthread_mutex_unlock
KLEE: WARNING: undefined reference to function: pthread_mutexattr_destroy
KLEE: WARNING: undefined reference to function: pthread_mutexattr_init
KLEE: WARNING: undefined reference to function: pthread_mutexattr_settype
KLEE: WARNING: undefined reference to function: pthread_once
KLEE: WARNING: undefined reference to function: pthread_setspecific
KLEE: WARNING: __cxa_atexit: FIXME: __cxa_atexit being ignored
KLEE: ERROR:
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26: invalid
klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
EXITING ON ERROR:
Error: invalid klee_assume call (provably false)
File: /home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c
Line: 26
Stack:
#0 00001867 in klee_range (start=0, end=5, name=155956576) at
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26
#1 00001628 in _Z4testv () at
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Dogfood/ImmutableSet
.cpp:95
#2 00001740 in main (argc=1, argv=155395712) at
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Dogfood/ImmutableSet
.cpp:131
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Lexer/dg.exp
...
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Parser/dg.exp
...
Running /home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/dg.exp
...
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Evaluate.pc
Failed with exit(1) at line 2
while running: grep "Query 0: INVALID" Evaluate.pc.tmp.log
child process exited abnormally
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/dg.exp ...
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/AliasFunctio
n.c
Failed with exit(1) at line 3
while running: grep -c foo AliasFunction.c.tmp1.log | grep 5
child process exited abnormally
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/AliasFunctio
nExit.c
Failed with exit(1) at line 4
while running: grep -c END AliasFunctionExit.c.tmp1.log | grep 2
child process exited abnormally
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/GetValue.c
Failed with exit(1) at line 2
while running: klee --exit-on-error GetValue.c.tmp1.bc
KLEE: output directory = "klee-out-118"
KLEE: WARNING: undefined reference to function: klee_get_value_i32
KLEE: ERROR: invalid klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
EXITING ON ERROR:
Error: invalid klee_assume call (provably false)
Stack:
#0 00000023 in main ()
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/InAndOutOfBo
unds.c
Failed with signal(SIGABRT) at line 2
while running: klee InAndOutOfBounds.c.tmp1.bc
KLEE: output directory = "klee-out-119"
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x08976978
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/LongDouble.c
pp
Failed with exit(1) at line 4
while running: grep -q {powl(-11\.0,1)=-11\.0\+} LongDouble.cpp.tmp.log
child process exited abnormally
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/LowerSwitch.
c
Failed with exit(1) at line 2
while running: klee --exit-on-error --allow-external-sym-calls
--switch-type=internal LowerSwitch.c.tmp.bc
KLEE: output directory = "klee-out-127"
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING: undefined reference to function: puts
KLEE: ERROR:
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26: invalid
klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
EXITING ON ERROR:
Error: invalid klee_assume call (provably false)
File: /home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c
Line: 26
Stack:
#0 00000176 in klee_range (start=0, end=256, name=164232104) at
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26
#1 00000028 in main (argc=1, argv=164238192) at
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/LowerSwitch.
c:10
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MakeSymbolic
Name.c
Failed with signal(SIGABRT) at line 2
while running: klee --use-random-search --exit-on-error
MakeSymbolicName.c.tmp1.bc
KLEE: output directory = "klee-out-130"
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x08976978
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MultipleFree
Resolution.c
Failed with signal(SIGABRT) at line 2
while running: klee --emit-all-errors MultipleFreeResolution.c.tmp1.bc
KLEE: output directory = "klee-out-133"
KLEE: WARNING: undefined reference to function: printf
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x08976978
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MultipleRead
Resolution.c
Failed with signal(SIGABRT) at line 6
while running: klee MultipleReadResolution.c.tmp1.bc >
MultipleReadResolution.c.tmp1.log
KLEE: output directory = "klee-out-134"
KLEE: WARNING: undefined reference to function: fflush
KLEE: WARNING: undefined reference to function: puts
KLEE: WARNING: undefined reference to variable: stdout
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x08976978
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MultipleReal
locResolution.c
Failed with signal(SIGABRT) at line 2
while running: klee MultipleReallocResolution.c.tmp1.bc
KLEE: output directory = "klee-out-135"
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x08976978
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MultipleWrit
eResolution.c
Failed with signal(SIGABRT) at line 6
while running: klee MultipleWriteResolution.c.tmp1.bc >
MultipleWriteResolution.c.tmp1.log
KLEE: output directory = "klee-out-136"
KLEE: WARNING: undefined reference to function: fflush
KLEE: WARNING: undefined reference to function: puts
KLEE: WARNING: undefined reference to variable: stdout
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x08976978
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/NamedSeedMat
ching.c
Failed with exit(1) at line 7
while running: grep -q "a==3" NamedSeedMatching.c.tmp.log
child process exited abnormally
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/OverlappedEr
ror.c
Failed with exit(1) at line 3
while running: ls klee-last/ | grep .ktest | wc -l | grep 4
child process exited abnormally
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/ReplayPath.c
Failed with signal(SIGABRT) at line 7
while running: klee --replay-path ReplayPath.c.tmp1.path
ReplayPath.c.tmp2.bc > ReplayPath.c.tmp3.log
KLEE: output directory = "klee-out-145"
KLEE: WARNING: undefined reference to function: printf
klee: /home/dbl/Source/KLEE/klee-2.7/lib/Core/Executor.cpp:724:
klee::Executor::StatePair klee::Executor::fork(klee::ExecutionState&,
klee::ref<klee::Expr>, bool): Assertion `!branch && "hit invalid branch in
replay path mode"' failed.
0 klee 0x08976978
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/SetForking.c
Failed with exit(1) at line 4
while running: grep "1 A" SetForking.c.tmp.uniq.log
child process exited abnormally
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/WriteCov.c
Failed with exit(1) at line 2
while running: klee --exit-on-error --write-cov WriteCov.c.tmp2.bc
KLEE: output directory = "klee-out-166"
KLEE: WARNING: undefined reference to function: printf
KLEE: ERROR:
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26: invalid
klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
EXITING ON ERROR:
Error: invalid klee_assume call (provably false)
File: /home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c
Line: 26
Stack:
#0 00000063 in klee_range (start=0, end=2, name=147651144) at
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26
#1 00000016 in main () at
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/WriteCov.c:9
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/const_array_
opt1.c
Failed with signal(SIGABRT) at line 2
while running: klee --const-array-opt --max-time=10
--only-output-states-covering-new const_array_opt1.c.tmp.bc
>const_array_opt1.c.tmp.log
KLEE: output directory = "klee-out-167"
KLEE: WARNING: undefined reference to function: puts
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x08976978
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Programs/dg.exp ...
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Runtime/POSIX/dg.exp
...
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Runtime/Uclibc/dg.ex
p ...
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Solver/dg.exp ...
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Solver/LargeIntegers
.pc
Failed with exit(1) at line 7
while running: grep "Array 0: a.16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5,
4, 3, 2, 1, 0" LargeIntegers.pc.tmp2
child process exited abnormally
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/dg.exp
...
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-08-0
1-cache-unclear-on-overwrite-flushed.c
Failed with signal(SIGABRT) at line 2
while running: klee 2007-08-01-cache-unclear-on-overwrite-flushed.c.tmp1.bc
KLEE: output directory = "klee-out-20"
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x08976978
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-10-1
1-illegal-access-after-free-and-branch.c
Failed with signal(SIGABRT) at line 2
while running: klee --optimize
2007-10-11-illegal-access-after-free-and-branch.c.tmp1.bc
KLEE: output directory = "klee-out-27"
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x08976978
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-10-1
2-failed-make-symbolic-after-copy.c
Failed with signal(SIGABRT) at line 2
while running: klee 2007-10-12-failed-make-symbolic-after-copy.c.tmp1.bc
KLEE: output directory = "klee-out-28"
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x08976978
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2008-03-1
1-free-of-malloc-zero.c
Failed with exit(1) at line 2
while running: klee --exit-on-error 2008-03-11-free-of-malloc-zero.c.tmp1.bc
KLEE: output directory = "klee-out-31"
KLEE: ERROR:
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26: invalid
klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
EXITING ON ERROR:
Error: invalid klee_assume call (provably false)
File: /home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c
Line: 26
Stack:
#0 00000068 in klee_range (start=0, end=4, name=179901040) at
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26
#1 00000031 in main ()
=== Summary ===
# of expected passes 62
# of unexpected failures 24
# of expected failures 1
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Dogfood/ImmutableSet
.cpp
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Evaluate.pc
XFAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Evaluate2.pc
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/AliasFunctio
n.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/AliasFunctio
nExit.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/GetValue.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/InAndOutOfBo
unds.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/LongDouble.c
pp
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/LowerSwitch.
c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MakeSymbolic
Name.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MultipleFree
Resolution.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MultipleRead
Resolution.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MultipleReal
locResolution.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MultipleWrit
eResolution.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/NamedSeedMat
ching.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/OverlappedEr
ror.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/ReplayPath.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/SetForking.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/WriteCov.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/const_array_
opt1.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Solver/LargeIntegers
.pc
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-08-0
1-cache-unclear-on-overwrite-flushed.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-10-1
1-illegal-access-after-free-and-branch.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-10-1
2-failed-make-symbolic-after-copy.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2008-03-1
1-free-of-malloc-zero.c
make[1]: *** [check-local] Error 1
make[1]: Leaving directory
`/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/test'
make: *** [check] Error 2
llvm[0]: Running unittests test suite
make[1]: Entering directory
`/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/unittests'
make[2]: Entering directory
`/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/unittests/Expr'
Release/ExprTests
[==========] Running 3 tests from 1 test case.
[----------] Global test environment set-up.
[----------] 3 tests from ExprTest
[ RUN ] ExprTest.BasicConstruction
[ OK ] ExprTest.BasicConstruction
[ RUN ] ExprTest.ConcatExtract
[ OK ] ExprTest.ConcatExtract
[ RUN ] ExprTest.ExtractConcat
[ OK ] ExprTest.ExtractConcat
[----------] Global test environment tear-down
[==========] 3 tests from 1 test case ran.
[ PASSED ] 3 tests.
make[2]: Leaving directory
`/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/unittests/Expr'
make[2]: Entering directory
`/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/unittests/Solver'
Release/SolverTests
[==========] Running 1 test from 1 test case.
[----------] Global test environment set-up.
[----------] 1 test from SolverTest
[ RUN ] SolverTest.Evaluation
[ OK ] SolverTest.Evaluation
[----------] Global test environment tear-down
[==========] 1 test from 1 test case ran.
[ PASSED ] 1 test.
make[2]: Leaving directory
`/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/unittests/Solver'
make[1]: Leaving directory
`/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/unittests'
[dbl at localhost Build-LLVM-32]$
For the 64 bit distribution
File test/testrun.log is as follows
Test Run By dbl on Tue Mar 1 08:23:42 2011
Native configuration is x86_64-unknown-linux-gnu
=== tests ===
Schedule of variations:
unix
Running target unix
Using /usr/share/dejagnu/baseboards/unix.exp as board description file for
target.
Using /usr/share/dejagnu/config/unix.exp as generic interface file for
target.
WARNING: Couldn't find tool config file for unix, using default.
Running /home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/CXX/dg.exp
...
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/CXX/ArrayNew.cpp
PASS: /home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/CXX/New.cpp
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/CXX/SimpleVirtual.cp
p
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/CXX/StaticConstructo
r.cpp
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/CXX/StaticDestructor
.cpp
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/CXX/Trivial.cpp
testcase /home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/CXX/dg.exp
completed in 3 seconds
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Coverage/dg.exp ...
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Coverage/ReadArgs.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Coverage/ReplayOutDi
r.c
testcase
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Coverage/dg.exp
completed in 1 seconds
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Dogfood/dg.exp ...
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Dogfood/ImmutableSet
.cpp
Failed with exit(1) at line 2
while running: klee --libc=klee --max-forks=200 --no-output --exit-on-error
--optimize --disable-inlining --use-non-uniform-random-search
--use-cex-cache ImmutableSet.cpp.tmp1.bc
KLEE: output directory = "klee-out-1"
KLEE: WARNING: undefined reference to function: pthread_cancel
KLEE: WARNING: undefined reference to function: pthread_create
KLEE: WARNING: undefined reference to function: pthread_getspecific
KLEE: WARNING: undefined reference to function: pthread_key_create
KLEE: WARNING: undefined reference to function: pthread_key_delete
KLEE: WARNING: undefined reference to function: pthread_mutex_init
KLEE: WARNING: undefined reference to function: pthread_mutex_lock
KLEE: WARNING: undefined reference to function: pthread_mutex_trylock
KLEE: WARNING: undefined reference to function: pthread_mutex_unlock
KLEE: WARNING: undefined reference to function: pthread_mutexattr_destroy
KLEE: WARNING: undefined reference to function: pthread_mutexattr_init
KLEE: WARNING: undefined reference to function: pthread_mutexattr_settype
KLEE: WARNING: undefined reference to function: pthread_once
KLEE: WARNING: undefined reference to function: pthread_setspecific
KLEE: WARNING: __cxa_atexit: FIXME: __cxa_atexit being ignored
KLEE: ERROR:
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26: invalid
klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
EXITING ON ERROR:
Error: invalid klee_assume call (provably false)
File: /home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c
Line: 26
Stack:
#0 00001881 in klee_range (start=0, end=5, name=48970400) at
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26
#1 00001638 in _Z4testv () at
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Dogfood/ImmutableSet
.cpp:95
#2 00001752 in main (argc=1, argv=48227680) at
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Dogfood/ImmutableSet
.cpp:131
testcase
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Dogfood/dg.exp
completed in 1 seconds
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Lexer/dg.exp
...
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Lexer/Numbers.p
c
testcase
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Lexer/dg.exp
completed in 0 seconds
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Parser/dg.exp
...
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Parser/Concat64
.pc
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Parser/Constant
Folding.pc
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Parser/Exprs.pc
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Parser/MultiByt
eReads.pc
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Parser/Simplify
.pc
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Parser/TypeChec
king.pc
testcase
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Parser/dg.exp
completed in 0 seconds
Running /home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/dg.exp
...
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Evaluate.pc
Failed with exit(1) at line 2
while running: grep "Query 0: INVALID" Evaluate.pc.tmp.log
child process exited abnormally
XFAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/Evaluate2.pc
Failed with exit(1) at line 2
while running: grep "Query 0: VALID" Evaluate2.pc.tmp.log
child process exited abnormally
testcase /home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Expr/dg.exp
completed in 0 seconds
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/dg.exp ...
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/Alias.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/AliasFunctio
n.c
Failed with exit(1) at line 3
while running: grep -c foo AliasFunction.c.tmp1.log | grep 5
child process exited abnormally
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/AliasFunctio
nExit.c
Failed with exit(1) at line 4
while running: grep -c END AliasFunctionExit.c.tmp1.log | grep 2
child process exited abnormally
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/AsmAddresses
.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/ByteSwap.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/CallToUndefi
nedExternal.cpp
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/CheckMemoryA
ccess.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/CopyOnWrite.
c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/DanglingConc
reteReadExpr.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/DefineFixedO
bject.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/DoubleFree.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/DumpStatesOn
Halt.c
PASS: /home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/Envp.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/ExprLogging.
c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/ExternalWeak
Linkage.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/Float.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/FunctionPoin
ter.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/GetValue.c
Failed with exit(1) at line 2
while running: klee --exit-on-error GetValue.c.tmp1.bc
KLEE: output directory = "klee-out-86"
KLEE: WARNING: undefined reference to function: klee_get_value_i32
KLEE: ERROR: invalid klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
EXITING ON ERROR:
Error: invalid klee_assume call (provably false)
Stack:
#0 00000023 in main ()
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/InAndOutOfBo
unds.c
Failed with signal(SIGABRT) at line 2
while running: klee InAndOutOfBounds.c.tmp1.bc
KLEE: output directory = "klee-out-87"
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x0000000000cdc0ff
1 klee 0x0000000000cdc78d
2 libpthread.so.0 0x00000031f9e0eeb0
3 libc.so.6 0x00000031f9a330c5 gsignal + 53
4 libc.so.6 0x00000031f9a34a76 abort + 390
5 libc.so.6 0x00000031f9a2b905 __assert_fail + 245
6 klee 0x000000000060c710
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&) + 320
7 klee 0x00000000006101ad MINISAT::Solver::search(int, int) +
205
8 klee 0x00000000006107f2
MINISAT::Solver::solve(MINISAT::vec<MINISAT::Lit> const&) + 370
9 klee 0x00000000005eecd0
BEEV::BeevMgr::toSATandSolve(MINISAT::Solver&,
std::vector<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*,
std::allocator<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*>
>&) + 528
10 klee 0x00000000005f0ba9
BEEV::BeevMgr::CallSAT_ResultCheck(MINISAT::Solver&, BEEV::ASTNode const&,
BEEV::ASTNode const&) + 73
11 klee 0x00000000005f348b
BEEV::BeevMgr::TopLevelSAT(BEEV::ASTNode const&, BEEV::ASTNode const&) +
4107
12 klee 0x00000000005d4b5d vc_query + 365
13 klee 0x00000000005a4ddb
STPSolverImpl::computeInitialValues(klee::Query const&,
std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&,
std::vector<std::vector<unsigned char, std::allocator<unsigned char> >,
std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > >
>&, bool&) + 1179
14 klee 0x000000000059245b
CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) +
251
15 klee 0x00000000005939bd
CexCachingSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 1245
16 klee 0x00000000005911c5
CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&)
+ 149
17 klee 0x000000000059e67d
IndependentSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 349
18 klee 0x0000000000574727
klee::TimingSolver::evaluate(klee::ExecutionState const&,
klee::ref<klee::Expr>, klee::Solver::Validity&) + 279
19 klee 0x000000000054e041
klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) +
225
20 klee 0x0000000000555859
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 10265
21 klee 0x000000000055876b
klee::Executor::run(klee::ExecutionState&) + 1787
22 klee 0x0000000000559104
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
1924
23 klee 0x000000000053e795 main + 8965
24 libc.so.6 0x00000031f9a1ee5d __libc_start_main + 253
25 klee 0x0000000000537009
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/IndirectCall
ToBuiltin.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/IndirectCall
ToExternal.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/InsertExtrac
tValue.ll
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/IsSymbolic.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/KleeReportEr
ror.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/LongDouble.c
pp
Failed with exit(1) at line 4
while running: grep -q {powl(-11\.0,1)=-11\.0\+} LongDouble.cpp.tmp.log
child process exited abnormally
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/LongDoubleSu
pport.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/LowerSwitch.
c
Failed with exit(1) at line 2
while running: klee --exit-on-error --allow-external-sym-calls
--switch-type=internal LowerSwitch.c.tmp.bc
KLEE: output directory = "klee-out-95"
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING: undefined reference to function: puts
KLEE: ERROR:
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26: invalid
klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
EXITING ON ERROR:
Error: invalid klee_assume call (provably false)
File: /home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c
Line: 26
Stack:
#0 00000176 in klee_range (start=0, end=256, name=35963664) at
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26
#1 00000028 in main (argc=1, argv=35911856) at
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/LowerSwitch.
c:10
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MakeConcrete
Symbolic.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MakeSymbolic
Name.c
Failed with signal(SIGABRT) at line 2
while running: klee --use-random-search --exit-on-error
MakeSymbolicName.c.tmp1.bc
KLEE: output directory = "klee-out-98"
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x0000000000cdc0ff
1 klee 0x0000000000cdc78d
2 libpthread.so.0 0x00000031f9e0eeb0
3 libc.so.6 0x00000031f9a330c5 gsignal + 53
4 libc.so.6 0x00000031f9a34a76 abort + 390
5 libc.so.6 0x00000031f9a2b905 __assert_fail + 245
6 klee 0x000000000060c710
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&) + 320
7 klee 0x00000000006101ad MINISAT::Solver::search(int, int) +
205
8 klee 0x00000000006107f2
MINISAT::Solver::solve(MINISAT::vec<MINISAT::Lit> const&) + 370
9 klee 0x00000000005eecd0
BEEV::BeevMgr::toSATandSolve(MINISAT::Solver&,
std::vector<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*,
std::allocator<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*>
>&) + 528
10 klee 0x00000000005f0ba9
BEEV::BeevMgr::CallSAT_ResultCheck(MINISAT::Solver&, BEEV::ASTNode const&,
BEEV::ASTNode const&) + 73
11 klee 0x00000000005f348b
BEEV::BeevMgr::TopLevelSAT(BEEV::ASTNode const&, BEEV::ASTNode const&) +
4107
12 klee 0x00000000005d4b5d vc_query + 365
13 klee 0x00000000005a4ddb
STPSolverImpl::computeInitialValues(klee::Query const&,
std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&,
std::vector<std::vector<unsigned char, std::allocator<unsigned char> >,
std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > >
>&, bool&) + 1179
14 klee 0x000000000059245b
CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) +
251
15 klee 0x00000000005939bd
CexCachingSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 1245
16 klee 0x00000000005911c5
CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&)
+ 149
17 klee 0x000000000059e67d
IndependentSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 349
18 klee 0x0000000000574727
klee::TimingSolver::evaluate(klee::ExecutionState const&,
klee::ref<klee::Expr>, klee::Solver::Validity&) + 279
19 klee 0x000000000054e041
klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) +
225
20 klee 0x0000000000555859
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 10265
21 klee 0x000000000055876b
klee::Executor::run(klee::ExecutionState&) + 1787
22 klee 0x0000000000559104
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
1924
23 klee 0x000000000053e795 main + 8965
24 libc.so.6 0x00000031f9a1ee5d __libc_start_main + 253
25 klee 0x0000000000537009
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MemoryLimit.
c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MultipleFree
Resolution.c
Failed with signal(SIGABRT) at line 2
while running: klee --emit-all-errors MultipleFreeResolution.c.tmp1.bc
KLEE: output directory = "klee-out-101"
KLEE: WARNING: undefined reference to function: printf
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x0000000000cdc0ff
1 klee 0x0000000000cdc78d
2 libpthread.so.0 0x00000031f9e0eeb0
3 libc.so.6 0x00000031f9a330c5 gsignal + 53
4 libc.so.6 0x00000031f9a34a76 abort + 390
5 libc.so.6 0x00000031f9a2b905 __assert_fail + 245
6 klee 0x000000000060c710
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&) + 320
7 klee 0x00000000006101ad MINISAT::Solver::search(int, int) +
205
8 klee 0x00000000006107f2
MINISAT::Solver::solve(MINISAT::vec<MINISAT::Lit> const&) + 370
9 klee 0x00000000005eecd0
BEEV::BeevMgr::toSATandSolve(MINISAT::Solver&,
std::vector<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*,
std::allocator<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*>
>&) + 528
10 klee 0x00000000005f0ba9
BEEV::BeevMgr::CallSAT_ResultCheck(MINISAT::Solver&, BEEV::ASTNode const&,
BEEV::ASTNode const&) + 73
11 klee 0x00000000005f348b
BEEV::BeevMgr::TopLevelSAT(BEEV::ASTNode const&, BEEV::ASTNode const&) +
4107
12 klee 0x00000000005d4b5d vc_query + 365
13 klee 0x00000000005a4ddb
STPSolverImpl::computeInitialValues(klee::Query const&,
std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&,
std::vector<std::vector<unsigned char, std::allocator<unsigned char> >,
std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > >
>&, bool&) + 1179
14 klee 0x000000000059245b
CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) +
251
15 klee 0x00000000005939bd
CexCachingSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 1245
16 klee 0x00000000005911c5
CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&)
+ 149
17 klee 0x000000000059e67d
IndependentSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 349
18 klee 0x0000000000574727
klee::TimingSolver::evaluate(klee::ExecutionState const&,
klee::ref<klee::Expr>, klee::Solver::Validity&) + 279
19 klee 0x000000000054e041
klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) +
225
20 klee 0x0000000000555859
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 10265
21 klee 0x000000000055876b
klee::Executor::run(klee::ExecutionState&) + 1787
22 klee 0x0000000000559104
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
1924
23 klee 0x000000000053e795 main + 8965
24 libc.so.6 0x00000031f9a1ee5d __libc_start_main + 253
25 klee 0x0000000000537009
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MultipleRead
Resolution.c
Failed with signal(SIGABRT) at line 6
while running: klee MultipleReadResolution.c.tmp1.bc >
MultipleReadResolution.c.tmp1.log
KLEE: output directory = "klee-out-102"
KLEE: WARNING: undefined reference to function: fflush
KLEE: WARNING: undefined reference to function: puts
KLEE: WARNING: undefined reference to variable: stdout
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x0000000000cdc0ff
1 klee 0x0000000000cdc78d
2 libpthread.so.0 0x00000031f9e0eeb0
3 libc.so.6 0x00000031f9a330c5 gsignal + 53
4 libc.so.6 0x00000031f9a34a76 abort + 390
5 libc.so.6 0x00000031f9a2b905 __assert_fail + 245
6 klee 0x000000000060c710
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&) + 320
7 klee 0x00000000006101ad MINISAT::Solver::search(int, int) +
205
8 klee 0x00000000006107f2
MINISAT::Solver::solve(MINISAT::vec<MINISAT::Lit> const&) + 370
9 klee 0x00000000005eecd0
BEEV::BeevMgr::toSATandSolve(MINISAT::Solver&,
std::vector<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*,
std::allocator<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*>
>&) + 528
10 klee 0x00000000005f0ba9
BEEV::BeevMgr::CallSAT_ResultCheck(MINISAT::Solver&, BEEV::ASTNode const&,
BEEV::ASTNode const&) + 73
11 klee 0x00000000005f348b
BEEV::BeevMgr::TopLevelSAT(BEEV::ASTNode const&, BEEV::ASTNode const&) +
4107
12 klee 0x00000000005d4b5d vc_query + 365
13 klee 0x00000000005a4ddb
STPSolverImpl::computeInitialValues(klee::Query const&,
std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&,
std::vector<std::vector<unsigned char, std::allocator<unsigned char> >,
std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > >
>&, bool&) + 1179
14 klee 0x000000000059245b
CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) +
251
15 klee 0x00000000005939bd
CexCachingSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 1245
16 klee 0x00000000005911c5
CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&)
+ 149
17 klee 0x000000000059e67d
IndependentSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 349
18 klee 0x0000000000574727
klee::TimingSolver::evaluate(klee::ExecutionState const&,
klee::ref<klee::Expr>, klee::Solver::Validity&) + 279
19 klee 0x000000000054e041
klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) +
225
20 klee 0x0000000000555859
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 10265
21 klee 0x000000000055876b
klee::Executor::run(klee::ExecutionState&) + 1787
22 klee 0x0000000000559104
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
1924
23 klee 0x000000000053e795 main + 8965
24 libc.so.6 0x00000031f9a1ee5d __libc_start_main + 253
25 klee 0x0000000000537009
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MultipleReal
locResolution.c
Failed with signal(SIGABRT) at line 2
while running: klee MultipleReallocResolution.c.tmp1.bc
KLEE: output directory = "klee-out-103"
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x0000000000cdc0ff
1 klee 0x0000000000cdc78d
2 libpthread.so.0 0x00000031f9e0eeb0
3 libc.so.6 0x00000031f9a330c5 gsignal + 53
4 libc.so.6 0x00000031f9a34a76 abort + 390
5 libc.so.6 0x00000031f9a2b905 __assert_fail + 245
6 klee 0x000000000060c710
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&) + 320
7 klee 0x00000000006101ad MINISAT::Solver::search(int, int) +
205
8 klee 0x00000000006107f2
MINISAT::Solver::solve(MINISAT::vec<MINISAT::Lit> const&) + 370
9 klee 0x00000000005eecd0
BEEV::BeevMgr::toSATandSolve(MINISAT::Solver&,
std::vector<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*,
std::allocator<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*>
>&) + 528
10 klee 0x00000000005f0ba9
BEEV::BeevMgr::CallSAT_ResultCheck(MINISAT::Solver&, BEEV::ASTNode const&,
BEEV::ASTNode const&) + 73
11 klee 0x00000000005f348b
BEEV::BeevMgr::TopLevelSAT(BEEV::ASTNode const&, BEEV::ASTNode const&) +
4107
12 klee 0x00000000005d4b5d vc_query + 365
13 klee 0x00000000005a4ddb
STPSolverImpl::computeInitialValues(klee::Query const&,
std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&,
std::vector<std::vector<unsigned char, std::allocator<unsigned char> >,
std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > >
>&, bool&) + 1179
14 klee 0x000000000059245b
CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) +
251
15 klee 0x00000000005939bd
CexCachingSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 1245
16 klee 0x00000000005911c5
CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&)
+ 149
17 klee 0x000000000059e67d
IndependentSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 349
18 klee 0x0000000000574727
klee::TimingSolver::evaluate(klee::ExecutionState const&,
klee::ref<klee::Expr>, klee::Solver::Validity&) + 279
19 klee 0x000000000054e041
klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) +
225
20 klee 0x0000000000555859
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 10265
21 klee 0x000000000055876b
klee::Executor::run(klee::ExecutionState&) + 1787
22 klee 0x0000000000559104
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
1924
23 klee 0x000000000053e795 main + 8965
24 libc.so.6 0x00000031f9a1ee5d __libc_start_main + 253
25 klee 0x0000000000537009
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/MultipleWrit
eResolution.c
Failed with signal(SIGABRT) at line 6
while running: klee MultipleWriteResolution.c.tmp1.bc >
MultipleWriteResolution.c.tmp1.log
KLEE: output directory = "klee-out-104"
KLEE: WARNING: undefined reference to function: fflush
KLEE: WARNING: undefined reference to function: puts
KLEE: WARNING: undefined reference to variable: stdout
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x0000000000cdc0ff
1 klee 0x0000000000cdc78d
2 libpthread.so.0 0x00000031f9e0eeb0
3 libc.so.6 0x00000031f9a330c5 gsignal + 53
4 libc.so.6 0x00000031f9a34a76 abort + 390
5 libc.so.6 0x00000031f9a2b905 __assert_fail + 245
6 klee 0x000000000060c710
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&) + 320
7 klee 0x00000000006101ad MINISAT::Solver::search(int, int) +
205
8 klee 0x00000000006107f2
MINISAT::Solver::solve(MINISAT::vec<MINISAT::Lit> const&) + 370
9 klee 0x00000000005eecd0
BEEV::BeevMgr::toSATandSolve(MINISAT::Solver&,
std::vector<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*,
std::allocator<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*>
>&) + 528
10 klee 0x00000000005f0ba9
BEEV::BeevMgr::CallSAT_ResultCheck(MINISAT::Solver&, BEEV::ASTNode const&,
BEEV::ASTNode const&) + 73
11 klee 0x00000000005f348b
BEEV::BeevMgr::TopLevelSAT(BEEV::ASTNode const&, BEEV::ASTNode const&) +
4107
12 klee 0x00000000005d4b5d vc_query + 365
13 klee 0x00000000005a4ddb
STPSolverImpl::computeInitialValues(klee::Query const&,
std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&,
std::vector<std::vector<unsigned char, std::allocator<unsigned char> >,
std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > >
>&, bool&) + 1179
14 klee 0x000000000059245b
CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) +
251
15 klee 0x00000000005939bd
CexCachingSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 1245
16 klee 0x00000000005911c5
CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&)
+ 149
17 klee 0x000000000059e67d
IndependentSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 349
18 klee 0x0000000000574727
klee::TimingSolver::evaluate(klee::ExecutionState const&,
klee::ref<klee::Expr>, klee::Solver::Validity&) + 279
19 klee 0x000000000054e041
klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) +
225
20 klee 0x0000000000555859
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 10265
21 klee 0x000000000055876b
klee::Executor::run(klee::ExecutionState&) + 1787
22 klee 0x0000000000559104
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
1924
23 klee 0x000000000053e795 main + 8965
24 libc.so.6 0x00000031f9a1ee5d __libc_start_main + 253
25 klee 0x0000000000537009
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/NamedSeedMat
ching.c
Failed with exit(1) at line 7
while running: grep -q "a==3" NamedSeedMatching.c.tmp.log
child process exited abnormally
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/OneFreeError
.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/OneOutOfBoun
ds.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/Optimize.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/OverlappedEr
ror.c
Failed with exit(1) at line 3
while running: ls klee-last/ | grep .ktest | wc -l | grep 4
child process exited abnormally
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/PreferCex.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/RaiseAsm.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/ReallocFailu
re.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/ReplayPath.c
Failed with signal(SIGABRT) at line 7
while running: klee --replay-path ReplayPath.c.tmp1.path
ReplayPath.c.tmp2.bc > ReplayPath.c.tmp3.log
KLEE: output directory = "klee-out-113"
KLEE: WARNING: undefined reference to function: printf
klee: /home/dbl/Source/KLEE/klee-2.7/lib/Core/Executor.cpp:724:
klee::Executor::StatePair klee::Executor::fork(klee::ExecutionState&,
klee::ref<klee::Expr>, bool): Assertion `!branch && "hit invalid branch in
replay path mode"' failed.
0 klee 0x0000000000cdc0ff
1 klee 0x0000000000cdc78d
2 libpthread.so.0 0x00000031f9e0eeb0
3 libc.so.6 0x00000031f9a330c5 gsignal + 53
4 libc.so.6 0x00000031f9a34a76 abort + 390
5 libc.so.6 0x00000031f9a2b905 __assert_fail + 245
6 klee 0x000000000054fbb0
klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) +
7248
7 klee 0x0000000000555859
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 10265
8 klee 0x000000000055876b
klee::Executor::run(klee::ExecutionState&) + 1787
9 klee 0x0000000000559104
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
1924
10 klee 0x000000000053e795 main + 8965
11 libc.so.6 0x00000031f9a1ee5d __libc_start_main + 253
12 klee 0x0000000000537009
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/Searchers.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/SetForking.c
Failed with exit(1) at line 4
while running: grep "1 A" SetForking.c.tmp.uniq.log
child process exited abnormally
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/Vararg.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/WithLibc.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/WriteCov.c
Failed with exit(1) at line 2
while running: klee --exit-on-error --write-cov WriteCov.c.tmp2.bc
KLEE: output directory = "klee-out-134"
KLEE: WARNING: undefined reference to function: printf
KLEE: ERROR:
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26: invalid
klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
EXITING ON ERROR:
Error: invalid klee_assume call (provably false)
File: /home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c
Line: 26
Stack:
#0 00000063 in klee_range (start=0, end=2, name=48888624) at
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26
#1 00000016 in main () at
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/WriteCov.c:9
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/const_array_
opt1.c
Failed with signal(SIGABRT) at line 2
while running: klee --const-array-opt --max-time=10
--only-output-states-covering-new const_array_opt1.c.tmp.bc
>const_array_opt1.c.tmp.log
KLEE: output directory = "klee-out-135"
KLEE: WARNING: undefined reference to function: puts
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x0000000000cdc0ff
1 klee 0x0000000000cdc78d
2 libpthread.so.0 0x00000031f9e0eeb0
3 libc.so.6 0x00000031f9a330c5 gsignal + 53
4 libc.so.6 0x00000031f9a34a76 abort + 390
5 libc.so.6 0x00000031f9a2b905 __assert_fail + 245
6 klee 0x000000000060c710
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&) + 320
7 klee 0x00000000006101ad MINISAT::Solver::search(int, int) +
205
8 klee 0x00000000006107f2
MINISAT::Solver::solve(MINISAT::vec<MINISAT::Lit> const&) + 370
9 klee 0x00000000005eecd0
BEEV::BeevMgr::toSATandSolve(MINISAT::Solver&,
std::vector<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*,
std::allocator<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*>
>&) + 528
10 klee 0x00000000005f0ba9
BEEV::BeevMgr::CallSAT_ResultCheck(MINISAT::Solver&, BEEV::ASTNode const&,
BEEV::ASTNode const&) + 73
11 klee 0x00000000005f348b
BEEV::BeevMgr::TopLevelSAT(BEEV::ASTNode const&, BEEV::ASTNode const&) +
4107
12 klee 0x00000000005d4b5d vc_query + 365
13 klee 0x00000000005a4ddb
STPSolverImpl::computeInitialValues(klee::Query const&,
std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&,
std::vector<std::vector<unsigned char, std::allocator<unsigned char> >,
std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > >
>&, bool&) + 1179
14 klee 0x000000000059245b
CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) +
251
15 klee 0x00000000005939bd
CexCachingSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 1245
16 klee 0x00000000005911c5
CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&)
+ 149
17 klee 0x000000000059e67d
IndependentSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 349
18 klee 0x0000000000574727
klee::TimingSolver::evaluate(klee::ExecutionState const&,
klee::ref<klee::Expr>, klee::Solver::Validity&) + 279
19 klee 0x000000000054e041
klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) +
225
20 klee 0x0000000000555859
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 10265
21 klee 0x000000000055876b
klee::Executor::run(klee::ExecutionState&) + 1787
22 klee 0x0000000000559104
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
1924
23 klee 0x000000000053e795 main + 8965
24 libc.so.6 0x00000031f9a1ee5d __libc_start_main + 253
25 klee 0x0000000000537009
testcase
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Feature/dg.exp
completed in 15 seconds
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Programs/dg.exp ...
XFAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Programs/pcregrep.c
Failed with exit(1) at line 1
while running:
/home/dbl/Source/LLVM/llvm-2.7/llvm-gcc-bootstrap/llvm-gcc4.2-2.7-x86_64-lin
ux/bin/llvm-gcc -I/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../include
-emit-llvm -m32
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Programs/pcregrep.c
-emit-llvm -O0 -c -o pcregrep.c.tmp1.bc
In file included from /usr/include/features.h:386,
from /usr/include/setjmp.h:26,
from
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Programs/pcregrep.c:
7:
/usr/include/gnu/stubs.h:7:27: error: gnu/stubs-32.h: No such file or
directory
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Programs/pcregrep.c:
In function 'main':
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Programs/pcregrep.c:
321: warning: return type of 'main' is not 'int'
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Programs/pcregrep.c:
In function 'compile_regex':
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Programs/pcregrep.c:
7901: warning: incompatible implicit declaration of built-in function
'memcpy'
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Programs/pcregrep.c:
8907: warning: incompatible implicit declaration of built-in function
'memcpy'
testcase
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Programs/dg.exp
completed in 0 seconds
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Runtime/POSIX/dg.exp
...
testcase
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Runtime/POSIX/dg.exp
completed in 0 seconds
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Runtime/Uclibc/dg.ex
p ...
testcase
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Runtime/Uclibc/dg.ex
p completed in 0 seconds
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Solver/dg.exp ...
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Solver/FastCexSolver
.pc
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Solver/LargeIntegers
.pc
Failed with exit(1) at line 7
while running: grep "Array 0: a.16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5,
4, 3, 2, 1, 0" LargeIntegers.pc.tmp2
child process exited abnormally
testcase
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/Solver/dg.exp
completed in 0 seconds
Running
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/dg.exp
...
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-07-2
5-invalid-stp-array-binding-to-objectstate.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-07-3
0-unflushed-byte.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-08-0
1-bool-zext-in-call.ll
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-08-0
1-cache-unclear-on-overwrite-flushed.c
Failed with signal(SIGABRT) at line 2
while running: klee 2007-08-01-cache-unclear-on-overwrite-flushed.c.tmp1.bc
KLEE: output directory = "klee-out-20"
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x0000000000cdc0ff
1 klee 0x0000000000cdc78d
2 libpthread.so.0 0x00000031f9e0eeb0
3 libc.so.6 0x00000031f9a330c5 gsignal + 53
4 libc.so.6 0x00000031f9a34a76 abort + 390
5 libc.so.6 0x00000031f9a2b905 __assert_fail + 245
6 klee 0x000000000060c710
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&) + 320
7 klee 0x00000000006101ad MINISAT::Solver::search(int, int) +
205
8 klee 0x00000000006107f2
MINISAT::Solver::solve(MINISAT::vec<MINISAT::Lit> const&) + 370
9 klee 0x00000000005eecd0
BEEV::BeevMgr::toSATandSolve(MINISAT::Solver&,
std::vector<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*,
std::allocator<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*>
>&) + 528
10 klee 0x00000000005f0ba9
BEEV::BeevMgr::CallSAT_ResultCheck(MINISAT::Solver&, BEEV::ASTNode const&,
BEEV::ASTNode const&) + 73
11 klee 0x00000000005f348b
BEEV::BeevMgr::TopLevelSAT(BEEV::ASTNode const&, BEEV::ASTNode const&) +
4107
12 klee 0x00000000005d4b5d vc_query + 365
13 klee 0x00000000005a4ddb
STPSolverImpl::computeInitialValues(klee::Query const&,
std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&,
std::vector<std::vector<unsigned char, std::allocator<unsigned char> >,
std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > >
>&, bool&) + 1179
14 klee 0x000000000059245b
CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) +
251
15 klee 0x00000000005939bd
CexCachingSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 1245
16 klee 0x00000000005911c5
CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&)
+ 149
17 klee 0x000000000059e67d
IndependentSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 349
18 klee 0x0000000000574727
klee::TimingSolver::evaluate(klee::ExecutionState const&,
klee::ref<klee::Expr>, klee::Solver::Validity&) + 279
19 klee 0x000000000054e041
klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) +
225
20 klee 0x0000000000555859
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 10265
21 klee 0x000000000055876b
klee::Executor::run(klee::ExecutionState&) + 1787
22 klee 0x0000000000559104
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
1924
23 klee 0x000000000053e795 main + 8965
24 libc.so.6 0x00000031f9a1ee5d __libc_start_main + 253
25 klee 0x0000000000537009
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-08-0
6-64bit-shift.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-08-0
6-access-after-free.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-08-0
8-free-zero.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-08-1
6-invalid-constant-value.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-08-1
6-valid-write-to-freed-object.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-10-1
1-free-of-alloca.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-10-1
1-illegal-access-after-free-and-branch.c
Failed with signal(SIGABRT) at line 2
while running: klee --optimize
2007-10-11-illegal-access-after-free-and-branch.c.tmp1.bc
KLEE: output directory = "klee-out-27"
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x0000000000cdc0ff
1 klee 0x0000000000cdc78d
2 libpthread.so.0 0x00000031f9e0eeb0
3 libc.so.6 0x00000031f9a330c5 gsignal + 53
4 libc.so.6 0x00000031f9a34a76 abort + 390
5 libc.so.6 0x00000031f9a2b905 __assert_fail + 245
6 klee 0x000000000060c710
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&) + 320
7 klee 0x00000000006101ad MINISAT::Solver::search(int, int) +
205
8 klee 0x00000000006107f2
MINISAT::Solver::solve(MINISAT::vec<MINISAT::Lit> const&) + 370
9 klee 0x00000000005eecd0
BEEV::BeevMgr::toSATandSolve(MINISAT::Solver&,
std::vector<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*,
std::allocator<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*>
>&) + 528
10 klee 0x00000000005f0ba9
BEEV::BeevMgr::CallSAT_ResultCheck(MINISAT::Solver&, BEEV::ASTNode const&,
BEEV::ASTNode const&) + 73
11 klee 0x00000000005f348b
BEEV::BeevMgr::TopLevelSAT(BEEV::ASTNode const&, BEEV::ASTNode const&) +
4107
12 klee 0x00000000005d4b5d vc_query + 365
13 klee 0x00000000005a4ddb
STPSolverImpl::computeInitialValues(klee::Query const&,
std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&,
std::vector<std::vector<unsigned char, std::allocator<unsigned char> >,
std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > >
>&, bool&) + 1179
14 klee 0x000000000059245b
CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) +
251
15 klee 0x00000000005939bd
CexCachingSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 1245
16 klee 0x00000000005911c5
CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&)
+ 149
17 klee 0x000000000059e67d
IndependentSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 349
18 klee 0x0000000000574727
klee::TimingSolver::evaluate(klee::ExecutionState const&,
klee::ref<klee::Expr>, klee::Solver::Validity&) + 279
19 klee 0x000000000054e041
klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) +
225
20 klee 0x0000000000555859
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 10265
21 klee 0x000000000055876b
klee::Executor::run(klee::ExecutionState&) + 1787
22 klee 0x0000000000559104
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
1924
23 klee 0x000000000053e795 main + 8965
24 libc.so.6 0x00000031f9a1ee5d __libc_start_main + 253
25 klee 0x0000000000537009
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2007-10-1
2-failed-make-symbolic-after-copy.c
Failed with signal(SIGABRT) at line 2
while running: klee 2007-10-12-failed-make-symbolic-after-copy.c.tmp1.bc
KLEE: output directory = "klee-out-28"
klee: /home/dbl/Source/KLEE/klee-2.7/stp/sat/Solver.cpp:298: void
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&): Assertion `confl != __null' failed.
0 klee 0x0000000000cdc0ff
1 klee 0x0000000000cdc78d
2 libpthread.so.0 0x00000031f9e0eeb0
3 libc.so.6 0x00000031f9a330c5 gsignal + 53
4 libc.so.6 0x00000031f9a34a76 abort + 390
5 libc.so.6 0x00000031f9a2b905 __assert_fail + 245
6 klee 0x000000000060c710
MINISAT::Solver::analyze(MINISAT::Clause*, MINISAT::vec<MINISAT::Lit>&,
int&) + 320
7 klee 0x00000000006101ad MINISAT::Solver::search(int, int) +
205
8 klee 0x00000000006107f2
MINISAT::Solver::solve(MINISAT::vec<MINISAT::Lit> const&) + 370
9 klee 0x00000000005eecd0
BEEV::BeevMgr::toSATandSolve(MINISAT::Solver&,
std::vector<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*,
std::allocator<std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> >*>
>&) + 528
10 klee 0x00000000005f0ba9
BEEV::BeevMgr::CallSAT_ResultCheck(MINISAT::Solver&, BEEV::ASTNode const&,
BEEV::ASTNode const&) + 73
11 klee 0x00000000005f348b
BEEV::BeevMgr::TopLevelSAT(BEEV::ASTNode const&, BEEV::ASTNode const&) +
4107
12 klee 0x00000000005d4b5d vc_query + 365
13 klee 0x00000000005a4ddb
STPSolverImpl::computeInitialValues(klee::Query const&,
std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&,
std::vector<std::vector<unsigned char, std::allocator<unsigned char> >,
std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > >
>&, bool&) + 1179
14 klee 0x000000000059245b
CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) +
251
15 klee 0x00000000005939bd
CexCachingSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 1245
16 klee 0x00000000005911c5
CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&)
+ 149
17 klee 0x000000000059e67d
IndependentSolver::computeValidity(klee::Query const&,
klee::Solver::Validity&) + 349
18 klee 0x0000000000574727
klee::TimingSolver::evaluate(klee::ExecutionState const&,
klee::ref<klee::Expr>, klee::Solver::Validity&) + 279
19 klee 0x000000000054e041
klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) +
225
20 klee 0x0000000000555859
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 10265
21 klee 0x000000000055876b
klee::Executor::run(klee::ExecutionState&) + 1787
22 klee 0x0000000000559104
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
1924
23 klee 0x000000000053e795 main + 8965
24 libc.so.6 0x00000031f9a1ee5d __libc_start_main + 253
25 klee 0x0000000000537009
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2008-02-1
1-phi-nodes-after-invoke.ll
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2008-03-0
4-free-of-global.c
FAIL:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2008-03-1
1-free-of-malloc-zero.c
Failed with exit(1) at line 2
while running: klee --exit-on-error 2008-03-11-free-of-malloc-zero.c.tmp1.bc
KLEE: output directory = "klee-out-31"
KLEE: ERROR:
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26: invalid
klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
EXITING ON ERROR:
Error: invalid klee_assume call (provably false)
File: /home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c
Line: 26
Stack:
#0 00000069 in klee_range (start=0, end=4, name=38132432) at
/home/dbl/Source/KLEE/klee-2.7/runtime/Intrinsic/klee_range.c:26
#1 00000031 in main ()
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2008-04-1
0-bad-alloca-free.c
PASS:
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/2008-05-2
3-gep-with-global-const.c
testcase
/home/dbl/Source/KLEE/klee-2.7/object-no-uClibc/../test/regression/dg.exp
completed in 1 seconds
=== Summary ===
# of expected passes 61
# of unexpected failures 24
# of expected failures 2
runtest completed at Tue Mar 1 08:24:03 2011
