Conversation
src/goto-programs/interpreter.cpp
Outdated
There was a problem hiding this comment.
The return value here gets truncated to 0 when size_t is 32 bits wide.
tautschnig
left a comment
There was a problem hiding this comment.
Good catch; shouldn't we really be using mp_integer here?
|
There are actually more problems in this code:
I believe unbounded objects need to be handled properly at the call site of |
|
Yes, mp_integer exists exactly to avoid such problems on all architectures. |
|
I started looking at this, but it seems like changing that one function to return Maybe this would be better addressed by someone who is already familiar with this code. |
Looking at the commit subjects, without actually having done a |
|
Would it be worth merging this fix in now, and filing an issue to do a proper cleanup? At the moment, we don't have a working 32-bit build, and this patch at least resolves the immediate problem. |
|
From a plain technical point of view, lacking all the management insight: do the proper fix, even if it means rewriting several functions. If questions about the code arise, |
5e09d48 to
377fe4e
Compare
|
Thank you for the further work! I think all instances of |
6af34a9 to
661e095
Compare
|
I've tried to remove all instances of The guiding rationale has been to leave collection types unchanged. Conversions from |
|
I'll be taking a proper look in the morning - does this now require #1341 to build? (Which I'd be fine with, would just like to understand the CI failures.) |
|
Yes, this depends on having properly-converting operators on big-int and therefore requires #1341 |
|
#1341 blocked indefinitely, closing this. |
|
Joining my to-do list. |
Actually @smowton knows that code better |
|
I think that mp_integer is the right answer for the addresses; we do so everywhere else, and the cost isn't significantly higher than that of the 64-bit integers. |
|
Closing in favour of #1484, which seems to be doing almost the same. (I don't know why this one hasn't been amended rather than doing duplicate work.) |
The build is broken on 32-bit platforms, which is important because we should support OS X universal binaries. This patch fixes the build errors by explicitly using 64-bit integers rather than depending on
size_tto be 64 bits wide.