Add support for in_range

[Yenyun035]

Requested feature: in_range to check if a float is in the range of the targeting integer type, e.g.

kani::in_range(IntType, floatType, float) or something similar
Example: f32::to_int_unchecked contract
#[requires(self.is_finite() && kani::in_range(Int, Self, self))]
pub unsafe fn to_int_unchecked<Int>(self) -> Int where Self: FloatToInt<Int> {...}

Full Discussion:

Thank you for sharing this. Is it possible to have Kani support this? E.g. expose an in_range(float, floatType, IntType) API that we can directly call. We saw that the Kani internally has codegen_in_range_expr which we think useful.
Thank you! @zhassan-aws

Yes, I think it would be possible. This would likely need to be done through providing a trait and its implementation for different float types so that it can be used with the generic Int. Can you file a feature request in the Kani repo?

[celinval]

We're taking a look at it. Thanks

[Yenyun035]

Thanks!

@celinval Will the changes be merged into the feature/verify-rust-std branch?