Skip to content

Commit 8880cf9

Browse files
committed
fix JavaDoc and trailing array-comma.
1 parent 66de726 commit 8880cf9

File tree

2 files changed

+7
-1
lines changed

2 files changed

+7
-1
lines changed

src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -400,6 +400,7 @@ FloatingPointFormula multiply(
400400
* <li>sign=? (irrelevant for NaN)
401401
* <li>exponent=11...11 (all bits are 1)
402402
* <li>mantissa!=00...00 (mantissa is not all 0)
403+
* </ul>
403404
*/
404405
BooleanFormula isNaN(FloatingPointFormula number);
405406

@@ -412,6 +413,7 @@ FloatingPointFormula multiply(
412413
* <li>sign=? (0 for +Inf, 1 for -Inf)
413414
* <li>exponent=11...11 (all bits are 1)
414415
* <li>mantissa=00...00 (all bits are 0)
416+
* </ul>
415417
*/
416418
BooleanFormula isInfinity(FloatingPointFormula number);
417419

@@ -424,6 +426,7 @@ FloatingPointFormula multiply(
424426
* <li>sign=? (0 for +0, 1 for -0)
425427
* <li>exponent=00...00 (all bits are 0)
426428
* <li>mantissa=00...00 (all bits are 0)
429+
* </ul>
427430
*/
428431
BooleanFormula isZero(FloatingPointFormula number);
429432

@@ -436,6 +439,7 @@ FloatingPointFormula multiply(
436439
* <li>sign=? (0 for positive numbers, 1 for negative numbers)
437440
* <li>exponent!=00...00 and exponent!=11...11 (exponent is not all 0 or all 1)
438441
* <li>mantissa!=00...00 (mantissa is not all 0)
442+
* </ul>
439443
*/
440444
BooleanFormula isNormal(FloatingPointFormula number);
441445

@@ -448,6 +452,7 @@ FloatingPointFormula multiply(
448452
* <li>sign=? (0 for positive numbers, 1 for negative numbers)
449453
* <li>exponent=00...00 (exponent is all 0)
450454
* <li>mantissa!=00...00 (mantissa is not all 0)
455+
* </ul>
451456
*/
452457
BooleanFormula isSubnormal(FloatingPointFormula number);
453458

@@ -459,6 +464,7 @@ FloatingPointFormula multiply(
459464
* <ul>
460465
* <li>sign=1 (1 for negative numbers)
461466
* <li>number is not NaN, i.e., exponent=11...11 implies mantissa=00...00
467+
* </ul>
462468
*/
463469
BooleanFormula isNegative(FloatingPointFormula number);
464470
}

src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -364,7 +364,7 @@ public void specialValueFunctionsFrom32Bits() throws SolverException, Interrupte
364364
Float.intBitsToFloat(0x7fc0_0003),
365365
Float.intBitsToFloat(0x7fc1_2345),
366366
Float.intBitsToFloat(0x7fdf_5678),
367-
Float.intBitsToFloat(0x7ff0_0001)
367+
Float.intBitsToFloat(0x7ff0_0001),
368368
// there are some more combinations for NaN, too much for one small test.
369369
}) {
370370
assertThatFormula(fpmgr.isNaN(fpmgr.makeNumber(nanFromBits, singlePrecType)))

0 commit comments

Comments
 (0)