Hi, sorry I notice that I used an the new version of Clang. It works now. Many thanks
On 5 July 2017 at 02:43, [email protected] <[email protected]> wrote: > Sorry it was my mistake. Please replace "sudo apt install wllvm" with the > following two commands: > > sudo apt install python-pip > sudo pip install wllvm > > Best, > Andrew > > > > On Wednesday, July 5, 2017, 7:35:00 AM GMT+8, Nourah mmm < > [email protected]> wrote: > > > Thank you very much for your replay. > > I tried to do that, however, its print extract-bc: command not found. > > I'm trying to extract the bc from SPEC cpu2006 Integer benchmarks. So I > did the following. > > 1. sudo apt install wllvm > 2. LLVM_COMPILER=clang CC=wllvm make --> here I use clang version 3.4 > and I just write wllvm without a path. > 3. Then, it generate the .o files and an executable program(mcf) > 4. extract-bc mcf > > Thank you > Nora > > On 4 July 2017 at 03:04, [email protected] <[email protected]> > wrote: > > I suppose what you want is to produce a bitcode for running with KLEE. You > can probably > do 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 > <https://github.com/travitch/whole-program-llvm> See also an installation > instruction as the Step 2 here: Testing Coreutils · KLEE > <https://klee.github.io/tutorials/testing-coreutils/> > > Testing Coreutils · KLEE > > <https://klee.github.io/tutorials/testing-coreutils/> > > > 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 assuming > that 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 > <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev> > > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
