diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-04-10 09:49:04 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-04-15 21:08:38 +0100 |
| commit | 1a175c67402430c8e6a970d42660dcf3b23110aa (patch) | |
| tree | 9001b1ac943bf1e45a24a0620e87bcafc1c08f24 /include | |
| parent | 44cceb1eb7ab58b153a20d12c84d6b0b352e05da (diff) | |
| download | klee-1a175c67402430c8e6a970d42660dcf3b23110aa.tar.gz | |
Fix the handling of AShrExpr in ExprSMTLIBPrinter so that an overshift
always goes to zero (matches LLVM's APInt::ashr(...)). This is meant to partially address issue #218. There are a few problems with this commit * It is possible for AShrExpr to not be abbreviated because the scan methods will not see that we print the 0th child of the AShrExpr twice * The added test case should really be run through an SMT solver ( i.e. STP) but that requires infrastructure changes.
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/util/ExprSMTLIBPrinter.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h index 6b0d260a..e90a49f1 100644 --- a/include/klee/util/ExprSMTLIBPrinter.h +++ b/include/klee/util/ExprSMTLIBPrinter.h @@ -319,6 +319,7 @@ protected: void printNotEqualExpr(const ref<NeExpr> &e); void printSelectExpr(const ref<SelectExpr> &e, ExprSMTLIBPrinter::SMTLIB_SORT s); + void printAShrExpr(const ref<AShrExpr> &e); // For the set of operators that take sort "s" arguments void printSortArgsExpr(const ref<Expr> &e, |