From 96138688bcb3aebbaa86d49471427ee4068b5994 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Mon, 5 Feb 2018 19:07:17 -0800
Subject: Aborting on errors in StatisticsRegistry::unregisterStat() instead of
 throwing exceptions. This is called from destructors and therefore it is
 inappropraiate to throw exceptions. This solution is temporary until Assert()
 is deprecated in favor of an aborting version. (#1539)

---
 src/util/statistics_registry.cpp | 30 ++++++++++++++++++++++++++----
 1 file changed, 26 insertions(+), 4 deletions(-)

(limited to 'src/util/statistics_registry.cpp')

diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 4e2b06d53..38113c512 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -17,6 +17,9 @@
 
 #include "util/statistics_registry.h"
 
+#include <cstdlib>
+#include <iostream>
+
 #include "base/cvc4_assert.h"
 #include "lib/clock_gettime.h"
 #include "util/ostream_util.h"
@@ -164,9 +167,19 @@ void StatisticsRegistry::registerStat(Stat* s)
 void StatisticsRegistry::unregisterStat(Stat* s)
 {
 #ifdef CVC4_STATISTICS_ON
-  PrettyCheckArgument(d_stats.find(s) != d_stats.end(), s,
-                "Statistic `%s' was not registered with this registry.",
-                s->getName().c_str());
+  try
+  {
+    PrettyCheckArgument(d_stats.find(s) != d_stats.end(),
+                        s,
+                        "Statistic `%s' was not registered with this registry.",
+                        s->getName().c_str());
+  }
+  catch (Exception& e)
+  {
+    std::cerr << "Failure in StatisticsRegistry::unregisterStat():" << e.what()
+              << std::endl;
+    abort();
+  }
   d_stats.erase(s);
 #endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::unregisterStat_() */
@@ -199,7 +212,16 @@ void TimerStat::start() {
 
 void TimerStat::stop() {
   if(__CVC4_USE_STATISTICS) {
-    PrettyCheckArgument(d_running, *this, "timer not running");
+    try
+    {
+      PrettyCheckArgument(d_running, *this, "timer not running");
+    }
+    catch (Exception& e)
+    {
+      std::cerr << "Fatal failure in TimerStat::stop(): " << e.what()
+                << std::endl;
+      abort();
+    }
     ::timespec end;
     clock_gettime(CLOCK_MONOTONIC, &end);
     d_data += end - d_start;
-- 
cgit v1.2.3