about summary refs log tree commit diff homepage
path: root/lib/Solver/STPBuilder.h
diff options
context:
space:
mode:
authorPeter Collingbourne <peter@pcc.me.uk>2012-03-26 21:52:43 +0000
committerPeter Collingbourne <peter@pcc.me.uk>2012-03-26 21:52:43 +0000
commit0e6c50c168a757201bdac4f0d442d248bd85de9c (patch)
treecab7c4fac50c4ff65785a1a7d606617dad169fb4 /lib/Solver/STPBuilder.h
parent911b3b2e1a9aa8d75d5fdb0465907082684d323a (diff)
downloadklee-0e6c50c168a757201bdac4f0d442d248bd85de9c.tar.gz
STPBuilder: fix bv{Zero,One,MinusOne} for the case where width>64
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@153474 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Solver/STPBuilder.h')
-rw-r--r--lib/Solver/STPBuilder.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index a4d6d0f8..7cc026bc 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -81,6 +81,8 @@ private:
   ExprHandle bvMinusOne(unsigned width);
   ExprHandle bvConst32(unsigned width, uint32_t value);
   ExprHandle bvConst64(unsigned width, uint64_t value);
+  ExprHandle bvZExtConst(unsigned width, uint64_t value);
+  ExprHandle bvSExtConst(unsigned width, uint64_t value);
 
   ExprHandle bvBoolExtract(ExprHandle expr, int bit);
   ExprHandle bvExtract(ExprHandle expr, unsigned top, unsigned bottom);