diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-03-03 18:35:17 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-03-03 18:35:17 +0000 |
commit | 3dbabefa475f034f07276dc0bb0d86f61f2239c3 (patch) | |
tree | af815c0324caafe10eeb21d2fba29ddac315a846 /src/util | |
parent | 43bf1fc1ba1770715fbe9fa15fa0be2cf6fb164a (diff) |
fix for bug #244, "Segfault if file cannot be found and --stats is on"
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/stats.h | 20 |
1 files changed, 20 insertions, 0 deletions
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 */ |