From: Morgan Deters 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 ? "" : 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 */