From 4b477f8108a2a92012ff138725f6c6f26ccb23e5 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 29 Aug 2013 17:30:33 +0100 Subject: Implemented runtime check for overshift (controllable with --check-overshift command line argument). Overshift is where a Shl, AShr or LShr has a shift width greater than the bit width of the first operand. This is undefined behaviour in LLVM so we report this as an error. --- include/klee/Interpreter.h | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'include') diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h index e29db411..e93284d6 100644 --- a/include/klee/Interpreter.h +++ b/include/klee/Interpreter.h @@ -51,11 +51,13 @@ public: std::string LibraryDir; bool Optimize; bool CheckDivZero; + bool CheckOvershift; ModuleOptions(const std::string& _LibraryDir, - bool _Optimize, bool _CheckDivZero) + bool _Optimize, bool _CheckDivZero, + bool _CheckOvershift) : LibraryDir(_LibraryDir), Optimize(_Optimize), - CheckDivZero(_CheckDivZero) {} + CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift) {} }; enum LogType -- cgit 1.4.1