summaryrefslogtreecommitdiff
path: root/src/expr/expr_manager_template.cpp
diff options
context:
space:
mode:
authorAndres Notzli <andres.noetzli@gmail.com>2017-03-31 14:27:05 -0700
committerAndres Nötzli <andres.noetzli@gmail.com>2017-05-12 08:50:36 -0700
commit31681c7ff2a1469f5efc325fc1b3a406e3a85949 (patch)
tree8a3a677f6520baf1429297d36c2e19518a7e545c /src/expr/expr_manager_template.cpp
parentb045d1d06f2d28957ccca6ed7d9e6458b4a96b79 (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/expr/expr_manager_template.cpp')
-rw-r--r--src/expr/expr_manager_template.cpp4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 82cabbd3e..cb8ad710f 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -1039,6 +1039,10 @@ SExpr ExprManager::getStatistic(const std::string& name) const throw() {
return d_nodeManager->getStatisticsRegistry()->getStatistic(name);
}
+void ExprManager::safeFlushStatistics(int fd) const {
+ d_nodeManager->getStatisticsRegistry()->safeFlushInformation(fd);
+}
+
namespace expr {
Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback