diff options
| author | Paul Marinescu <paul.marinescu@imperial.ac.uk> | 2013-11-03 19:07:20 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-02-14 17:37:30 +0000 |
| commit | 3160935d77c3fd6d24be7fddd5c570d6b3944c18 (patch) | |
| tree | 1f7afaea2a06744df65cdf55886fd7eb5ec0b2b9 /lib/Solver | |
| parent | d2f1684355e9a99545aa864e3eac81b259712a6f (diff) | |
| download | klee-3160935d77c3fd6d24be7fddd5c570d6b3944c18.tar.gz | |
Translate shl overshifts into 0
The other shift operators still need to be changed
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 90252656..6cb7dd38 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -223,6 +223,10 @@ ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle amount, unsign bvLeftShift(expr, i, shiftBits), res); } + res = vc_iteExpr(vc, + vc_bvLtExpr(vc, amount, bvConst32(32, width)), + res, + bvZero(width)); return res; } |