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, asantosa1...@gmail.com <asantosa1...@gmail.com>
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
> 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 <dnoo...@gmail.com>
> 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
> klee-dev@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to