[klee-dev] Quick confirmation: Ada testing possibilities with KLEE

[Buck, Erik Marlow]

Before I attempt to cobble together a system using KLEE and the gcc/gnat/llvm tool suite, I'd like to know if anyone has blazed this trail already. I noticed several Ada related comments in the archives, but none confirmed success using KLEE with binaries (or byte code)  produced from Ada source code.

Do you have any advice for setting up KLEE based testing for old Ada projects?

Background:
 
I have been using combinations of random data driven testing and hand written test cases to achieve high code/path coverage during automated testing. In the past, most testing was for machine instruction set validation/regression. I build hardware emulators and need to validate that an emulator produces the same results including side effects as a hardware implementation.

I am excited to try KLEE for machine instruction set validation - I already produce LLVM IR in many cases to leverage the IR level optimizations provided by LLVM and avoid excessive test case equivalency/duplication …

But first, I have been tasked to generate a set of test cases that achieves high code/path coverage for a large body of existing Ada code. I've attempted the random data approach I've used in the past with underwhelming results so far.

I think symbolic execution and constraint solving may be the best path forward.