Avoid invoking copy constructor when safe printing (#184)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 7 Jul 2017 22:21:12 +0000 (15:21 -0700)
committerGitHub <noreply@github.com>
Fri, 7 Jul 2017 22:21:12 +0000 (15:21 -0700)
commit4f9f046557b4de30c8f2ff654ea6e172e9cd912d
treeae08cd8d86cdfc86a8f8b67e596e74377685ccb7
parent4fa50d388112bf30f9ebe219898cdc4dea76fd18
Avoid invoking copy constructor when safe printing (#184)

When CVC4 gets interrupted, we use async-signal safe printing functions
to print statistics. Unfortunately, the code for that was invoking copy
constructors, which is problematic due to memory allocation; for example
with statistics such as ReferenceStat<std::string>. This commit adds a
getDataRef() method for statistics that returns a const reference to the
object being printed such that the copy constructor is not called. Note:
modifying getData() was unfortunately not an option because in the case
of TimerStat, we can't return a reference to an object on the stack. We
could remove the const modifier on getData() and use d_data to store the
information but then we would have to remove it on
safeFlushInformation() and potentially other methods as well, which
seems like a worse solution.
src/util/statistics_registry.h