Remove floating-point check for +/-Inf

[feliperodri]

Kani included by default the flag --float-overflow-check, which reports overflow for arithmetic operations over floating-point numbers that result in +/-Inf. This doesn't panic in Rust and it shouldn't be consider a verification failure by default.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[zhassan-aws]

You might want to add --cbmc-args --float-overflow-check to tests/ui/cbmc_checks/float-overflow/check_message.rs.

[celinval]

I was about to ask for a test, but I see that our regression already has one, and that is failing now.

[tautschnig]

Here are the operations that CBMC currently creates checks for with --float-overflow-check:

1. Type casts (float-to-float or non-float to float).
2. Division (where an overflow may happen when dividing by a very small number).
3. Addition, subtraction, multiplication.

Looking at https://doc.rust-lang.org/std/primitive.f32.html, it seems the last two cases are well defined in Rust. For type casts, however, I don't know whether these have firmly defined behaviour?

Furthermore: should we enable users to insert such checks? It might not be undefined behaviour in Rust, but it might still be undesired behaviour?

[zhassan-aws]

Furthermore: should we enable users to insert such checks? It might not be undefined behaviour in Rust, but it might still be undesired behaviour?

Yes, I think we should add a switch (default off) to insert those checks. This is possible through passing --enable-unstable --cbmc-args --float-overflow-check, but adding a Kani-level flag would be cleaner.

[celinval]

You might want to add --cbmc-args --float-overflow-check to tests/ui/cbmc_checks/float-overflow/check_message.rs.

But also please also add tests that cover that overflow scenarios behavior is correct