[klee-dev] -DSPEC_CPU -DNDEBUG -DSPEC_CPU_LP64

[asantosa1999 at gmail.com]

Sorry it was my mistake. Please replace "sudo apt install wllvm"  with the following two commands:
sudo apt install python-pipsudo 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. 
   
   - sudo apt install wllvm
   - LLVM_COMPILER=clang CC=wllvm make --> here I use clang version 3.4 and I just write wllvm without a path.
   - Then, it generate the .o files and an executable program(mcf)   

   - 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 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 <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


-------------- next part --------------
HTML attachment scrubbed and removed