about summary refs log tree commit diff homepage
path: root/lib/Expr/Constraints.cpp
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2015-04-10 09:49:04 +0100
committerDan Liew <daniel.liew@imperial.ac.uk>2015-04-15 21:08:38 +0100
commit1a175c67402430c8e6a970d42660dcf3b23110aa (patch)
tree9001b1ac943bf1e45a24a0620e87bcafc1c08f24 /lib/Expr/Constraints.cpp
parent44cceb1eb7ab58b153a20d12c84d6b0b352e05da (diff)
downloadklee-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