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
