From 52a4fc6f445610a5a2f2b76ce537651ea3fb736e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 1 Apr 2019 09:29:07 +0100 Subject: [PATCH 1/5] Update java-models-library for diffblue/java-models-library#19 (getMonitorCount) https://github.com/diffblue/java-models-library/pull/19 --- jbmc/lib/java-models-library | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library index 766ac7a2c87..d92026cd8dd 160000 --- a/jbmc/lib/java-models-library +++ b/jbmc/lib/java-models-library @@ -1 +1 @@ -Subproject commit 766ac7a2c87dadfc7286ea0aab0a6eabdf3e4cdc +Subproject commit d92026cd8dd8f1e769f5b11831e831fefdc4c080 From 1b8feb87188821fe2f386ccb4bb5298ddc169978 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 1 Apr 2019 09:45:04 +0100 Subject: [PATCH 2/5] Activate tests working after submodule update This shows that the changes brought with the update are working correctly. --- jbmc/regression/jbmc-strings/TokenTest01/test.desc | 4 ++-- jbmc/regression/jbmc-strings/TokenTest02/test.desc | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/jbmc/regression/jbmc-strings/TokenTest01/test.desc b/jbmc/regression/jbmc-strings/TokenTest01/test.desc index 2de78f35997..8f1f684e1f9 100644 --- a/jbmc/regression/jbmc-strings/TokenTest01/test.desc +++ b/jbmc/regression/jbmc-strings/TokenTest01/test.desc @@ -1,6 +1,6 @@ -FUTURE +CORE TokenTest01.class ---max-nondet-string-length 1000 --unwind 30 +--max-nondet-string-length 1000 --unwind 30 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/TokenTest02/test.desc b/jbmc/regression/jbmc-strings/TokenTest02/test.desc index b065ddf0d67..b94f880173a 100644 --- a/jbmc/regression/jbmc-strings/TokenTest02/test.desc +++ b/jbmc/regression/jbmc-strings/TokenTest02/test.desc @@ -1,6 +1,6 @@ -FUTURE +CORE TokenTest02.class ---max-nondet-string-length 1000 --unwind 15 +--max-nondet-string-length 1000 --unwind 15 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ From 4b86c69e88e676bebedd04c1f524a25bd249b864 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 1 Apr 2019 10:16:31 +0100 Subject: [PATCH 3/5] Reduce unwind value for TokenTest01 Unwind 6 should be enough to detect any error and makes jbmc end quicker than with 30. --- jbmc/regression/jbmc-strings/TokenTest01/test.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/regression/jbmc-strings/TokenTest01/test.desc b/jbmc/regression/jbmc-strings/TokenTest01/test.desc index 8f1f684e1f9..210c573d3f0 100644 --- a/jbmc/regression/jbmc-strings/TokenTest01/test.desc +++ b/jbmc/regression/jbmc-strings/TokenTest01/test.desc @@ -1,6 +1,6 @@ CORE TokenTest01.class ---max-nondet-string-length 1000 --unwind 30 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +--max-nondet-string-length 1000 --unwind 6 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ From 260da11783f4a25aa5a55bf63c9342798a303ab1 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 1 Apr 2019 10:19:29 +0100 Subject: [PATCH 4/5] Strengthen condition in TokenTest02 and reduce unwind The check for VERIFICATION FAILED could match a null pointer check rather than an assertion. --- jbmc/regression/jbmc-strings/TokenTest02/test.desc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/jbmc/regression/jbmc-strings/TokenTest02/test.desc b/jbmc/regression/jbmc-strings/TokenTest02/test.desc index b94f880173a..a22c7f272a4 100644 --- a/jbmc/regression/jbmc-strings/TokenTest02/test.desc +++ b/jbmc/regression/jbmc-strings/TokenTest02/test.desc @@ -1,8 +1,9 @@ CORE TokenTest02.class ---max-nondet-string-length 1000 --unwind 15 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +--max-nondet-string-length 1000 --unwind 6 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ +line 13 assertion at file TokenTest02\.java .*: FAILURE -- ^warning: ignoring From 4254f76fe5005ccdc1fc8ee95c1d5b149632f79c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Sun, 25 Nov 2018 20:01:59 +0000 Subject: [PATCH 5/5] Activate tests fixed by getChar models --- jbmc/regression/jbmc-strings/StringBuilderChars04/test.desc | 4 ++-- jbmc/regression/jbmc-strings/StringMiscellaneous01/test.desc | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/jbmc/regression/jbmc-strings/StringBuilderChars04/test.desc b/jbmc/regression/jbmc-strings/StringBuilderChars04/test.desc index 0923359deef..8df4c46ffc9 100644 --- a/jbmc/regression/jbmc-strings/StringBuilderChars04/test.desc +++ b/jbmc/regression/jbmc-strings/StringBuilderChars04/test.desc @@ -1,6 +1,6 @@ -FUTURE +CORE StringBuilderChars04.class ---max-nondet-string-length 1000 --unwind 100 +--max-nondet-string-length 1000 --unwind 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringMiscellaneous01/test.desc b/jbmc/regression/jbmc-strings/StringMiscellaneous01/test.desc index b6fc0921c0c..5166387582c 100644 --- a/jbmc/regression/jbmc-strings/StringMiscellaneous01/test.desc +++ b/jbmc/regression/jbmc-strings/StringMiscellaneous01/test.desc @@ -1,6 +1,6 @@ -FUTURE +CORE StringMiscellaneous01.class ---max-nondet-string-length 1000 --unwind 30 +--max-nondet-string-length 1000 --unwind 30 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$