diff options
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/Internal/Module/KModule.h | 4 | ||||
-rw-r--r-- | include/klee/Internal/Support/ModuleUtil.h | 2 |
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 |