From: Tim King <taking@cs.nyu.edu>
Date: Tue, 6 Feb 2018 03:07:17 +0000 (-0800)
Subject: Aborting on errors in StatisticsRegistry::unregisterStat() instead of throwing except... 
X-Git-Tag: cvc5-1.0.0~5330
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=96138688bcb3aebbaa86d49471427ee4068b5994;p=cvc5.git

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)
---

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;