diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2017-07-07 15:21:12 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-07-07 15:21:12 -0700 |
commit | 4f9f046557b4de30c8f2ff654ea6e172e9cd912d (patch) | |
tree | ae08cd8d86cdfc86a8f8b67e596e74377685ccb7 /src/options/didyoumean.cpp | |
parent | 4fa50d388112bf30f9ebe219898cdc4dea76fd18 (diff) |
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.
Diffstat (limited to 'src/options/didyoumean.cpp')
0 files changed, 0 insertions, 0 deletions