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

Hongxu Chen leftcopy.chx at gmail.com
Fri Nov 1 01:44:49 GMT 2013


My pleasure. And glad to here that.


On Fri, Nov 1, 2013 at 9:31 AM, Qiuping Yi <yiqiuping at gmail.com> wrote:

> Thank you, we have solved this problem following your instructions.
>
>
> --------------------------------------------
> Qiuping Yi
>
> Institute Of Software
> Chinese Academy of Sciences
>
>
> On Thu, Oct 31, 2013 at 10:04 AM, Hongxu Chen <leftcopy.chx at gmail.com>wrote:
>
>> 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
>>>
>>>
>>
>> _______________________________________________
>> 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


More information about the klee-dev mailing list