From 1a175c67402430c8e6a970d42660dcf3b23110aa Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 10 Apr 2015 09:49:04 +0100 Subject: 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. --- include/klee/util/ExprSMTLIBPrinter.h | 1 + 1 file changed, 1 insertion(+) (limited to 'include') 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 &e); void printSelectExpr(const ref &e, ExprSMTLIBPrinter::SMTLIB_SORT s); + void printAShrExpr(const ref &e); // For the set of operators that take sort "s" arguments void printSortArgsExpr(const ref &e, -- cgit 1.4.1