diff options
Diffstat (limited to 'include/klee/Internal/Module/KModule.h')
| -rw-r--r-- | include/klee/Internal/Module/KModule.h | 4 |
1 files changed, 4 insertions, 0 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 |