I suppose what you want is to produce a bitcode for running with KLEE. You can probablydo a normal build procedure for the program, but with replacing your C compiler with wllvm.wllvm is available here: https://github.com/travitch/whole-program-llvm See also an installationinstruction as the Step 2 here: Testing Coreutils · KLEE
| | | | Testing Coreutils · KLEE | | | Alternatively, on Ubuntu 16.04, you can do sudo apt install wllvm to install wllvm. I assume you would normally build the program using "make". In that case, and assumingthat both clang and wllvm are in your PATH, the following might work to produce the binary: LLVM_COMPILER=clang CC=wllvm make And then you can do: extract-bc program To get the program.bc for running with KLEE. Best,Andrew On Tuesday, July 4, 2017, 9:05:49 AM GMT+8, Nourah mmm <[email protected]> wrote: Hi, I'm testing a program that compress and decompress files. For C compilation I'm using these flags: -DSPEC_CPU-DNDEBUG -DSPEC_CPU_LP64 How could I use these in KLEE? Thank you Nora _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
