File tree 4 files changed +32
-9
lines changed
jbmc/regression/strings-smoke-tests/java_intern 4 files changed +32
-9
lines changed Original file line number Diff line number Diff line change 1
1
CORE
2
2
test_intern.class
3
- --max-nondet-string-length 1000 --function test_intern.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --unwind 10
3
+ --max-nondet-string-length 1000 --function test_intern.testPass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --unwind 10
4
4
^EXIT=0$
5
5
^SIGNAL=0$
6
- ^\[.*assertion.1\].* line 9 .* SUCCESS$
6
+ ^\[.*assertion.1\].* line 12 .* SUCCESS$
7
7
--
8
8
non equal types
Original file line number Diff line number Diff line change
1
+ CORE
2
+ test_intern.class
3
+ --max-nondet-string-length 1000 --function test_intern.testFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --unwind 10
4
+ ^EXIT=10$
5
+ ^SIGNAL=0$
6
+ ^\[.*assertion.1\].* line 24.* FAILURE$
7
+ --
8
+ non equal types
Original file line number Diff line number Diff line change 1
1
public class test_intern
2
2
{
3
- public static void main ()
4
- {
5
- String s1 = "abc" ;
6
- String s3 = "abc" ;
7
- String x = s1 .intern ();
8
- String y = s3 .intern ();
9
- assert (x == y );
3
+ public static void testPass ()
4
+ {
5
+ // Arrange
6
+ String s1 = "abc" ;
7
+ String s2 = "abc" ;
8
+ // Act
9
+ String x = s1 .intern ();
10
+ String y = s2 .intern ();
11
+ // Assert
12
+ assert (x == y );
13
+ }
14
+
15
+ public static void testFail ()
16
+ {
17
+ // Arrange
18
+ String s1 = "abc" ;
19
+ String s2 = "abd" ;
20
+ // Act
21
+ String x = s1 .intern ();
22
+ String y = s2 .intern ();
23
+ // Assert
24
+ assert (x == y );
10
25
}
11
26
}
You can’t perform that action at this time.
0 commit comments