Skip to content

Commit 84d84c6

Browse files
kfriedbergerkfriedberger
committed
fix compiler warnings and cleanup some exception handling in tests.
1 parent 659998e commit 84d84c6

File tree

8 files changed

+37
-66
lines changed

8 files changed

+37
-66
lines changed

‎src/org/sosy_lab/java_smt/example/FormulaClassifier.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -294,7 +294,7 @@ public Integer visitFunction(
294294
nonLinearArithmetic = true;
295295
return allArgLevel + 1;
296296
}
297-
// $FALL-THROUGH$
297+
// $FALL-THROUGH$
298298
default:
299299
if (pFunctionDeclaration.getType().isBooleanType()) {
300300
if (EnumSet.of(

‎src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java‎

Lines changed: 14 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@
1010

1111
import static com.google.common.truth.Truth.assertThat;
1212
import static com.google.common.truth.Truth.assertWithMessage;
13-
import static com.google.common.truth.Truth.assert_;
1413
import static com.google.common.truth.TruthJUnit.assume;
1514
import static org.junit.Assert.assertThrows;
1615
import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
@@ -534,11 +533,9 @@ public void bvInRange() throws SolverException, InterruptedException {
534533
@SuppressWarnings("CheckReturnValue")
535534
public void bvOutOfRange() {
536535
for (int[] sizeAndValue : new int[][] {{4, 32}, {4, -9}, {8, 300}, {8, -160}}) {
537-
try {
538-
bvmgr.makeBitvector(sizeAndValue[0], sizeAndValue[1]);
539-
assert_().fail();
540-
} catch (IllegalArgumentException expected) {
541-
}
536+
assertThrows(
537+
IllegalArgumentException.class,
538+
() -> bvmgr.makeBitvector(sizeAndValue[0], sizeAndValue[1]));
542539
}
543540

544541
for (int size : new int[] {4, 6, 8, 10, 16, 32}) {
@@ -547,16 +544,9 @@ public void bvOutOfRange() {
547544
bvmgr.makeBitvector(size, -(1L << (size - 1)));
548545

549546
// forbitten values
550-
try {
551-
bvmgr.makeBitvector(size, 1L << size);
552-
assert_().fail();
553-
} catch (IllegalArgumentException expected) {
554-
}
555-
try {
556-
bvmgr.makeBitvector(size, -(1L << (size - 1)) - 1);
557-
assert_().fail();
558-
} catch (IllegalArgumentException expected) {
559-
}
547+
assertThrows(IllegalArgumentException.class, () -> bvmgr.makeBitvector(size, 1L << size));
548+
assertThrows(
549+
IllegalArgumentException.class, () -> bvmgr.makeBitvector(size, -(1L << (size - 1)) - 1));
560550
}
561551

562552
for (int size : new int[] {36, 40, 64, 65, 100, 128, 200, 250, 1000, 10000}) {
@@ -572,17 +562,14 @@ public void bvOutOfRange() {
572562
bvmgr.makeBitvector(size, BigInteger.ONE.shiftLeft(size - 1).negate());
573563

574564
// forbitten values
575-
try {
576-
bvmgr.makeBitvector(size, BigInteger.ONE.shiftLeft(size));
577-
assert_().fail();
578-
} catch (IllegalArgumentException expected) {
579-
}
580-
try {
581-
bvmgr.makeBitvector(
582-
size, BigInteger.ONE.shiftLeft(size - 1).negate().subtract(BigInteger.ONE));
583-
assert_().fail();
584-
} catch (IllegalArgumentException expected) {
585-
}
565+
assertThrows(
566+
IllegalArgumentException.class,
567+
() -> bvmgr.makeBitvector(size, BigInteger.ONE.shiftLeft(size)));
568+
assertThrows(
569+
IllegalArgumentException.class,
570+
() ->
571+
bvmgr.makeBitvector(
572+
size, BigInteger.ONE.shiftLeft(size - 1).negate().subtract(BigInteger.ONE)));
586573
}
587574
}
588575

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

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,8 @@
1010

1111
import static com.google.common.truth.Truth.assertThat;
1212
import static com.google.common.truth.Truth.assertWithMessage;
13-
import static com.google.common.truth.Truth.assert_;
1413
import static com.google.common.truth.TruthJUnit.assume;
14+
import static org.junit.Assert.assertThrows;
1515
import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
1616

1717
import com.google.common.collect.ImmutableList;
@@ -1024,11 +1024,9 @@ public void fpInterpolation() throws SolverException, InterruptedException {
10241024
}
10251025
}
10261026

1027-
@SuppressWarnings("CheckReturnValue")
1028-
@Test(expected = Exception.class)
1027+
@Test
10291028
public void failOnInvalidString() {
1030-
fpmgr.makeNumber("a", singlePrecType);
1031-
assert_().fail();
1029+
assertThrows(Exception.class, () -> fpmgr.makeNumber("a", singlePrecType));
10321030
}
10331031

10341032
@Test

‎src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java‎

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@
1111
import static com.google.common.collect.Iterables.getLast;
1212
import static com.google.common.truth.Truth.assertThat;
1313
import static com.google.common.truth.Truth.assertWithMessage;
14-
import static com.google.common.truth.Truth.assert_;
1514
import static com.google.common.truth.TruthJUnit.assume;
1615
import static org.junit.Assert.assertThrows;
1716
import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
@@ -362,8 +361,7 @@ public <T> void sequentialInterpolationIsNotRepeatedIndividualInterpolation()
362361
}
363362
}
364363

365-
@Test(expected = IllegalArgumentException.class)
366-
@SuppressWarnings("CheckReturnValue")
364+
@Test
367365
public <T> void sequentialInterpolationWithoutPartition()
368366
throws SolverException, InterruptedException {
369367
requireIntegers();
@@ -373,8 +371,8 @@ public <T> void sequentialInterpolationWithoutPartition()
373371
assertThat(stack).isUnsatisfiable();
374372

375373
// empty list of partition
376-
stack.getSeqInterpolants(ImmutableList.of());
377-
assert_().fail();
374+
assertThrows(
375+
IllegalArgumentException.class, () -> stack.getSeqInterpolants(ImmutableList.of()));
378376
}
379377

380378
@Test
@@ -973,8 +971,7 @@ public <T> void treeInterpolationMalFormed6() throws SolverException, Interrupte
973971
stack.getTreeInterpolants0(ImmutableList.of(TA, TA, TA), new int[] {0, 2, 0});
974972
}
975973

976-
@Test(expected = IllegalArgumentException.class)
977-
@SuppressWarnings("CheckReturnValue")
974+
@Test
978975
public <T> void treeInterpolationWithoutPartition() throws SolverException, InterruptedException {
979976
requireTreeItp();
980977

@@ -984,8 +981,9 @@ public <T> void treeInterpolationWithoutPartition() throws SolverException, Inte
984981
assertThat(stack).isUnsatisfiable();
985982

986983
// empty list of partition
987-
stack.getTreeInterpolants(ImmutableList.of(), new int[] {});
988-
assert_().fail();
984+
assertThrows(
985+
IllegalArgumentException.class,
986+
() -> stack.getTreeInterpolants(ImmutableList.of(), new int[] {}));
989987
}
990988

991989
@Test

‎src/org/sosy_lab/java_smt/test/ModelTest.java‎

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
import static com.google.common.truth.Truth.assertWithMessage;
1313
import static com.google.common.truth.Truth.assert_;
1414
import static com.google.common.truth.TruthJUnit.assume;
15+
import static org.junit.Assert.assertThrows;
1516
import static org.sosy_lab.java_smt.api.FormulaType.IntegerType;
1617
import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
1718

@@ -2306,22 +2307,19 @@ public void modelAfterSolverCloseTest() throws SolverException, InterruptedExcep
23062307
}
23072308
}
23082309

