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

[Yi Zhou]

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

[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

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

Hi,
I want to compile gnu utility 'find' to get an executed *.bc file, so I
./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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Qiuping Yi]

Thank you, we have solved this problem following your instructions.


--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences

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

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

Hi,
I want to compile gnu utility 'find' to get an executed *.bc file, so I
./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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Hongxu Chen]

My pleasure. And glad to here that.

Post by Qiuping Yi
Thank you, we have solved this problem following your instructions.
--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences

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

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

Hi,
I want to compile gnu utility 'find' to get an executed *.bc file, so I
./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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev