diff options
| -rw-r--r-- | lib/Module/KModule.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index e22b3d24..f3487baf 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -374,6 +374,16 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, #else runtimeFileName += ".bca"; #endif + + // Some SV-COMP benchmarks might provide their own implementation of + // __VERIFIER functions. Remove them + llvm::Function* existingVERIFIER_assert = module->getFunction("__VERIFIER_assert"); + if (existingVERIFIER_assert) { + existingVERIFIER_assert->deleteBody(); + klee_warning("Deleting existing implementation of %s", existingVERIFIER_assert->getName().data()); + } + + llvm::sys::path::append(LibPath, runtimeFileName.str()); module = linkWithLibrary(module, LibPath.str()); |