diff options
| author | Martin Nowack <martin.nowack@gmail.com> | 2015-08-09 12:14:39 +0200 |
|---|---|---|
| committer | Martin Nowack <martin@se.inf.tu-dresden.de> | 2015-09-22 22:37:55 +0200 |
| commit | a801ac5dfef0533c3fc00a7dbfb630eccb0b8f30 (patch) | |
| tree | c591187a2af65ec9182d7d1bbf678daaccc37143 /lib | |
| parent | e8fded10ccdaea3d9d72d178506d6aebb799394e (diff) | |
| download | klee-a801ac5dfef0533c3fc00a7dbfb630eccb0b8f30.tar.gz | |
[STPBuilder] Generate SRrem expressions correctly
The '%' operater in C is not Gauss Modulo
but remainder operations.
Using a negative number as right operand
can result in a negative number.
Fix appropriate SRem building
Note: MetaSMTlib implementation doesn't have that bug.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index c2f23c0a..ddeb3c37 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -751,7 +751,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { #endif // XXX implement my fast path and test for proper handling of sign - return vc_sbvModExpr(vc, *width_out, left, right); + return vc_sbvRemExpr(vc, *width_out, left, right); } // Bitwise |