remove flag float-overflow-check (#3873)

Resolves #3620

Removing default 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.

Users can enable them using --cbmc-args as and when required.

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

Author: rajath-mk

kani-driver/src/call_cbmc.rs

@@ -233,7 +233,6 @@ impl KaniSession {
             args.push("--no-pointer-check".into());
         }
         if self.args.checks.overflow_on() {
-            args.push("--float-overflow-check".into());
             args.push("--nan-check".into());
 
             // TODO: Implement conversion checks as an optional check.

…s/ui/cbmc_checks/float-overflow/expected …ks/float-overflow/check_message.expectedtests/ui/cbmc_checks/float-overflow/expected renamed to tests/ui/cbmc_checks/float-overflow/check_message.expected tests/ui/cbmc_checks/float-overflow/expected renamed to tests/ui/cbmc_checks/float-overflow/check_message.expected

@@ -1,6 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
+// kani-flags: --enable-unstable --cbmc-args --float-overflow-check
 // Check we don't print temporary variables as part of CBMC messages.
 extern crate kani;
 

tests/ui/cbmc_checks/float-overflow/check_message.rs

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/ui/cbmc_checks/float-overflow/check_message_overflow.expected

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// This test verifies that Kani does not report floating-point overflow by default
+// for operations that result in +/-Infinity.
+extern crate kani;
+
+// Use the result so rustc doesn't optimize them away.
+fn dummy(result: f32) -> f32 {
+    result
+}
+
+#[kani::proof]
+fn main() {
+    let a = kani::any_where(|&x: &f32| x.is_finite());
+    let b = kani::any_where(|&x: &f32| x.is_finite());
+
+    dummy(a + b);
+    dummy(a - b);
+    dummy(a * b);
+    dummy(-a);
+}