From a53fade6e85394ef95dfaaa1c264149e85ea5451 Mon Sep 17 00:00:00 2001 From: Andrea Mattavelli Date: Wed, 22 Nov 2017 17:18:07 +0000 Subject: Added support for KLEE index-based array optimization --- lib/Core/Executor.h | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'lib/Core/Executor.h') diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index ec2d49c0..6a640905 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -16,6 +16,7 @@ #define KLEE_EXECUTOR_H #include "klee/ExecutionState.h" +#include "klee/ArrayExprOptimizer.h" #include "klee/Interpreter.h" #include "klee/Internal/Module/Cell.h" #include "klee/Internal/Module/KInstruction.h" @@ -228,6 +229,9 @@ private: // @brief buffer to store logs before flushing to file llvm::raw_string_ostream debugLogBuffer; + /// Optimizes expressions + ExprOptimizer optimizer; + llvm::Function* getTargetFunction(llvm::Value *calledVal, ExecutionState &state); -- cgit 1.4.1