Add a Kani function that checks if the range of a float is valid for conversion to int

[zhassan-aws]

This introduces a new generic Kani function, kani::float::float_to_int_in_range, that can be used for checking if a floating-point value satisfies the range requirement of the to_int_unchecked methods, e.g https://doc.rust-lang.org/std/primitive.f32.html#method.to_int_unchecked and https://doc.rust-lang.org/std/primitive.f64.html#method.to_int_unchecked.

Resolves #3711

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