Skip to content

Commit 51c0047

Browse files
committed
Refactored tests
Due to multiple error check/annotation, some tests have been merged into single files to reduce testing workload. Math tests need to be reviewed due to weird behavior if the refinements aren't alone in the same folder as the test.
1 parent 19e479c commit 51c0047

30 files changed

+178
-280
lines changed

liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,16 +4,28 @@
44

55
@SuppressWarnings("unused")
66
public class ErrorAfterIf {
7-
public void have2(int a, int b) {
7+
public void afterIf1(int a, int b) {
88
@Refinement("pos > 0")
99
int pos = 10;
1010

1111
if (a > 0 && b > 0) {
1212
pos = a;
1313
} else {
14-
if (b > 0) pos = b;
14+
if (b > 0)
15+
pos = b;
1516
}
1617
@Refinement("_ == a || _ == b")
1718
int r = pos; // Refinement Error
1819
}
20+
21+
public void afterIf2() {
22+
@Refinement("k > 0 && k < 100")
23+
int k = 5;
24+
if (k > 7) {
25+
k = 9;
26+
}
27+
k = 50;
28+
@Refinement("_ < 10")
29+
int m = k; // Refinement Error
30+
}
1931
}

liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java

Lines changed: 0 additions & 17 deletions
This file was deleted.
Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
@SuppressWarnings("unused")
6+
public class ErrorArithmeticFP {
7+
8+
private static void arithmetic1(){
9+
@Refinement("_ > 5.0")
10+
double a = 5.0; // Refinement Error
11+
}
12+
13+
private static void arithmetic2(){
14+
@Refinement("_ > 5.0")
15+
double a = 5.5;
16+
17+
@Refinement("_ == 10.0")
18+
double c = a * 2.0; // Refinement Error
19+
}
20+
21+
private static void arithmetic3(){
22+
@Refinement("_ > 5.0")
23+
double a = 5.5;
24+
25+
@Refinement("_ < -5.5")
26+
double d = -a; // Refinement Error
27+
}
28+
29+
private static void arithmetic4(){
30+
@Refinement("_ > 5.0")
31+
double a = 5.5;
32+
33+
@Refinement("_ < -5.5")
34+
double d = -(a - 2.0); // Refinement Error
35+
}
36+
}

liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java

Lines changed: 0 additions & 12 deletions
This file was deleted.

liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java

Lines changed: 0 additions & 15 deletions
This file was deleted.

liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java

Lines changed: 0 additions & 13 deletions
This file was deleted.

liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java

Lines changed: 0 additions & 14 deletions
This file was deleted.

liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java

Lines changed: 0 additions & 11 deletions
This file was deleted.

liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java

Lines changed: 0 additions & 11 deletions
This file was deleted.

liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java

Lines changed: 0 additions & 11 deletions
This file was deleted.

0 commit comments

Comments
 (0)