2309-
@SuppressWarnings("resource")
2310-
@Test(expected = IllegalStateException.class)
2310+
@Test
23112311
public void testGenerateModelsOption() throws SolverException, InterruptedException {
23122312
try (ProverEnvironment prover = context.newProverEnvironment()) { // no option
23132313
assertThat(prover).isSatisfiable();
2314-
prover.getModel();
2315-
assert_().fail();
2314+
assertThrows(IllegalArgumentException.class, () -> prover.getModel());
23162315
}
23172316
}
23182317

2319-
@Test(expected = IllegalStateException.class)
2318+
@Test
23202319
public void testGenerateModelsOption2() throws SolverException, InterruptedException {
23212320
try (ProverEnvironment prover = context.newProverEnvironment()) { // no option
23222321
assertThat(prover).isSatisfiable();
2323-
prover.getModelAssignments();
2324-
assert_().fail();
2322+
assertThrows(IllegalArgumentException.class, () -> prover.getModelAssignments());
23252323
}
23262324
}
23272325

‎src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java‎

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@
99
package org.sosy_lab.java_smt.test;
1010

1111
import static com.google.common.truth.Truth.assertThat;
12-
import static com.google.common.truth.Truth.assert_;
1312
import static com.google.common.truth.TruthJUnit.assume;
13+
import static org.junit.Assert.assertThrows;
1414

