about summary refs log tree commit diff homepage
path: root/lib/Solver/STPBuilder.h
diff options
context:
space:
mode:
authorMartinNowack <martin.nowack@gmail.com>2016-07-09 09:36:36 +0200
committerGitHub <noreply@github.com>2016-07-09 09:36:36 +0200
commit48797d9846c38406f31e8a933a28eeef480a664d (patch)
treede7ce7fcce647ec650630a071b5d570d54a1cedf /lib/Solver/STPBuilder.h
parente87e5bd478d8dad5a7c164197b9e39da3873442d (diff)
parent61bb349e953d76bf3fd96a6f853f273f81ed13ff (diff)
downloadklee-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.h2
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);