[klee-dev] Writing tests for KLEE

[Marko Dimjašević]

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ć <marko at cs.utah.edu> .   University of Utah
https://dimjasevic.net/marko         . PGP key ID: 1503F0AA
Learn email self-defense!  https://emailselfdefense.fsf.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20160614/da7c76a5/attachment.sig>