diff options
author | MartinNowack <martin.nowack@gmail.com> | 2016-07-09 09:36:36 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-07-09 09:36:36 +0200 |
commit | 48797d9846c38406f31e8a933a28eeef480a664d (patch) | |
tree | de7ce7fcce647ec650630a071b5d570d54a1cedf /lib/Solver/STPBuilder.h | |
parent | e87e5bd478d8dad5a7c164197b9e39da3873442d (diff) | |
parent | 61bb349e953d76bf3fd96a6f853f273f81ed13ff (diff) | |
download | klee-48797d9846c38406f31e8a933a28eeef480a664d.tar.gz |
Merge pull request #377 from MartinNowack/fix_div_constant
Fix generation of STP shift operations with variable shift
Diffstat (limited to 'lib/Solver/STPBuilder.h')
-rw-r--r-- | lib/Solver/STPBuilder.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h index 3b17ccf1..5be34029 100644 --- a/lib/Solver/STPBuilder.h +++ b/lib/Solver/STPBuilder.h @@ -93,6 +93,8 @@ private: ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift); ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift); ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle shift); + ExprHandle extractPartialShiftValue(ExprHandle shift, unsigned width, + unsigned &shiftBits); ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift, ExprHandle isSigned); |