Thanks Paul! Actually, I tried KLEE and found the shared libraries can be linked well with approach. And the shared libraries in native form can be linked correctly with the following two strategies:
1. llvm-ld 2. sys::DynamicLibrary::LoadLibraryPermanently However, the static libraries can not be understood by KLEE through those strategies, do you have special idea about static libraries? Thanks Peng On 8/12/2012 4:35 PM, Paul Marinescu wrote: > Hello Peng, > I don't know what you're referring to by 'native bitcode' but > a) If you have a library in bitcode format, link it with the main executable > before passing it to KLEE > b) If you have a library in native format, pass --load=</path/to/library> to > KLEE (usual restrictions involving externals apply). > > Best, > Paul > > On 12 Aug 2012, at 23:38, Peng Li wrote: > >> Hi There >> >> I think it is common that source code includes the external invocations >> which require the external libraries. >> >> If the user does not have the source code of external libraries, but >> only ones compiled into native bitcode, >> in this case, how does KLEE work? I tried the simple case, looks like >> klee is not able to resolve the external >> functions correctly. >> >> Thanks >> Peng >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
