Skip to content

Commit 754ebdb

Browse files
danpoedanpoe
committed
Add regression tests for CProverString.toString() operations
1 parent 1639ab5 commit 754ebdb

File tree

8 files changed

+180
-0
lines changed

8 files changed

+180
-0
lines changed

‎jbmc/regression/jbmc-strings/CProverStringToString/Main.class

2.16 KB
Binary file not shown.

‎jbmc/regression/jbmc-strings/CProverStringToString/Main.java

Lines changed: 132 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,132 @@
1+
import org.cprover.CProverString;
2+
3+
class Main {
4+
public void testIntSuccess(int choice) {
5+
int i;
6+
String r;
7+
8+
switch (choice) {
9+
case 0:
10+
i = 0;
11+
r = "0";
12+
break;
13+
case 1:
14+
i = 1;
15+
r = "1";
16+
break;
17+
case 2:
18+
i = -1;
19+
r = "-1";
20+
break;
21+
case 3:
22+
i = Integer.MIN_VALUE;
23+
r = "-2147483648";
24+
case 4:
25+
i = Integer.MAX_VALUE;
26+
r = "2147483647";
27+
default:
28+
return;
29+
}
30+
31+
String s = CProverString.toString(i);
32+
assert s.equals(r);
33+
}
34+
35+
public void testIntFailure() {
36+
String s = CProverString.toString(123);
37+
assert s.equals("0");
38+
}
39+
40+
public void testLongSuccess(int choice) {
41+
long l;
42+
String r;
43+
44+
switch (choice) {
45+
case 0:
46+
l = 0L;
47+
r = "0";
48+
break;
49+
case 1:
50+
l = 1L;
51+
r = "1";
52+
break;
53+
case 2:
54+
l = -1L;
55+
r = "-1";
56+
break;
57+
case 3:
58+
l = Long.MIN_VALUE;
59+
;
60+
r = "-9223372036854775808";
61+
break;
62+
case 4:
63+
l = Long.MAX_VALUE;
64+
r = "9223372036854775807";
65+
break;
66+
default:
67+
return;
68+
}
69+
70+
String s = CProverString.toString(l);
71+
assert s.equals(r);
72+
}
73+
74+
public void testLongFailure() {
75+
String s = CProverString.toString(9223372036854775807L);
76+
assert s.equals("0");
77+
}
78+
79+
public void testFloatSuccess(int choice) {
80+
float f;
81+
String r;
82+
83+
switch (choice) {
84+
case 0:
85+
f = 0F;
86+
r = "0.0";
87+
break;
88+
case 1:
89+
f = 1F;
90+
r = "1.0";
91+
break;
92+
case 2:
93+
f = -1F;
94+
r = "-1.0";
95+
break;
96+
case 3:
97+
f = 1.1F;
98+
r = "1.1";
99+
break;
100+
case 4:
101+
f = Float.MAX_VALUE;
102+
r = "3.4028235E38";
103+
break;
104+
case 5:
105+
f = Float.MIN_VALUE;
106+
r = "1.4E-45";
107+
break;
108+
case 6:
109+
f = Float.POSITIVE_INFINITY;
110+
r = "Infinity";
111+
break;
112+
case 7:
113+
f = Float.NEGATIVE_INFINITY;
114+
r = "-Infinity";
115+
break;
116+
case 8:
117+
f = Float.NaN;
118+
r = "NaN";
119+
break;
120+
default:
121+
return;
122+
}
123+
124+
String s = CProverString.toString(f);
125+
assert s.equals(r);
126+
}
127+
128+
public void testFloatFailure() {
129+
String s = CProverString.toString(1.1F);
130+
assert s.equals("0");
131+
}
132+
}

‎jbmc/regression/jbmc-strings/CProverStringToString/test_float_fail.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
Main.class
3+
--function Main.testFloatFailure --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
--

‎jbmc/regression/jbmc-strings/CProverStringToString/test_float_success.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
Main.class
3+
--function Main.testFloatSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--

‎jbmc/regression/jbmc-strings/CProverStringToString/test_int_fail.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
Main.class
3+
--function Main.testIntFailure --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
--

‎jbmc/regression/jbmc-strings/CProverStringToString/test_int_success.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
Main.class
3+
--function Main.testIntSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--

‎jbmc/regression/jbmc-strings/CProverStringToString/test_long_fail.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
Main.class
3+
--function Main.testLongFailure --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
--

‎jbmc/regression/jbmc-strings/CProverStringToString/test_long_success.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
Main.class
3+
--function Main.testLongSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--

0 commit comments

Comments
 (0)