Commons Math is a library of lightweight, self-contained mathematics and statistics components addressing the most common problems not available in the Java programming language or Commons Lang.
http://commons.apache.org/proper/commons-math/
Issue 835: https://issues.apache.org/jira/browse/MATH-835
Problem:
The percentageValue() method of the Fraction class works by first multiplying the Fraction by 100, then converting the Fraction to a double. This causes overflows when the numerator is greater than Integer.MAX_VALUE/100, even when the value of the fraction is far below this value.

Test case:


Expected:

percentage  = 100 * ((double) numer) / denom

percentage < 0 (due to overflow)

Add this assertion into org.apache.commons.math3.fraction.Fraction.percentageValue() at line 599:

assert numerator >= 0 ? result >= 0 : true;

org.apache.commons.math3.fraction.Fraction:599 (debugLine: 603)
suspiciousness: 0.96
Logic: result >= -0.0
Accuracy: 1


org.apache.commons.math3.fraction.Fraction:600 (debugLine: 604)
suspiciousness: 0.96
Logic: result >= -0.0
Accuracy: 1


org.apache.commons.math3.fraction.Fraction:555 (debugLine: 558)
suspiciousness: 0.92
Logic: fraction.numerator >= -0.0
Accuracy: 1


org.apache.commons.math3.fraction.Fraction:557 (debugLine: 560)
suspiciousness: 0.92
Logic: fraction.numerator >= -0.0
Accuracy: 1

fraction.numerator >= -0.0 (org.apache.commons.math3.fraction.Fraction:557)

This bug is caused by an integer overflow which caused numerator to be negative internally.

We feed the passed test cases from Ziyuan to Daikon. After a while, Daikon creates a lot of invariants (file). We check the invariants inside the functions multiply() and percentageValue(). However, no useful invariants has been found.