CombineDateAndTimeDuration: Recheck if still fallible anywhere #3023
Comments
ptomato
added a commit
that referenced
this issue
Dec 5, 2024
dateDuration and roundedTimeDuration cannot have opposite signs, so the operation can't throw. dateDuration must have the same sign as duration, because dayDelta either is 0 or also has the same sign as duration. roundedTimeDuration must have the same sign as duration or be 0, because either it is rounded from duration in step 10, or it is rounded from beyondDaySpan in step 12.c. beyondDaySpan also cannot have the opposite sign as duration if we go into the substeps of step 12. See: #3023
ptomato
added a commit
that referenced
this issue
Dec 5, 2024
dateDuration and remainder cannot have opposite signs, so the operation can't throw. dateDuration must either have the same sign as roundedTime or be 0, because days must either be 0 or be equal to roundedWholeDays, which is rounded from roundedTime. remainder must either have the same sign as roundedTime or be 0, because it is either equal to roundedTime or it has roundedWholeDays × HoursPerDay subtracted from it. roundedWholeDays × HoursPerDay cannot be greater than roundedTime because it is calculated from a truncating division of roundedTime in step 6. See: #3023
ptomato
added a commit
that referenced
this issue
Dec 5, 2024
…nfallible dateDifference and timeDuration cannot have opposite signs here, so the operation can't fail. This is ensured by the loop above, which backs up the intermediate date by one day until the signs match, which is asserted after the loop exits in step 11. See: #3023
ptomato
added a commit
that referenced
this issue
Dec 5, 2024
We now have proven that all of the call sites cannot provide a date duration and time duration with mixed signs. So we change the exception to an assertion. h/t Anba Closes: #3023
Ms2ger
pushed a commit
that referenced
this issue
Dec 5, 2024
dateDuration and roundedTimeDuration cannot have opposite signs, so the operation can't throw. dateDuration must have the same sign as duration, because dayDelta either is 0 or also has the same sign as duration. roundedTimeDuration must have the same sign as duration or be 0, because either it is rounded from duration in step 10, or it is rounded from beyondDaySpan in step 12.c. beyondDaySpan also cannot have the opposite sign as duration if we go into the substeps of step 12. See: #3023
Ms2ger
pushed a commit
that referenced
this issue
Dec 5, 2024
dateDuration and remainder cannot have opposite signs, so the operation can't throw. dateDuration must either have the same sign as roundedTime or be 0, because days must either be 0 or be equal to roundedWholeDays, which is rounded from roundedTime. remainder must either have the same sign as roundedTime or be 0, because it is either equal to roundedTime or it has roundedWholeDays × HoursPerDay subtracted from it. roundedWholeDays × HoursPerDay cannot be greater than roundedTime because it is calculated from a truncating division of roundedTime in step 6. See: #3023
Ms2ger
pushed a commit
that referenced
this issue
Dec 5, 2024
…nfallible dateDifference and timeDuration cannot have opposite signs here, so the operation can't fail. This is ensured by the loop above, which backs up the intermediate date by one day until the signs match, which is asserted after the loop exits in step 11. See: #3023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
All calls to
CombineDateAndTimeDurationare likely infallible with user-defined calendars and time zones gone.The text was updated successfully, but these errors were encountered: