[klee-dev] -DSPEC_CPU -DNDEBUG -DSPEC_CPU_LP64

[Nourah mmm]

Thank you very much Andrew. I'm able now to extract the bc file. However,
when I run klee on it. I relieved the following message:

~/klee/examples/test$ myklee --emit-all-errors --allow-external-sym-calls
--optimize --libc=uclibc --posix-runtime --max-memory=1000 ./mcf.bc
KLEE: ERROR: error loading program './mcf.bc': Invalid value

Do you know the reason of this error?

Thanks a lot
Nora

On 5 July 2017 at 02:43, asantosa1999 at gmail.com <asantosa1999 at gmail.com>
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 <
> dnoorah at gmail.com> 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, asantosa1999 at gmail.com <asantosa1999 at 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
> <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 <dnoorah at 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 at imperial.ac.uk
> https://mailman.ic.ac.uk/ mailman/listinfo/klee-dev
> <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>
>
>
-------------- next part --------------
HTML attachment scrubbed and removed