kata-containers/regorus
1
0
Fork 0
mirror of https://github.com/microsoft/regorus.git synced 2026-08-05 02:16:11 +00:00
Code Issues Packages Projects Releases Wiki Activity

Simplify float spec by avoiding partial_cmp_spec

Browse Source
This commit is contained in:
Jay Lorch
2026-03-19 11:33:30 -07:00
parent 2e454f2708
commit 9e18ded98e
1 changed files with 14 additions and 20 deletions
Download Patch File Download Diff File Expand all files Collapse all files

34
src/number.rs
View File

@@ -90,29 +90,23 @@ pub open spec fn float_to_small_int(value: f64) -> Option<int>
{
if !value.is_finite_spec() ||
!spec_f64_fract(value).eq_spec(&0.0f64) ||
spec_f64_abs(value).partial_cmp_spec(&9_007_199_254_740_992.0) == Some(Ordering::Greater) {
spec_f64_abs(value).is_gt(&9_007_199_254_740_992.0) {
None
}
else if value.is_ge(&0.0) {
if ieee_float_cast::<u64, f64>(ieee_float_cast::<f64, u64>(value)).eq_spec(&value) {
Some(ieee_float_cast::<f64, u64>(value) as int)
}
else {
None
}
}
else {
match value.partial_cmp_spec(&0.0) {
Some(Ordering::Greater) | Some(Ordering::Equal) =>
{
if ieee_float_cast::<u64, f64>(ieee_float_cast::<f64, u64>(value)).eq_spec(&value) {
Some(ieee_float_cast::<f64, u64>(value) as int)
}
else {
None
}
},
Some(Ordering::Less) | None =>
{
if ieee_float_cast::<i64, f64>(ieee_float_cast::<f64, i64>(value)).eq_spec(&value) {
Some(ieee_float_cast::<f64, i64>(value) as int)
}
else {
None
}
},
if ieee_float_cast::<i64, f64>(ieee_float_cast::<f64, i64>(value)).eq_spec(&value) {
Some(ieee_float_cast::<f64, i64>(value) as int)
}
else {
None
}
}
}