diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2013-11-07 10:55:12 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-02-14 17:52:10 +0000 |
| commit | 458eb00a569445b82decf5687cb4716217ad1ad6 (patch) | |
| tree | 9e892ee8609b31201a912b2c021483b5d853db86 /lib/Solver | |
| parent | 3160935d77c3fd6d24be7fddd5c570d6b3944c18 (diff) | |
| download | klee-458eb00a569445b82decf5687cb4716217ad1ad6.tar.gz | |
Added a test case for testing overshift behaviour of Shl and fixed
a bug in the previous commit where 32-bit width was assumed.
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 6cb7dd38..cdc30f85 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -223,8 +223,10 @@ ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle amount, unsign bvLeftShift(expr, i, shiftBits), res); } + + // If overshifting, shift to zero res = vc_iteExpr(vc, - vc_bvLtExpr(vc, amount, bvConst32(32, width)), + vc_bvLtExpr(vc, amount, bvConst32(width, width)), res, bvZero(width)); return res; |