From 50b9e95064a8a312c365fda57ed5729cd91706ba Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 17 Oct 2015 15:45:29 +0100 Subject: Some SV-COMP benchmarks provide an existing implementation of ``__VERIFIER_assert()`` which conflicts with ours. Remove their implementation if it is detected. --- lib/Module/KModule.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) 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()); -- cgit 1.4.1