diff options
Diffstat (limited to 'lib/Core/Executor.h')
-rw-r--r-- | lib/Core/Executor.h | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index c9d715ad..27cefcc0 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -349,9 +349,17 @@ private: ExecutionState &state, ref<Expr> value); - ref<klee::ConstantExpr> evalConstantExpr(const llvm::ConstantExpr *ce); - - ref<klee::ConstantExpr> evalConstant(const llvm::Constant *c); + /// Evaluates an LLVM constant expression. The optional argument ki + /// is the instruction where this constant was encountered, or NULL + /// if not applicable/unavailable. + ref<klee::ConstantExpr> evalConstantExpr(const llvm::ConstantExpr *c, + const KInstruction *ki = NULL); + + /// Evaluates an LLVM constant. The optional argument ki is the + /// instruction where this constant was encountered, or NULL if + /// not applicable/unavailable. + ref<klee::ConstantExpr> evalConstant(const llvm::Constant *c, + const KInstruction *ki = NULL); /// Return a unique constant value for the given expression in the /// given state, if it has one (i.e. it provably only has a single |