Util changes needed for VSD #5375
Conversation
This don't show up on travis because the unit tests are currently not being built on Travis if USE_STD_STRING is set. Originally by Hannes Steffenhagen.
Codecov Report
@@ Coverage Diff @@
## develop #5375 +/- ##
========================================
Coverage 68.15% 68.15%
========================================
Files 1173 1173
Lines 97392 97392
========================================
Hits 66380 66380
Misses 31012 31012
Continue to review full report at Codecov.
|
hannes-steffenhagen-diffblue
left a comment
hannes-steffenhagen-diffblue
left a comment
There was a problem hiding this comment.
Other than the USE_STD_STRING change I don’t believe any of these changes should be merged as they already exist in some form or another on develop.
| #endif | ||
|
|
||
| #ifndef USE_STRING | ||
| #ifndef USE_STD_STRING |
There was a problem hiding this comment.
Side note: I’d really love if we could just get rid of USE_STD_STRING already. I’m not entirely convinced we keep it around for anything other than nostalgia at this point.
There was a problem hiding this comment.
I believe the only use case for it is / was debugging problems in the dtringt implementation. I am not sure how many issues it will find that have not already been found.
|
|
||
| symbol_table_baset::const_iteratort symbol_table_baset::end() const | ||
| { | ||
| return symbols.end(); |
There was a problem hiding this comment.
96bd3ae s/interate/iterate in the commit message.
Also this commit should be removed; Current develop already has begin/end for symbol_tablet.
|
|
||
| int counter = 0; | ||
| for(auto &entry : symbol_table) | ||
| SECTION("Non const iterator") |
There was a problem hiding this comment.
This commit (a9afb9a) can also be removed; symbol table iterators are tested in unit/util/symbol_table.cpp
There was a problem hiding this comment.
I can see a single class to begin() but no call to end. This also tests the correct dispatching when you have a symbol_tablet but the compile time type is symbol_table_baset
| return internal_symbols.end(); | ||
| } | ||
| using symbol_table_baset::begin; | ||
| using symbol_table_baset::end; |
There was a problem hiding this comment.
develop symbol_table_baset::begin/end are both purely virtual, so can not be used in this way.
There was a problem hiding this comment.
Discussed out of band: more consistent to have both const and non-const iterators be virtual and defined in the base class.
Patch originally by Chris Ryder.
Check that both const and non-const iterators work as expected.
|
@hannes-steffenhagen-diffblue I've made the begin/end virtual in the base class as agreed, ready for re-review |
thk123
requested review from
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
Since the const iterators can use the base class directly, these are not pure virtual - so derived classes can still provide an entirely different mechanism for iterating over the symbols - though this is not currently used.
martin-cs
left a comment
martin-cs
left a comment
There was a problem hiding this comment.
Am happy once @hannes-steffenhagen-diffblue 's comments have been addressed. I think that it will still work with the patch set.
hannes-steffenhagen-diffblue
left a comment
hannes-steffenhagen-diffblue
left a comment
There was a problem hiding this comment.
I still think it’s a bit inconsistent we have a pure virtual mut begin/end but an implementation for const begin/end. But I’d not block on that if that’s the only complaint.
|
@peterschrammel if you get a min, would you be able to provide the code owner review for this short PR? You reviewed this originally in #5205, Martin addressed your comments (this is a rebased version) |
4 participants
Rebased version of #5205, with two additions:
tests for the const iterators added to base symbol table
stop definitions in symbol_table hiding the implemention in symbol_table_baset (risks these defintions going out of sync)
Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
[na] The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
[na] My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.