1515
import com.google.common.collect.Iterables;
1616
import java.util.HashSet;
@@ -139,10 +139,8 @@ protected Boolean visitDefault(Formula pF) {
139139
}
140140
}
141141

142-
@SuppressWarnings("CheckReturnValue")
143-
@Test(expected = Exception.class)
142+
@Test
144143
public void failOnInvalidString() {
145-
rmgr.makeNumber("a");
146-
assert_().fail();
144+
assertThrows(Exception.class, () -> rmgr.makeNumber("a"));
147145
}
148146
}

‎src/org/sosy_lab/java_smt/test/SolverTacticsTest.java‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
package org.sosy_lab.java_smt.test;
1010

1111
import static com.google.common.truth.Truth.assertThat;
12-
import static com.google.common.truth.Truth.assert_;
12+
import static org.junit.Assert.assertThrows;
1313
import static org.sosy_lab.java_smt.api.FormulaType.BooleanType;
1414
import static org.sosy_lab.java_smt.api.FormulaType.IntegerType;
1515

@@ -216,11 +216,7 @@ public void ufEliminationNesteQuantifierTest() throws InterruptedException {
216216
qmgr.exists(
217217
ImmutableList.of(variable1, variable2, variable3, variable4), bmgr.equivalence(f1, f2));
218218

219-
try {
220-
mgr.applyTactic(f, Tactic.ACKERMANNIZATION);
221-
assert_().fail();
222-
} catch (IllegalArgumentException expected) {
223-
}
219+
assertThrows(IllegalArgumentException.class, () -> mgr.applyTactic(f, Tactic.ACKERMANNIZATION));
224220
}
225221

226222
private static class CNFChecker implements BooleanFormulaVisitor<Void> {

‎src/org/sosy_lab/java_smt/test/UfEliminationTest.java‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@
88

99
package org.sosy_lab.java_smt.test;
1010

11-
import static com.google.common.truth.Truth.assert_;
1211
import static com.google.common.truth.TruthJUnit.assume;
12+
import static org.junit.Assert.assertThrows;
1313
import static org.sosy_lab.java_smt.api.FormulaType.BooleanType;
1414
import static org.sosy_lab.java_smt.api.FormulaType.IntegerType;
1515

@@ -238,11 +238,7 @@ public void quantifierTest() {
238238
qmgr.exists(
239239
ImmutableList.of(variable1, variable2, variable3, variable4), bmgr.equivalence(f1, f2));
240240

241-
try {
242-
ackermannization.eliminateUfs(f);
243-
assert_().fail();
244-
} catch (IllegalArgumentException expected) {
245-
}
241+
assertThrows(IllegalArgumentException.class, () -> ackermannization.eliminateUfs(f));
246242
}
247243

248244
@Test

0 commit comments

Comments
 (0)