Hi, As I found out klee doesn't execute extern functions (functions declared in other compilation units) symbolically even if the --allow-external-sym-calls argument is given. Extern functions always get executed with ExecutionEngineState::runFunction which is in llvm code - which knows nothing of symbolic execution.
I was wondering this seems to be a very useful feature to have, and for a noob like me, seems easy to implement (if you have the bitcode of the extern function of course). Or is there a reason this has not been implemented for so long? Thanks, Jamm
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
