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 /lib/Expr/Constraints.cpp | |
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 'lib/Expr/Constraints.cpp')
0 files changed, 0 insertions, 0 deletions