Disable Divide by 0 Checks for Floats

[cvick32]

Proposed change: Remove divide by 0 checks for floating point numbers, as they are well-defined in Rust? A similar change for +/- Inf was made in this PR.

Motivation: This change would eliminate false positives in verification failures.

[tautschnig]

Would you have a concrete example to use as test? With CBMC v6 (merged in #2995) we do not enable division-by-zero checks for floating point numbers by default anymore, so this one might as well quietly have been fixed by #2995.

[cvick32]

Kani previously found a counterexample on this function using this harness:

fn div_euclid_f64(lhs: f64, rhs: f64) -> f64 {
    let q = (lhs / rhs).trunc();
    if lhs % rhs < 0.0 {
        if rhs > 0.0 {
            q - 1.0
        } else {
            q + 1.0
        }
    } else {
        q
    }
}

#[kani::proof]
fn kani_harness_div_euclid_f64() {
  let lhs: f64 = kani::any();
  let rhs: f64 = kani::any();
  div_euclid_f64(lhs, rhs);
}

Kani's output summary from running cargo kani --harness kani_harness_div_euclid_f64:

SUMMARY:
 ** 4 of 62 failed
Failed Checks: division by zero
 File: "src/epoch/mod.rs", line 1186, in epoch::div_euclid_f64
Failed Checks: NaN on division
 File: "src/epoch/mod.rs", line 1186, in epoch::div_euclid_f64
Failed Checks: arithmetic overflow on floating-point division
 File: "src/epoch/mod.rs", line 1186, in epoch::div_euclid_f64
Failed Checks: division by zero
 File: "src/epoch/mod.rs", line 1187, in epoch::div_euclid_f64

[tautschnig]

Hmm, looks like we have a bug on the CBMC side in that floating-point division does not have checks enabled by default anymore, but floating-point remainder still has those.

[tautschnig]

I intend to fold the fix for this on the CBMC side into diffblue/cbmc#7885 as, until that work is completed, any floating-point remainder operations are very questionable.