On Tue, 2016-06-14 at 09:16 +0200, Martin Nowack wrote: > No, it is not outdated, according to unit tests, it’s the current > state of the KLEE project.
Martin, thank you for the clarification!
I've been trying to understand how to run these unit tests. When in the
root directory of KLEE (version 1.2.0 + all commits to the master branch
up to this date), this is what I get:
$ $ make unittests
llvm[0]: Running unittests test suite
make[1]: Entering directory '/home/marko/research/klee/unittests'
make[2]: Entering directory '/home/marko/research/klee/unittests/Expr'
llvm[2]: Compiling ExprTest.cpp for Release+Asserts build
llvm[2]: Linking Release+Asserts unit test Expr (without symbols)
llvm[2]: ======= Finished Linking Release+Asserts Unit test Expr
(without symbols)
="/home/marko/research/klee/Release+Asserts/lib${:+:}$" Release
+Asserts/ExprTests
/bin/sh: 1: Bad substitution
/usr/lib/llvm-3.4/build/unittests/Makefile.unittest:60: recipe for
target 'unitcheck' failed
make[2]: *** [unitcheck] Error 2
make[2]: Leaving directory '/home/marko/research/klee/unittests/Expr'
/home/marko/research/klee/Makefile.rules:757: recipe for target
'unitcheck' failed
make[1]: *** [unitcheck] Error 1
make[1]: Leaving directory '/home/marko/research/klee/unittests'
/home/marko/research/klee/Makefile.rules:1906: recipe for target
'unittests' failed
make: *** [unittests] Error 2
I have the GoogleTest framework 1.7.0 (as shared libraries) and STP
2.1.1 installed system-wide, i.e. under /usr. My OS is Debian GNU/Linux
8.5, the amd64 architecture. This is how I configured KLEE:
$ ./configure --with-llvmsrc=/usr/lib/llvm-3.4/build
--with-llvmobj=/usr/lib/llvm-3.4/build --with-llvmcc=/usr/bin/clang-3.4
--with-llvmcxx=/usr/bin/clang++-3.4 --enable-posix-runtime
--with-stp=/usr
In KLEE's Developer's Guide it says to do this for internal tests:
$ cd path/to/klee/build
$ make unittests
Is the 'build' directory literally supposed to be there? I guess not as
I get the 'Release+Asserts' directory when building, but it has no
Makefile. Instead, I ran the 'make unittests' command from the root of
the code base.
Finally, I did look
at /usr/lib/llvm-3.4/build/unittests/Makefile.unittest that is mentioned
in the error message, but I can't figure out what wasn't properly
substituted.
--
Regards,
Marko Dimjašević <ma...@cs.utah.edu> . University of Utah
https://dimjasevic.net/marko . PGP key ID: 1503F0AA
Learn email self-defense! https://emailselfdefense.fsf.org
signature.asc
Description: This is a digitally signed message part
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
