Use numeric_cast<mp_integer> instead of deprecated to_integer(exprt) #3252
Conversation
tautschnig
requested review from
kroening,
martin-cs,
peterschrammel,
pkesseli and
smowton
as code owners
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: b4a93cb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/89879668
| return nil_exprt(); | ||
| } | ||
| const mp_integer vector_size = | ||
| numeric_cast_v<mp_integer>(vector_type.size()); | ||
|
|
There was a problem hiding this comment.
This is a change in behavior -- intended?
There was a problem hiding this comment.
Yes, my apologies for not noting that in the commit message (which I have now done). In several places we had already treated vectors having constant size as an invariant. This should add consistency.
| @@ -124,15 +120,10 @@ pointer_offset_bits(const typet &type, const namespacet &ns) | |||
| return {}; | |||
|
|
|||
| // get size | |||
| const exprt &size=to_vector_type(type).size(); | |||
| const mp_integer size = | |||
| numeric_cast_v<mp_integer>(to_vector_type(type).size()); | |||
|
|
|||
kroening
assigned tautschnig and unassigned smowton, kroening, peterschrammel and martin-cs
This reduces the number of warnings flagged, in particular in Visual-Studio builds. Also turn tests of the size of ID_vector types being constants into invariants as was already done in some places.
tautschnig
force-pushed
the
vs-no-to_integer
branch
from
b4a93cb to
638d91c
Compare
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 638d91c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90146796
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
|
Could someone with sufficient access please take a look as this may have broken TG? |
|
Looked like a post-build network-related failure, but restarted the build to make sure |
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 638d91c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90146796
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
|
Failure is real but also present on current test-gen/develop, so nothing to worry about here |
This reduces the number of warnings flagged, in particular in Visual-Studio
builds.