about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorHoang M. Le <hle@informatik.uni-bremen.de>2016-06-28 13:18:52 +0200
committerHoang M. Le <hle@informatik.uni-bremen.de>2016-06-28 13:18:52 +0200
commit5b893715d020165f69062273741b7db99eb47624 (patch)
tree7346bcb2e04c40c2b95e7c608e743a890783de34 /lib/Solver
parent4f4b930df0306fb57eecd06eea182115f01b94e5 (diff)
downloadklee-5b893715d020165f69062273741b7db99eb47624.tar.gz
add assertions to check the pre-condition of bvVar*Shift that both operands have the same bv width
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/MetaSMTBuilder.h9
1 files changed, 9 insertions, 0 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index a166db5a..ad26f2ed 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -540,6 +540,9 @@ MetaSMTBuilder<SolverContext>::bvVarLeftShift(
     typename SolverContext::result_type expr,
     typename SolverContext::result_type shift, unsigned width) {
 
+  assert(_solver.get_bv_width(expr) == width);
+  assert(_solver.get_bv_width(shift) == width);
+
   typename SolverContext::result_type res = bvZero(width);
 
   // construct a big if-then-elif-elif-... with one case per possible shift
@@ -566,6 +569,9 @@ MetaSMTBuilder<SolverContext>::bvVarRightShift(
     typename SolverContext::result_type expr,
     typename SolverContext::result_type shift, unsigned width) {
 
+  assert(_solver.get_bv_width(expr) == width);
+  assert(_solver.get_bv_width(shift) == width);
+
   typename SolverContext::result_type res = bvZero(width);
 
   // construct a big if-then-elif-elif-... with one case per possible shift
@@ -593,6 +599,9 @@ MetaSMTBuilder<SolverContext>::bvVarArithRightShift(
     typename SolverContext::result_type expr,
     typename SolverContext::result_type shift, unsigned width) {
 
+  assert(_solver.get_bv_width(expr) == width);
+  assert(_solver.get_bv_width(shift) == width);
+
   // get the sign bit to fill with
   typename SolverContext::result_type signedBool =
       bvBoolExtract(expr, width - 1);