replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Improve test for String.intern 

We add a version of the test which should fail in addition to the one
that should pass.
This commit is contained in:
Romain Brenguier 2019-04-30 08:10:38 +01:00
parent e6a5a11a4e
commit 524c13ff2d
4 changed files with 32 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
jbmc/regression/strings-smoke-tests/java_intern/test.desc
View File

@ -1,8 +1,8 @@
CORE
test_intern.class
--max-nondet-string-length 1000 --function test_intern.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --unwind 10
--max-nondet-string-length 1000 --function test_intern.testPass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --unwind 10
^EXIT=0$
^SIGNAL=0$
^\[.*assertion.1\].* line 9.* SUCCESS$
^\[.*assertion.1\].* line 12.* SUCCESS$
--
non equal types

8
jbmc/regression/strings-smoke-tests/java_intern/testFail.desc Normal file
View File

@ -0,0 +1,8 @@
CORE
test_intern.class
--max-nondet-string-length 1000 --function test_intern.testFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --unwind 10
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 24.* FAILURE$
--
non equal types

BIN
jbmc/regression/strings-smoke-tests/java_intern/test_intern.class
View File

Binary file not shown.

29
jbmc/regression/strings-smoke-tests/java_intern/test_intern.java
View File

@ -1,11 +1,26 @@
public class test_intern
{
public static void main()
{
String s1 = "abc";
String s3 = "abc";
String x = s1.intern();
String y = s3.intern();
assert(x == y);
public static void testPass()
{
// Arrange
String s1 = "abc";
String s2 = "abc";
// Act
String x = s1.intern();
String y = s2.intern();
// Assert
assert(x == y);
}
public static void testFail()
{
// Arrange
String s1 = "abc";
String s2 = "abd";
// Act
String x = s1.intern();
String y = s2.intern();
// Assert
assert(x == y);
}
}