-
Notifications
You must be signed in to change notification settings - Fork 12.9k
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
float::round doesn't #3281
Comments
This is because c_double is a typedef for f64, and f64 and float are not type compatible (they used to be). Most of the float functions are just reexports of bindings to the C math libraries. The easiest fix is to write wrapper functions in core::float that cast to the right type (will be a noop). Beyond that it might be nice to think about how to get rid of the duplication between float/f32/f64. |
(sorry, clicked close by mistake) |
The specific code in question appears to have been fixed in d9c54f8, although I believe the preferred method is now I'm going to close this saying that it's been fixed, but if others feel |
fix typo in operator.rs
We believe the `--visualize` is much harder to use than concrete playback. In the rare cases where a trace might be relevant, users can still use CBMC trace. For most users, this will simplify installation since Kani will no longer depend on Python3. Note: As opposed to `--function` which was purely an internal feature, I believe we have mentioned `--visualize` to users before, so I think it's important to have a deprecation period. Related rust-lang#2832
Doesn't work as expected that is. Reasoning by analogy with the int modules I would expect that float::round(5.8) returns 6.0, but instead you get: error: mismatched types: expected
core::libc::types::os::arch::c95::c_double
but foundfloat
.Looking at the code I expect that more that just round has this problem.
The text was updated successfully, but these errors were encountered: