about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorHristina Palikareva <h.palikareva@imperial.ac.uk>2014-12-03 13:43:44 +0000
committerHristina Palikareva <h.palikareva@imperial.ac.uk>2014-12-03 13:43:44 +0000
commitd0ca2fd3211f3bc0cfc582df978b6a82ea7ec390 (patch)
tree3919ab02e4dab4f9c0a7d7fbdb1bb6264859c549 /lib
parentd0f8c9ee4140689043ff5857f5283f6b0d22cbdc (diff)
downloadklee-d0ca2fd3211f3bc0cfc582df978b6a82ea7ec390.tar.gz
Handling overshift behaviour in MetaSMTBuilder
Diffstat (limited to 'lib')
-rw-r--r--lib/Solver/MetaSMTBuilder.h15
1 files changed, 15 insertions, 0 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index b5c99907..458c55ba 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -499,6 +499,11 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarLeftShif
                                                     bvLeftShift(expr, width, i, shiftBits),
                                                     res));
     }
+    
+    // If overshifting, shift to zero    
+    res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)),
+                                                res,
+                                                bvZero(width)));                                                
 
     return(res);
 }
@@ -521,6 +526,11 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarRightShi
                                                     res));
          // ToDo Reconsider widht to provide to bvRightShift
     }
+    
+    // If overshifting, shift to zero
+    res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)),
+                                                res,
+                                                bvZero(width)));                                                
 
     return(res);
 }
@@ -548,6 +558,11 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarArithRig
                                                     constructAShrByConstant(expr, width, i, signedBool, shiftBits),
                                                     res));
     }
+    
+    // If overshifting, shift to zero
+    res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)),
+                                                res,
+                                                bvZero(width)));      
 
     return(res);
 }