I disabled the assertion and I think it works, at least I got into the  
error related to unsupported inline assembly, no linker errors, which  
is good. I should be able to handle the inline asm error by either  
creating an equivalent function or using the hack suggested by Philip.

I linked native libraries before and I did not get the error so I am  
wondering why I got it now. As you mentioned, even though the linking  
worked, things didn't "really" work if the external call modified the  
memory or did allocations, etc so it is best to compile the bitcode  
versions instead. I'll see which libraries cause the error, perhaps  
this will explain more about the error.

Thanks for the help,
Cristi



On May 8, 2009, at 7:59 PM, Daniel Dunbar wrote:

> Some more details, Chris explained that this is to support the MSVC
> pragmas which allow code to specify which libraries are used. It is
> possible in this case that they are just slipping in by accident, I
> wonder if things work if you just disable the assertion?
>
> - Daniel
>
> On Fri, May 8, 2009 at 10:54 AM, Daniel Dunbar <daniel at zuster.org>  
> wrote:
>> On Fri, May 8, 2009 at 9:48 AM, Cristian Zamfir <cristian.zamfir at epfl.ch 
>> > wrote:
>>>
>>> Hi,
>>>
>>> I managed to compile Apache using the normal compile process, after
>>> hacking the libtool and Makefiles to compile and link the LLVM  
>>> bitcode.
>>
>> Nice!
>>
>>> However, when running with KLEE, I get the error "do not support
>>> dependent libraries".
>>> This is from Executor.cpp
>>>
>>> void Executor::initializeGlobals(ExecutionState &state) {
>>>   Module *m = kmodule->module;
>>>
>>> ....
>>>
>>>   demand(m->lib_begin() == m->lib_end(),
>>>          "XXX do not support dependent libraries");
>>>
>>> Is there any particular reason why these are not supported by  
>>> KLEE, or
>>> should I try to add support for that?
>>
>> I don't think I ever saw these in practice, but I believe these are
>> added as reference to external references to binary libraries. In
>> theory we could make them work using the external function calls, but
>> probably what you want to do instead is to get the build process to
>> link in bitcode versions of the required libraries, otherwise things
>> aren't "really" going to work.
>>
>>  - Daniel
>>
>>> Thanks,
>>> Cristi
>>> _______________________________________________
>>> klee-dev mailing list
>>> klee-dev at keeda.Stanford.EDU
>>> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>>>
>>

Reply via email to