6 files changed, 31 insertions, 31 deletions
diff --git a/include/klee/Internal/Module/KModule.h b/include/klee/Internal/Module/KModule.h
index 478e24d7..db50f06e 100644
--- a/include/klee/Internal/Module/KModule.h
+++ b/include/klee/Internal/Module/KModule.h
@@ -143,6 +143,10 @@ namespace klee {
 
     /// Return an id for the given constant, creating a new one if necessary.
     unsigned getConstantID(llvm::Constant *c, KInstruction* ki);
+
+    /// Run passes that check if module is valid LLVM IR and if invariants
+    /// expected by KLEE's Executor hold.
+    void checkModule();
   };
 } // End klee namespace
 
diff --git a/include/klee/Internal/Support/ModuleUtil.h b/include/klee/Internal/Support/ModuleUtil.h
index 8c819f40..6180225c 100644
--- a/include/klee/Internal/Support/ModuleUtil.h
+++ b/include/klee/Internal/Support/ModuleUtil.h
@@ -70,8 +70,6 @@ bool functionEscapes(const llvm::Function *f);
 bool loadFile(const std::string &libraryName, llvm::LLVMContext &context,
               std::vector<std::unique_ptr<llvm::Module>> &modules,
               std::string &errorMsg);
-
-void checkModule(llvm::Module *m);
 }
 
 #endif
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 3a5202ac..70561216 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -527,6 +527,7 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &modules,
   preservedFunctions.push_back("memmove");
 
   kmodule->optimiseAndPrepare(opts, preservedFunctions);
+  kmodule->checkModule();
 
   // 4.) Manifest the module
   kmodule->manifest(interpreterHandler, StatsTracker::useStatistics());
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 4817b6cc..3ce95a9e 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -41,6 +41,7 @@
 #include "llvm/Support/CallSite.h"
 #else
 #include "llvm/IR/CallSite.h"
+#include "llvm/IR/Verifier.h"
 #include "llvm/Linker/Linker.h"
 #endif
 
@@ -105,6 +106,12 @@ namespace {
   DebugPrintEscapingFunctions("debug-print-escaping-functions", 
                               cl::desc("Print functions whose address is taken (default=false)"),
 			      cl::cat(ModuleCat));
+
+  // Don't run VerifierPass when checking module
+  cl::opt<bool>
+  DontVerify("disable-verify",
+             cl::desc("Do not verify the module integrity (default=false)"),
+             cl::init(false), cl::cat(klee::ModuleCat));
 }
 
 /***/
@@ -282,19 +289,9 @@ void KModule::optimiseAndPrepare(
   case eSwitchTypeLLVM:  pm3.add(createLowerSwitchPass()); break;
   default: klee_error("invalid --switch-type");
   }
-  InstructionOperandTypeCheckPass *operandTypeCheckPass =
-      new InstructionOperandTypeCheckPass();
   pm3.add(new IntrinsicCleanerPass(*targetData));
   pm3.add(new PhiCleanerPass());
-  pm3.add(operandTypeCheckPass);
   pm3.run(*module);
-
-  // Enforce the operand type invariants that the Executor expects.  This
-  // implicitly depends on the "Scalarizer" pass to be run in order to succeed
-  // in the presence of vector instructions.
-  if (!operandTypeCheckPass->checkPassed()) {
-    klee_error("Unexpected instruction operand types detected");
-  }
 }
 
 void KModule::manifest(InterpreterHandler *ih, bool forceSourceOutput) {
@@ -360,6 +357,24 @@ void KModule::manifest(InterpreterHandler *ih, bool forceSourceOutput) {
   }
 }
 
+void KModule::checkModule() {
+  InstructionOperandTypeCheckPass *operandTypeCheckPass =
+      new InstructionOperandTypeCheckPass();
+
+  LegacyLLVMPassManagerTy pm;
+  if (!DontVerify)
+    pm.add(createVerifierPass());
+  pm.add(operandTypeCheckPass);
+  pm.run(*module);
+
+  // Enforce the operand type invariants that the Executor expects.  This
+  // implicitly depends on the "Scalarizer" pass to be run in order to succeed
+  // in the presence of vector instructions.
+  if (!operandTypeCheckPass->checkPassed()) {
+    klee_error("Unexpected instruction operand types detected");
+  }
+}
+
 KConstant* KModule::getKConstant(const Constant *c) {
   auto it = constantMap.find(c);
   if (it != constantMap.end())
diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp
index 399e5577..5c9aad1a 100644
--- a/lib/Module/ModuleUtil.cpp
+++ b/lib/Module/ModuleUtil.cpp
@@ -33,12 +33,10 @@
 #include "llvm/Support/SourceMgr.h"
 
 #if LLVM_VERSION_CODE < LLVM_VERSION(3, 5)
-#include "llvm/Analysis/Verifier.h"
 #include "llvm/Assembly/AssemblyAnnotationWriter.h"
 #include "llvm/Linker.h"
 #else
 #include "llvm/IR/AssemblyAnnotationWriter.h"
-#include "llvm/IR/Verifier.h"
 #include "llvm/Linker/Linker.h"
 #endif
 
@@ -599,9 +597,3 @@ std::unique_ptr<llvm::Module> module(ParseIR(Buffer.take(), Err, context));
   modules.push_back(std::move(module));
   return true;
 }
-
-void klee::checkModule(llvm::Module *m) {
-  LegacyLLVMPassManagerTy pm;
-  pm.add(createVerifierPass());
-  pm.run(*m);
-}
diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp
index d55fd0c3..22b9a16a 100644
--- a/lib/Module/Optimize.cpp
+++ b/lib/Module/Optimize.cpp
@@ -56,12 +56,6 @@
 
 using namespace llvm;
 
-// Don't verify at the end
-static cl::opt<bool>
-    DontVerify("disable-verify", cl::ReallyHidden,
-               cl::desc("Do not verify the module integrity (default=false)"),
-               cl::init(false), cl::cat(klee::ModuleCat));
-
 static cl::opt<bool>
     DisableInline("disable-inlining",
                   cl::desc("Do not run the inliner pass (default=false)"),
@@ -74,7 +68,7 @@ static cl::opt<bool> DisableInternalize(
 
 static cl::opt<bool> VerifyEach(
     "verify-each",
-    cl::desc("Verify intermediate results of all passes (default=false)"),
+    cl::desc("Verify intermediate results of all optimization passes (default=false)"),
     cl::init(false),
     cl::cat(klee::ModuleCat));
 
@@ -317,10 +311,6 @@ void Optimize(Module *M, llvm::ArrayRef<const char *> preservedFunctions) {
   addPass(Passes, createAggressiveDCEPass());
   addPass(Passes, createGlobalDCEPass());
 
-  // Make sure everything is still good.
-  if (!DontVerify)
-    Passes.add(createVerifierPass());
-
   // Run our queue of passes all at once now, efficiently.
   Passes.run(*M);
 }