Skip to content

Commit 26c6889

Browse files
committed
Fix undefined behaviour in saturating addition.
Found by Frama-C/WP.
1 parent 8cbe63c commit 26c6889

File tree

1 file changed

+7
-6
lines changed

1 file changed

+7
-6
lines changed

include/fixed_point/inline/fixed_point.h

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -493,15 +493,16 @@ FXP_DECLARATION(frac f_clip (frac x, frac limit))
493493
*/
494494
FXP_DECLARATION(dfrac df_addsat(dfrac x1, dfrac x2))
495495
{
496-
dfrac_base result = x1.v + x2.v;
497496
dfrac r;
498497

499-
if (x1.v > 0 && x2.v > 0)
500-
r.v = ((result < x1.v) ? DFRAC_MAX_V : result);
501-
else if (x1.v < 0 && x2.v < 0)
502-
r.v = ((result > x1.v) ? DFRAC_MIN_V : result);
498+
/* The compiler does not seem to generate nice code for the
499+
* implementation below: */
500+
501+
if (x1.v >= 0)
502+
r.v = (x2.v > DFRAC_MAX_V - x1.v)? DFRAC_MAX_V : x1.v + x2.v;
503503
else
504-
r.v = result;
504+
r.v = (x2.v < DFRAC_MIN_V - x1.v) ? DFRAC_MIN_V : x1.v + x2.v;
505+
505506

506507
return r;
507508
}

0 commit comments

Comments
 (0)