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

[Sean Bartell]

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