-
Notifications
You must be signed in to change notification settings - Fork 274
change type of numerical architecture symbols to integer #7215
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Conversation
Sure, we could do this, but it will require updating the goto binary version (and re-compiling binaries that are part of regression tests). |
No need -- this is compatible both ways (old versions can read new binaries, and old binaries can be read by new versions). |
Linking won't work for the architecture symbols now have conflicting types. We might gloss over that and would then just need to recompile the goto binaries in our regression tests. Further fixes that seem to be necessary:
--- a/src/util/interval.cpp
+++ b/src/util/interval.cpp
@@ -1094,7 +1094,7 @@ bool constant_interval_exprt::is_numeric(
bool constant_interval_exprt::is_int(const typet &type)
{
- return (is_signed(type) || is_unsigned(type));
+ return is_signed(type) || is_unsigned(type) || type.id() == ID_integer;
}
bool constant_interval_exprt::is_float(const typet &src)
|
d507f87
to
4ad807a
Compare
@@ -113,7 +113,8 @@ static std::string architecture_string(const std::string &value, const char *s) | |||
template <typename T> | |||
static std::string architecture_string(T value, const char *s) | |||
{ | |||
return std::string("const int " CPROVER_PREFIX "architecture_") + | |||
return std::string("const __CPROVER_integer " CPROVER_PREFIX |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this should also use CPROVER_PREFIX
in the first case of "__CPROVER_" (actually the failing cpplint job says the same :-) )
4ad807a
to
be35902
Compare
1a42130
to
c50d2e1
Compare
This extends the C++ front-end to recognize __CPROVER_integer and __CPROVER_rational, in the same way as done in the C frontend.
This enables using unbounded integers instead of bitvectors for architecture-independent constants.
c50d2e1
to
a4ffe59
Compare
Codecov ReportBase: 77.92% // Head: 77.97% // Increases project coverage by
Additional details and impacted files@@ Coverage Diff @@
## develop #7215 +/- ##
===========================================
+ Coverage 77.92% 77.97% +0.04%
===========================================
Files 1616 1616
Lines 186777 186837 +60
===========================================
+ Hits 145550 145683 +133
+ Misses 41227 41154 -73
Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here. ☔ View full report at Codecov. |
Following a suggestion in ##5878, this changes the type of the numerical _CPROVER_architecture symbols from
int
(which is itself architecture-dependent) to integer (which does not depend on the architecture).Closes #5878