[klee-dev] Writing tests for KLEE

[Marko Dimjašević]

Dear all,

I'm implementing the Firehose output format for KLEE. So far I only
created a library for Firehose data structures, but I'd like to write
tests for them.

At the Developer's Guide for KLEE:

https://klee.github.io/docs/developers-guide/#regression-testing-framework

You say there are two levels of testing KLEE: external and internal.
External is done by calling KLEE from the command line with needed
arguments. This is done through llvm-lit. The internal level consists of
writing unit tests in the GoogleTest framework.

Unit tests for KLEE should be under the unittests directory. I see only
3 meaningful C++ files in there. Therefore, can you confirm this is how
unit tests should be written for KLEE, or is the guide outdated?


-- 
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/20160613/66bb8458/attachment.sig>