-
Notifications
You must be signed in to change notification settings - Fork 284
use constructor for constant_exprt in convert_float_literal #3108
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
kroening
commented
Oct 6, 2018
- Each commit message has a non-empty body, explaining why the change was made.
- My contribution is formatted in line with CODING_STANDARD.md.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- 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).
- 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.
allredj
left a comment
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.
Passed Diffblue compatibility checks (cbmc commit: 853ebb2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87108003
allredj
left a comment
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.
Passed Diffblue compatibility checks (cbmc commit: 4813eba).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87108515
| } | ||
|
|
||
| ieee_floatt a(to_floatbv_type(result.type())); | ||
| ieee_floatt a(to_floatbv_type(type)); |
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.
How about we go one step further and fix up the return types of the float_type, double_type etc. to return a floatbv_typet? Then this would be ensured at compile-time rather than performing a run-time check?
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'd say yes to that, but would make it a separate PR.
4813eba to
bca1663
Compare
allredj
left a comment
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.
This PR failed Diffblue compatibility checks (cbmc commit: bca1663).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87182849
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).
allredj
left a comment
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.
This PR failed Diffblue compatibility checks (cbmc commit: bca1663).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87184017
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).