[klee-dev] Question about "-load" option

[Bin Lin]

Alright, I got it.

Thanks, Sean

On Thu, Sep 10, 2015 at 7:38 AM, Sean Bartell <sean at yotann.org> wrote:

> Bin Lin on 2015-09-09:
>
>> Both './klee -load=path-to-lib/libfoo.so main.bc' and LD_PRELOAD work for
>> this simple case. But for my situation, the "main()" function of C program
>> is wrapped in the dynamic library not in the program, in which case they
>> do
>> not work. It complains that " 'main' function not found in the module".
>> Does any one have ideas how to fix this?
>>
>
> Various parts of KLEE require 'main' to be in the program's bitcode file
> (main.bc). Your best option is to compile the library as LLVM bitcode, like
> the program, and link the library and program together somehow so you just
> have one bitcode file to give to KLEE.
>
>
> On Tue, Sep 8, 2015 at 2:48 PM, Sean Bartell <sean at yotann.org> wrote:
>>
>> Bin Lin on 2015-09-08:
>>>
>>> Hello Martin,
>>>
>>> Thank you!
>>>
>>> After I set the LD_RUN_PATH, what command should I use in my case? If I
>>> use the command './klee main.bc -load=path-to-lib/libfoo.so', I still get
>>> the same error. So how to load the dynamic library in my case?
>>>
>>> Try these, maybe one will work:
>>>
>>> LD_RUN_PATH=path-to-lib ./klee main.bc
>>>
>>> ./klee -load=path-to-lib/libfoo.so main.bc
>>>
>>> In addition, I do not understand why the '-load=path-to-lib/libfoo.so' is
>>> part of the arguments for my tested application not for KLEE. As far as I
>>> know, KLEE has the '-load' option.
>>>
>>> It's because of the order. If you use './klee main.bc -load=...', -load
>>> is
>>> passed through to the application. If you use './klee -load=... main.bc',
>>> -load is handled by KLEE.
>>>
>>>
-------------- next part --------------
HTML attachment scrubbed and removed