[klee-dev] how to compile gnu utility 'find' using klee-gcc?

[Hongxu Chen]

Hi Yi,

   I guess you need to read the original makefile and do some wrapper
yourself instead of using klee-gcc.

   From KLEE's "coreutils case study" page, Step 2(
http://ccadar.github.io/klee/TestingCoreutils.html), There are such
sentences:

> It depends on the actual project what the best way to do this is. For
coreutils, we use a helper script klee-gcc, which acts like llvm-gcc but
adds additional arguments to cause it > to emit LLVM bitcode files and to
call llvm-ld to link executables. This is *not* a general solution, and
your mileage may vary.

   klee-gcc is a python script specified for coreutils bitcode generation.

   To build bc instead of native code for general purpose, I think you can
try wllvm.

Thanks,
Hongxu Chen



On Thu, Oct 31, 2013 at 9:28 AM, Yi Zhou <zhouyi198925 at gmail.com> wrote:

> Hi,
>
> I want to compile gnu utility 'find' to get an executed *.bc file, so I
> use the following commands:
>
> ./configure CC=/path/to/klee-gcc LD=/path/to/llvm-ld
> make
> make install
>
> However, at the end I did not get any *.bc file, and the generated file
> 'find' is said to "Invalid bitcode signature",but I can use the similar
> configure command to compile bosybox successfully. where is the error, and
> what should I do? Thank you all.
>
> Yi Zhou
> Institute Of Software
> Chinese Academy of Sciences
>
> _______________________________________________
> 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