projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ec834d5) | patch
Review of statistics code. Added lots of documentation, and fixed an issue (I think...
authorMorgan Deters <mdeters@gmail.com>
Mon, 28 Feb 2011 06:06:25 +0000 (06:06 +0000)
committerMorgan Deters <mdeters@gmail.com>
Mon, 28 Feb 2011 06:06:25 +0000 (06:06 +0000)
commit9e2a8db966072b5264e829ba1cd682eef7f58d62
tree89ffd0a61e71fc11ec5e27b01b7e7d539aa0f75etree
parentec834d513b8d390682a08f2ea2d159c3e35a4a2dcommit | diff
Review of statistics code.  Added lots of documentation, and fixed an issue (I think) that Tim found with TimerStat involving wild, sometimes negative, timer statistic values.  (It was due to improper initialization.)
src/util/stats.h diff | blob | history
test/unit/util/stats_black.h diff | blob | history