From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 3 Mar 2011 18:35:17 +0000 (+0000)
Subject: fix for bug #244, "Segfault if file cannot be found and --stats is on"
X-Git-Tag: cvc5-1.0.0~8672
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3dbabefa475f034f07276dc0bb0d86f61f2239c3;p=cvc5.git

fix for bug #244, "Segfault if file cannot be found and --stats is on"
---

diff --git a/src/main/main.cpp b/src/main/main.cpp
index fcd322e99..563fa472e 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -181,7 +181,7 @@ int runCvc4(int argc, char* argv[]) {
   const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
 
   ReferenceStat< const char* > s_statFilename("filename", filename);
-  StatisticsRegistry::registerStat(&s_statFilename);
+  RegisterStatistic statFilenameReg(&s_statFilename);
 
   if(options.inputLanguage == language::input::LANG_AUTO) {
     if( inputFromStdin ) {
@@ -273,15 +273,12 @@ int runCvc4(int argc, char* argv[]) {
 #endif
 
   ReferenceStat< Result > s_statSatResult("sat/unsat", result);
-  StatisticsRegistry::registerStat(&s_statSatResult);
+  RegisterStatistic statSatResultReg(&s_statSatResult);
 
   if(options.statistics) {
     StatisticsRegistry::flushStatistics(*options.err);
   }
 
-  StatisticsRegistry::unregisterStat(&s_statSatResult);
-  StatisticsRegistry::unregisterStat(&s_statFilename);
-
   return returnValue;
 }
 
diff --git a/src/util/stats.h b/src/util/stats.h
index bf2e9d46c..978893a51 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -703,6 +703,26 @@ public:
     }                                                                   \
   } _StatField
 
+/**
+ * Resource-acquisition-is-initialization idiom for statistics
+ * registry.  Useful for stack-based statistics (like in the driver).
+ * Generally, for statistics kept in a member field of class, it's
+ * better to use the above KEEP_STATISTIC(), which does declaration of
+ * the member, construction of the statistic, and
+ * registration/unregistration.  This RAII class only does
+ * registration and unregistration.
+ */
+class RegisterStatistic {
+  Stat* d_stat;
+public:
+  RegisterStatistic(Stat* stat) : d_stat(stat) {
+    StatisticsRegistry::registerStat(d_stat);
+  }
+  ~RegisterStatistic() {
+    StatisticsRegistry::unregisterStat(d_stat);
+  }
+};/* class RegisterStatistic */
+
 #undef __CVC4_USE_STATISTICS
 
 }/* CVC4 namespace */