I'm having trouble using KLEE on Ubuntu 11.10. I've had to define some
macros and modify kernel_types.h slightly for consistency with the Linux
headers. Five tests are still failing in the POSIX suite. It appears to
be due to accessing the file system. Has anyone else had issues in this
environment or can recommend how to go about debugging it?
For DirConsistency and DirSeek there are assertions failures when
asserting that something is returned from the file system access.
For FD_Fail and FD_Fail2 the read statements which are supposed to
succeed also fail.
For Isatty the correct tests are generated but the fprintf statements
have no effect.
I've attached the testrun.log for reference.
--
Regards,
Daniel Wainwright
Test Run By djwainwr on Thu Dec 15 12:03:27 2011
Target is x86_64-unknown-linux-gnu
Host is x86_64-redhat-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.
WARNING: Assuming target board is the local machine (which is probably wrong).
You may need to set your DEJAGNU environment variable.
Running /home/djwainwr/klee/test/CXX/dg.exp ...
PASS: /home/djwainwr/klee/test/CXX/ArrayNew.cpp
PASS: /home/djwainwr/klee/test/CXX/New.cpp
PASS: /home/djwainwr/klee/test/CXX/SimpleVirtual.cpp
PASS: /home/djwainwr/klee/test/CXX/StaticConstructor.cpp
PASS: /home/djwainwr/klee/test/CXX/StaticDestructor.cpp
PASS: /home/djwainwr/klee/test/CXX/Trivial.cpp
testcase /home/djwainwr/klee/test/CXX/dg.exp completed in 1 seconds
Running /home/djwainwr/klee/test/Coverage/dg.exp ...
PASS: /home/djwainwr/klee/test/Coverage/ReadArgs.c
PASS: /home/djwainwr/klee/test/Coverage/ReplayOutDir.c
testcase /home/djwainwr/klee/test/Coverage/dg.exp completed in 2 seconds
Running /home/djwainwr/klee/test/Dogfood/dg.exp ...
PASS: /home/djwainwr/klee/test/Dogfood/ImmutableSet.cpp
testcase /home/djwainwr/klee/test/Dogfood/dg.exp completed in 33 seconds
Running /home/djwainwr/klee/test/Expr/Lexer/dg.exp ...
PASS: /home/djwainwr/klee/test/Expr/Lexer/Numbers.pc
testcase /home/djwainwr/klee/test/Expr/Lexer/dg.exp completed in 0 seconds
Running /home/djwainwr/klee/test/Expr/Parser/dg.exp ...
PASS: /home/djwainwr/klee/test/Expr/Parser/Concat64.pc
PASS: /home/djwainwr/klee/test/Expr/Parser/ConstantFolding.pc
PASS: /home/djwainwr/klee/test/Expr/Parser/Exprs.pc
PASS: /home/djwainwr/klee/test/Expr/Parser/MultiByteReads.pc
PASS: /home/djwainwr/klee/test/Expr/Parser/Simplify.pc
PASS: /home/djwainwr/klee/test/Expr/Parser/TypeChecking.pc
testcase /home/djwainwr/klee/test/Expr/Parser/dg.exp completed in 1 seconds
Running /home/djwainwr/klee/test/Expr/dg.exp ...
PASS: /home/djwainwr/klee/test/Expr/Evaluate.pc
XFAIL: /home/djwainwr/klee/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/djwainwr/klee/test/Expr/dg.exp completed in 0 seconds
Running /home/djwainwr/klee/test/Feature/dg.exp ...
PASS: /home/djwainwr/klee/test/Feature/Alias.c
PASS: /home/djwainwr/klee/test/Feature/AliasFunction.c
PASS: /home/djwainwr/klee/test/Feature/AliasFunctionExit.c
PASS: /home/djwainwr/klee/test/Feature/AsmAddresses.c
PASS: /home/djwainwr/klee/test/Feature/BitcastAlias.ll
PASS: /home/djwainwr/klee/test/Feature/ByteSwap.c
PASS: /home/djwainwr/klee/test/Feature/CallToUndefinedExternal.cpp
PASS: /home/djwainwr/klee/test/Feature/CheckForImpliedValue.c
PASS: /home/djwainwr/klee/test/Feature/CheckMemoryAccess.c
PASS: /home/djwainwr/klee/test/Feature/ConstantStruct.ll
PASS: /home/djwainwr/klee/test/Feature/CopyOnWrite.c
PASS: /home/djwainwr/klee/test/Feature/DanglingConcreteReadExpr.c
PASS: /home/djwainwr/klee/test/Feature/DefineFixedObject.c
PASS: /home/djwainwr/klee/test/Feature/DoubleFree.c
PASS: /home/djwainwr/klee/test/Feature/DumpStatesOnHalt.c
PASS: /home/djwainwr/klee/test/Feature/Envp.c
PASS: /home/djwainwr/klee/test/Feature/ExprLogging.c
PASS: /home/djwainwr/klee/test/Feature/ExternalWeakLinkage.c
PASS: /home/djwainwr/klee/test/Feature/Float.c
PASS: /home/djwainwr/klee/test/Feature/FunctionPointer.c
PASS: /home/djwainwr/klee/test/Feature/GetElementPtr.ll
PASS: /home/djwainwr/klee/test/Feature/GetValue.c
PASS: /home/djwainwr/klee/test/Feature/InAndOutOfBounds.c
PASS: /home/djwainwr/klee/test/Feature/IndirectCallToBuiltin.c
PASS: /home/djwainwr/klee/test/Feature/IndirectCallToExternal.c
PASS: /home/djwainwr/klee/test/Feature/InsertExtractValue.ll
PASS: /home/djwainwr/klee/test/Feature/InvalidBitfieldAccess.c
PASS: /home/djwainwr/klee/test/Feature/IsSymbolic.c
PASS: /home/djwainwr/klee/test/Feature/KleeReportError.c
PASS: /home/djwainwr/klee/test/Feature/LargeReturnTypes.cpp
PASS: /home/djwainwr/klee/test/Feature/LongDouble.cpp
PASS: /home/djwainwr/klee/test/Feature/LongDoubleSupport.c
PASS: /home/djwainwr/klee/test/Feature/LowerSwitch.c
PASS: /home/djwainwr/klee/test/Feature/MakeConcreteSymbolic.c
PASS: /home/djwainwr/klee/test/Feature/MakeSymbolicName.c
PASS: /home/djwainwr/klee/test/Feature/MemoryLimit.c
PASS: /home/djwainwr/klee/test/Feature/MultipleFreeResolution.c
PASS: /home/djwainwr/klee/test/Feature/MultipleReadResolution.c
PASS: /home/djwainwr/klee/test/Feature/MultipleReallocResolution.c
PASS: /home/djwainwr/klee/test/Feature/MultipleWriteResolution.c
PASS: /home/djwainwr/klee/test/Feature/NamedSeedMatching.c
PASS: /home/djwainwr/klee/test/Feature/OneFreeError.c
PASS: /home/djwainwr/klee/test/Feature/OneOutOfBounds.c
PASS: /home/djwainwr/klee/test/Feature/Optimize.c
PASS: /home/djwainwr/klee/test/Feature/OverlappedError.c
PASS: /home/djwainwr/klee/test/Feature/PreferCex.c
PASS: /home/djwainwr/klee/test/Feature/RaiseAsm.c
PASS: /home/djwainwr/klee/test/Feature/ReallocFailure.c
PASS: /home/djwainwr/klee/test/Feature/ReplayPath.c
PASS: /home/djwainwr/klee/test/Feature/Searchers.c
PASS: /home/djwainwr/klee/test/Feature/SetForking.c
PASS: /home/djwainwr/klee/test/Feature/Vararg.c
PASS: /home/djwainwr/klee/test/Feature/WithLibc.c
PASS: /home/djwainwr/klee/test/Feature/WriteCov.c
PASS: /home/djwainwr/klee/test/Feature/const_array_opt1.c
testcase /home/djwainwr/klee/test/Feature/dg.exp completed in 24 seconds
Running /home/djwainwr/klee/test/Programs/dg.exp ...
XFAIL: /home/djwainwr/klee/test/Programs/pcregrep.c
Failed with signal(SIGABRT) at line 2
while running: klee --libc=klee --exit-on-error pcregrep.c.tmp1.bc 2 2
WARNING: Linking two modules of different data layouts!
WARNING: Linking two modules of different target triples!
WARNING: Linking two modules of different data layouts!
WARNING: Linking two modules of different target triples!
WARNING: Linking two modules of different data layouts!
WARNING: Linking two modules of different target triples!
WARNING: Linking two modules of different data layouts!
WARNING: Linking two modules of different target triples!
WARNING: Linking two modules of different data layouts!
WARNING: Linking two modules of different target triples!
KLEE: output directory = "klee-out-13"
WARNING: Linking two modules of different data layouts!
WARNING: Linking two modules of different target triples!
WARNING: Linking two modules of different data layouts!
WARNING: Linking two modules of different target triples!
WARNING: Linking two modules of different data layouts!
WARNING: Linking two modules of different target triples!
WARNING: Linking two modules of different data layouts!
WARNING: Linking two modules of different target triples!
KLEE: WARNING: undefined reference to function: __errno_location
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING: calling external: __ctype_b_loc()
KLEE: ERROR: /home/djwainwr/klee/runtime/klee-libc/strtol.c:63: memory error:
out of bound pointer
KLEE: NOTE: now ignoring this error at this location
EXITING ON ERROR:
Error: memory error: out of bound pointer
File: /home/djwainwr/klee/runtime/klee-libc/strtol.c
Line: 63
Stack:
#0 00024015 in strtol (nptr=429379888, endptr=0, base=10) at
/home/djwainwr/klee/runtime/klee-libc/strtol.c:63
#1 00023913 in atoi (str=429379888) at
/home/djwainwr/klee/runtime/klee-libc/atoi.c:36
#2 00000212 in main (llvm_cbe_argc=3, llvm_cbe_argv=432638992)
Info:
address: 1712501240
next: object at 249113393856 of size 768
MO45[768] (no allocation info)
prev: object at 432827792 of size 4
MO210[4] allocated at main(): %llvm_cbe_tmp61_i__PHI_TEMPORARY
= alloca %struct.l_struct_2E_pcre*
pure virtual method called
terminate called without an active exception
0 klee 0x0000000000d0ee5f
1 klee 0x0000000000d11122
2 libpthread.so.0 0x0000003a0100e7c0
3 libc.so.6 0x0000003a00430265 gsignal + 53
4 libc.so.6 0x0000003a00431d10 abort + 272
5 libstdc++.so.6 0x0000003f784bec44 __gnu_cxx::__verbose_terminate_handler()
+ 276
6 libstdc++.so.6 0x0000003f784bcdb6
7 libstdc++.so.6 0x0000003f784bcde3
8 libstdc++.so.6 0x0000003f784bd2ef
9 klee 0x0000000000d03b09 llvm::raw_ostream::write(char const*,
unsigned long) + 185
10 klee 0x0000000000d03b09 llvm::raw_ostream::write(char const*,
unsigned long) + 185
11 klee 0x0000000000cb185c llvm::Value::~Value() + 812
12 klee 0x0000000000c30976
llvm::GetElementPtrConstantExpr::~GetElementPtrConstantExpr() + 54
13 klee 0x0000000000c8031a llvm::LLVMContextImpl::~LLVMContextImpl()
+ 570
14 klee 0x0000000000c7d031 llvm::LLVMContext::~LLVMContext() + 17
15 klee 0x0000000000c7db4e
llvm::object_deleter<llvm::LLVMContext>::call(void*) + 14
16 klee 0x0000000000cf0eed llvm::ManagedStaticBase::destroy() const
+ 45
17 klee 0x0000000000cf0f55 llvm::llvm_shutdown() + 21
18 libc.so.6 0x0000003a004333a5 exit + 229
19 klee 0x0000000000547cd2
KleeHandler::processTestCase(klee::ExecutionState const&, char const*, char
const*) + 98
20 klee 0x00000000005569a9
klee::Executor::terminateStateOnError(klee::ExecutionState&, llvm::Twine
const&, char const*, llvm::Twine const&) + 793
21 klee 0x000000000055b9a3
klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool,
klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 3763
22 klee 0x000000000055f319
klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*)
+ 4265
23 klee 0x000000000056343e
klee::Executor::run(klee::ExecutionState&) + 1774
24 klee 0x00000000005667c4
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 2068
25 klee 0x000000000054acd1 main + 9105
26 libc.so.6 0x0000003a0041d994 __libc_start_main + 244
27 klee 0x0000000000541fb9 __gxx_personality_v0 + 753
testcase /home/djwainwr/klee/test/Programs/dg.exp completed in 1 seconds
Running /home/djwainwr/klee/test/Runtime/POSIX/dg.exp ...
PASS: /home/djwainwr/klee/test/Runtime/POSIX/DirConsistency.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/DirSeek.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/FDNumbers.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/FD_Fail.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/FD_Fail2.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/Fcntl.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/FilePerm.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/FreeArgv.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/Getenv.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/Ioctl.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/Isatty.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/PrgName.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/Read1.c
XPASS: /home/djwainwr/klee/test/Runtime/POSIX/SELinux.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/SeedAndFail.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/Stdin.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/Write1.c
PASS: /home/djwainwr/klee/test/Runtime/POSIX/Write2.c
testcase /home/djwainwr/klee/test/Runtime/POSIX/dg.exp completed in 8 seconds
Running /home/djwainwr/klee/test/Runtime/Uclibc/dg.exp ...
PASS:
/home/djwainwr/klee/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c
PASS:
/home/djwainwr/klee/test/Runtime/Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c
PASS: /home/djwainwr/klee/test/Runtime/Uclibc/Environ.c
testcase /home/djwainwr/klee/test/Runtime/Uclibc/dg.exp completed in 0 seconds
Running /home/djwainwr/klee/test/Solver/dg.exp ...
PASS: /home/djwainwr/klee/test/Solver/FastCexSolver.pc
PASS: /home/djwainwr/klee/test/Solver/LargeIntegers.pc
testcase /home/djwainwr/klee/test/Solver/dg.exp completed in 0 seconds
Running /home/djwainwr/klee/test/regression/dg.exp ...
PASS:
/home/djwainwr/klee/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c
PASS: /home/djwainwr/klee/test/regression/2007-07-30-unflushed-byte.c
PASS: /home/djwainwr/klee/test/regression/2007-08-01-bool-zext-in-call.ll
PASS:
/home/djwainwr/klee/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c
PASS: /home/djwainwr/klee/test/regression/2007-08-06-64bit-shift.c
PASS: /home/djwainwr/klee/test/regression/2007-08-06-access-after-free.c
PASS: /home/djwainwr/klee/test/regression/2007-08-08-free-zero.c
PASS: /home/djwainwr/klee/test/regression/2007-08-16-invalid-constant-value.c
PASS:
/home/djwainwr/klee/test/regression/2007-08-16-valid-write-to-freed-object.c
PASS: /home/djwainwr/klee/test/regression/2007-10-11-free-of-alloca.c
PASS:
/home/djwainwr/klee/test/regression/2007-10-11-illegal-access-after-free-and-branch.c
PASS:
/home/djwainwr/klee/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
PASS: /home/djwainwr/klee/test/regression/2008-02-11-phi-nodes-after-invoke.ll
PASS: /home/djwainwr/klee/test/regression/2008-03-04-free-of-global.c
PASS: /home/djwainwr/klee/test/regression/2008-03-11-free-of-malloc-zero.c
PASS: /home/djwainwr/klee/test/regression/2008-04-10-bad-alloca-free.c
PASS: /home/djwainwr/klee/test/regression/2008-05-23-gep-with-global-const.c
testcase /home/djwainwr/klee/test/regression/dg.exp completed in 1 seconds
=== Summary ===
# of expected passes 111
# of unexpected successes 1
# of expected failures 2
runtest completed at Thu Dec 15 12:04:46 2011
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
