string_constantt typing #7965
string_constantt typing #7965
Conversation
kroening
commented
Oct 18, 2023
kroening
commented
- 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.
- n/a 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).
- n/a My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.
kroening
force-pushed
the
string-constant-types
branch
from
344fa2b to
758913c
Compare
Codecov ReportAttention:
Additional details and impacted files@@ Coverage Diff @@
## develop #7965 +/- ##
===========================================
- Coverage 78.87% 78.74% -0.13%
===========================================
Files 1701 1701
Lines 196386 196396 +10
===========================================
- Hits 154893 154647 -246
- Misses 41493 41749 +256
☔ View full report in Codecov by Sentry. |
src/util/string_constant.h
Outdated
| @@ -11,19 +11,37 @@ Author: Daniel Kroening, [email protected] | |||
|
|
|||
| #include "std_expr.h" | |||
|
|
|||
| class string_constantt : public nullary_exprt | |||
| class string_constantt : public constant_exprt | |||
There was a problem hiding this comment.
This is weird: we have a constant_exprt per the C++ type system, but it won’t have ID_constant in the irept type hierarchy. I’m not yet convinced this is the right thing to do.
There was a problem hiding this comment.
ok, going back to nullary_exprt
| { | ||
| public: | ||
| explicit string_constantt(const irep_idt &value); |
There was a problem hiding this comment.
I know that the value identifier isn't required here, but I'd prefer that we either keep it or explicitly document what this parameter is used for in the header file.
1) The string_constantt class is expected to maintain the invariant that its type is an array type. This is now made explicit by changing the type of string_constantt::type(). 2) A convenience helper to obtain the character type of the string is added.
This adds C++ style (as opposed to Java style) accessors to string_constantt.
kroening
force-pushed
the
string-constant-types
branch
from
758913c to
cc0d810
Compare
| @@ -12,25 +12,40 @@ Author: Daniel Kroening, [email protected] | |||
| #include "c_types.h" | |||
| #include "std_expr.h" | |||
|
|
|||
| static array_typet make_type(const irep_idt &value) | |||
| { | |||
| exprt size_expr = from_integer(value.size() + 1, c_index_type()); | |||
There was a problem hiding this comment.
I am quite confused by the Codecov warnings here: isn't this code path necessarily hit if we ever construct a string_constantt for there is just one constructor? That would suggest that none of our tests ever result in constructing a string_constantt?!
There was a problem hiding this comment.
Seems more likely that the coverage job isn't working correctly. There are a couple of things I can think of to try -
- Removing
-Dparallel_tests=2. Concurrent accesses to the coverage data files could be clobbering each other. - There is a hint that building with
-fprofile-arcsmay be needed here - https://discourse.cmake.org/t/guideline-for-code-coverage/167
