Skip to content
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

Arbitrary implementations for floats trigger compiler warnings #3878

Open
carolynzech opened this issue Feb 7, 2025 · 1 comment
Open

Arbitrary implementations for floats trigger compiler warnings #3878

carolynzech opened this issue Feb 7, 2025 · 1 comment
Labels
[C] Bug This is a bug. Something isn't working.

Comments

@carolynzech
Copy link
Contributor

Upgrading our toolchain to 2/7/25, then running ./scripts/kani-regression.sh now produces this warning:

   Compiling kani_core v0.59.0 (/Users/cmzech/kani/library/kani_core)
warning: target feature `neon` must be enabled to ensure that the ABI of the current target can be implemented correctly                                                                                                                                                                
  |
  = note: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
  = note: for more information, see issue #116344 <https://github.com/rust-lang/rust/issues/116344>


warning: target feature `neon` must be enabled to ensure that the ABI of the current target can be implemented correctly                                                                                                                                                                
  |
  = note: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
  = note: for more information, see issue #116344 <https://github.com/rust-lang/rust/issues/116344>


   Compiling std v0.59.0 (/Users/cmzech/kani/library/std)
warning: target feature `neon` must be enabled to ensure that the ABI of the current target can be implemented correctly                                                                                                                                                                
  |
  = note: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
  = note: for more information, see issue #116344 <https://github.com/rust-lang/rust/issues/116344>

My hunch is that our trivial_arbitrary! implementations for floats are triggering this warning. The solution may just be to enable this target feature, but we need to dig more into the linked issue to ensure that's the right course of action.

@carolynzech carolynzech added the [C] Bug This is a bug. Something isn't working. label Feb 7, 2025
@tautschnig
Copy link
Member

I think we should just enable that target_feature to silence the warning: Kani does not care about the ABI for it uses its own interpretation of MIR and never deals with the actual object code generated for the target platform.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working.
Projects
None yet
Development

No branches or pull requests

2 participants