run VerifierPass after optimization and instrumentation

2 files changed, 4 insertions, 2 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