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ć <[email protected]> .   University of Utah
https://dimjasevic.net/marko         . PGP key ID: 1503F0AA
Learn email self-defense!  https://emailselfdefense.fsf.org

Attachment: signature.asc
Description: This is a digitally signed message part

_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to