verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.08k stars 58 forks source link

Suppress unused variable warning for print_u64 in no_std #1133

Closed ouuan closed 1 month ago

utaal commented 1 month ago

Is it correct that the unused variable warning only appears if the println! macro is called in a non-std build?

One moment, I'm confused about what the issue is.

ouuan commented 1 month ago

In std build, the println! macro in std is used, so the parameter i is used there.

In no_std build, the println! macro defined here is used. The old one was empty so the parameter i was not used.

ouuan commented 1 month ago

Now I added let _ = for each expression used in the println! macro instead of adding attributes to the print_u64 function. In this way, if we have more functions that use println! in the future, we won't need to add #[allow(unused_variables)] for all of them.

utaal commented 1 month ago

I prefer we address this directly on print_u64. I pushed a commit to that effect: https://github.com/verus-lang/verus/commit/4132e1f192a31a9a680c5e6c3f2f2814d2267e0b

The proposed change to the macro in this PR I think assumes a certain way of calling println!, I prefer if we kept it as simple as possible.

Thanks for bringing this up, but I'll close this in favor of the commit I pushed, which should address the warning in the cfg(not(feature = "std")) build.