ExprEngine: Catch and handle exceptions in ExprData

lib/exprengine.cpp

@@ -1213,6 +1213,10 @@ bool ExprEngine::IntRange::isEqual(DataBase *dataBase, int value) const
     } catch (const z3::exception &exception) {
         std::cerr << "z3: " << exception << std::endl;
         return true;  // Safe option is to return true
+    } catch (const ExprData::BailoutValueException &) {
+        return true;  // Safe option is to return true
+    } catch (const ExprEngineException &) {
+        return true;  // Safe option is to return true
     }
 #else
     // The value may or may not be in range
@@ -1241,6 +1245,10 @@ bool ExprEngine::IntRange::isGreaterThan(DataBase *dataBase, int value) const
     } catch (const z3::exception &exception) {
         std::cerr << "z3: " << exception << std::endl;
         return true;  // Safe option is to return true
+    } catch (const ExprData::BailoutValueException &) {
+        return true;  // Safe option is to return true
+    } catch (const ExprEngineException &) {
+        return true;  // Safe option is to return true
     }
 #else
     // The value may or may not be in range
@@ -1269,6 +1277,10 @@ bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const
     } catch (const z3::exception &exception) {
         std::cerr << "z3: " << exception << std::endl;
         return true;  // Safe option is to return true
+    } catch (const ExprData::BailoutValueException &) {
+        return true;  // Safe option is to return true
+    } catch (const ExprEngineException &) {
+        return true;  // Safe option is to return true
     }
 #else
     // The value may or may not be in range
@@ -1298,6 +1310,10 @@ bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const
     } catch (const z3::exception &exception) {
         std::cerr << "z3: " << exception << std::endl;
         return true;  // Safe option is to return true
+    } catch (const ExprData::BailoutValueException &) {
+        return true;  // Safe option is to return true
+    } catch (const ExprEngineException &) {
+        return true;  // Safe option is to return true
     }
 #else
     // The value may or may not be in range
@@ -1328,6 +1344,10 @@ bool ExprEngine::FloatRange::isGreaterThan(DataBase *dataBase, int value) const
     } catch (const z3::exception &exception) {
         std::cerr << "z3: " << exception << std::endl;
         return true;  // Safe option is to return true
+    } catch (const ExprData::BailoutValueException &) {
+        return true;  // Safe option is to return true
+    } catch (const ExprEngineException &) {
+        return true;  // Safe option is to return true
     }
 #else
     // The value may or may not be in range
@@ -1358,6 +1378,10 @@ bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const
     } catch (const z3::exception &exception) {
         std::cerr << "z3: " << exception << std::endl;
         return true;  // Safe option is to return true
+    } catch (const ExprData::BailoutValueException &) {
+        return true;  // Safe option is to return true
+    } catch (const ExprEngineException &) {
+        return true;  // Safe option is to return true
     }
 #else
     // The value may or may not be in range
@@ -1369,6 +1393,7 @@ bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const
 bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value) const
 {
 #ifdef USE_Z3
+    try {
         ExprData exprData;
         z3::solver solver(exprData.context);
         z3::expr e = exprData.getExpr(this);
@@ -1376,6 +1401,14 @@ bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value)
         exprData.addAssertions(solver);
         solver.add(exprData.int_expr(e) == value);
         return solver.check() == z3::sat;
+    } catch (const z3::exception &exception) {
+        std::cerr << "z3:" << exception << std::endl;
+        return true;  // Safe option is to return true
+    } catch (const ExprData::BailoutValueException &) {
+        return true;  // Safe option is to return true
+    } catch (const ExprEngineException &) {
+        return true;  // Safe option is to return true
+    }
 #else
     (void)dataBase;
     (void)value;
@@ -1397,6 +1430,10 @@ bool ExprEngine::BinOpResult::isGreaterThan(ExprEngine::DataBase *dataBase, int
     } catch (const z3::exception &exception) {
         std::cerr << "z3:" << exception << std::endl;
         return true;  // Safe option is to return true
+    } catch (const ExprData::BailoutValueException &) {
+        return true;  // Safe option is to return true
+    } catch (const ExprEngineException &) {
+        return true;  // Safe option is to return true
     }
 #else
     (void)dataBase;
@@ -1419,6 +1456,10 @@ bool ExprEngine::BinOpResult::isLessThan(ExprEngine::DataBase *dataBase, int val
     } catch (const z3::exception &exception) {
         std::cerr << "z3:" << exception << std::endl;
         return true;  // Safe option is to return true
+    } catch (const ExprData::BailoutValueException &) {
+        return true;  // Safe option is to return true
+    } catch (const ExprEngineException &) {
+        return true;  // Safe option is to return true
     }
 #else
     (void)dataBase;
@@ -1441,6 +1482,10 @@ bool ExprEngine::BinOpResult::isTrue(ExprEngine::DataBase *dataBase) const
     } catch (const z3::exception &exception) {
         std::cerr << "z3:" << exception << std::endl;
         return true;  // Safe option is to return true
+    } catch (const ExprData::BailoutValueException &) {
+        return true;  // Safe option is to return true
+    } catch (const ExprEngineException &) {
+        return true;  // Safe option is to return true
     }
 #else
     (void)dataBase;
@@ -2688,7 +2733,7 @@ void ExprEngine::executeFunction(const Scope *functionScope, ErrorLogger *errorL
 
     try {
         execute(functionScope->bodyStart, functionScope->bodyEnd, data);
-    } catch (ExprEngineException &e) {
+    } catch (const ExprEngineException &e) {
         if (settings->debugBugHunting)
             report << "ExprEngineException tok.line:" << e.tok->linenr() << " what:" << e.what << "\n";
         trackExecution.setAbortLine(e.tok->linenr());