diff options
author | Andres Notzli <andres.noetzli@gmail.com> | 2017-03-31 14:27:05 -0700 |
---|---|---|
committer | Andres Nötzli <andres.noetzli@gmail.com> | 2017-05-12 08:50:36 -0700 |
commit | 31681c7ff2a1469f5efc325fc1b3a406e3a85949 (patch) | |
tree | 8a3a677f6520baf1429297d36c2e19518a7e545c /src/util/statistics_registry.cpp | |
parent | b045d1d06f2d28957ccca6ed7d9e6458b4a96b79 (diff) |
Make signal handlers safer
As reported in bug 769, the signal handlers currently use unsafe
functions such as dynamic memory allocations and fprintf. This commit
fixes the issue by introducing functions for printing statistics in
signal handlers (functions with the `safe` prefix). It also avoids
copying statistics, which further avoids dynamic memory allocation. The
safe printing of statistics has some limitations (it does not support
SExprStats or printing CVC4::Result), which should not matter much in
practice. Printing statistics in a non-signal handler is not affected by
these changes as that uses a separate code path (the functions without
the `safe` prefix).
Additional changes:
- Remove ListStat as it is not used anywhere
- Add unit test for safe printing statistics
Diffstat (limited to 'src/util/statistics_registry.cpp')
-rw-r--r-- | src/util/statistics_registry.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index cb8e1ce90..4b0626048 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -182,6 +182,12 @@ void StatisticsRegistry::flushInformation(std::ostream &out) const { #endif /* CVC4_STATISTICS_ON */ } +void StatisticsRegistry::safeFlushInformation(int fd) const { +#ifdef CVC4_STATISTICS_ON + this->StatisticsBase::safeFlushInformation(fd); +#endif /* CVC4_STATISTICS_ON */ +} + void TimerStat::start() { if(__CVC4_USE_STATISTICS) { PrettyCheckArgument(!d_running, *this, "timer already running"); |