diff --git a/jbmc/regression/jbmc-strings/bug-test-gen-119-2/test.desc b/jbmc/regression/jbmc-strings/bug-test-gen-119-2/test.desc index 447be05df73..0f52c235798 100644 --- a/jbmc/regression/jbmc-strings/bug-test-gen-119-2/test.desc +++ b/jbmc/regression/jbmc-strings/bug-test-gen-119-2/test.desc @@ -1,6 +1,6 @@ CORE StringValueOfLong.class ---refine-strings --string-max-length 1000 +--refine-strings --string-max-length 1000 --function StringValueOfLong.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/bug-test-gen-119/test.desc b/jbmc/regression/jbmc-strings/bug-test-gen-119/test.desc index 22bd78b3cac..c0f9b9e2d82 100644 --- a/jbmc/regression/jbmc-strings/bug-test-gen-119/test.desc +++ b/jbmc/regression/jbmc-strings/bug-test-gen-119/test.desc @@ -1,6 +1,6 @@ CORE StringValueOfBool.class ---refine-strings --string-max-length 1000 +--refine-strings --string-max-length 1000 --function StringValueOfBool.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/java_append_string/test.desc b/jbmc/regression/jbmc-strings/java_append_string/test.desc deleted file mode 100644 index cb881ab83d9..00000000000 --- a/jbmc/regression/jbmc-strings/java_append_string/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -FUTURE -test_append_string.class ---refine-strings --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion.1\].* line 12.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_append_string/test_append_string.class b/jbmc/regression/jbmc-strings/java_append_string/test_append_string.class deleted file mode 100644 index f2cb5cf8bea..00000000000 Binary files a/jbmc/regression/jbmc-strings/java_append_string/test_append_string.class and /dev/null differ diff --git a/jbmc/regression/jbmc-strings/java_append_string/test_append_string.java b/jbmc/regression/jbmc-strings/java_append_string/test_append_string.java deleted file mode 100644 index 54665da29cc..00000000000 --- a/jbmc/regression/jbmc-strings/java_append_string/test_append_string.java +++ /dev/null @@ -1,14 +0,0 @@ -public class test_append_string -{ - public static void main(/*String[] args*/) - { - String di = new String("di"); - StringBuilder diff = new StringBuilder(); - diff.append(di); - diff.append("ff"); - System.out.println(diff); - String s = diff.toString(); - System.out.println(s); - assert (!s.equals("diff")); - } -} diff --git a/jbmc/regression/jbmc-strings/java_case/test.desc b/jbmc/regression/jbmc-strings/java_case/test.desc deleted file mode 100644 index 22d58ddb3ac..00000000000 --- a/jbmc/regression/jbmc-strings/java_case/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_case.class ---refine-strings --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 8.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_case/test_case.class b/jbmc/regression/jbmc-strings/java_case/test_case.class deleted file mode 100644 index 5887b496986..00000000000 Binary files a/jbmc/regression/jbmc-strings/java_case/test_case.class and /dev/null differ diff --git a/jbmc/regression/jbmc-strings/java_case/test_case.java b/jbmc/regression/jbmc-strings/java_case/test_case.java deleted file mode 100644 index 309abfc07b9..00000000000 --- a/jbmc/regression/jbmc-strings/java_case/test_case.java +++ /dev/null @@ -1,12 +0,0 @@ -public class test_case -{ - public static void main(/*String[] argv*/) - { - String s = new String("Ab"); - String l = s.toLowerCase(); - String u = s.toUpperCase(); - assert(!l.equals("ab") || - !u.equals("AB") || - !s.equalsIgnoreCase("aB")); - } -} diff --git a/jbmc/regression/jbmc-strings/java_char_array/test.desc b/jbmc/regression/jbmc-strings/java_char_array/test.desc deleted file mode 100644 index aaf2c9f8fd4..00000000000 --- a/jbmc/regression/jbmc-strings/java_char_array/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_char_array.class ---refine-strings --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 9.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_char_array/test_char_array.class b/jbmc/regression/jbmc-strings/java_char_array/test_char_array.class deleted file mode 100644 index 38a7ecf41ed..00000000000 Binary files a/jbmc/regression/jbmc-strings/java_char_array/test_char_array.class and /dev/null differ diff --git a/jbmc/regression/jbmc-strings/java_char_array/test_char_array.java b/jbmc/regression/jbmc-strings/java_char_array/test_char_array.java deleted file mode 100644 index 96e250fb030..00000000000 --- a/jbmc/regression/jbmc-strings/java_char_array/test_char_array.java +++ /dev/null @@ -1,13 +0,0 @@ -public class test_char_array -{ - public static void main(/*String[] argv*/) - { - String s = "abc"; - char [] str = s.toCharArray(); - char c = str[2]; - char a = s.charAt(0); - assert(str.length != 3 || - a != 'a' || - c != 'c'); - } -} diff --git a/jbmc/regression/jbmc-strings/java_char_at/test.desc b/jbmc/regression/jbmc-strings/java_char_at/test.desc index dd2c1c343ae..8507d50a8fb 100644 --- a/jbmc/regression/jbmc-strings/java_char_at/test.desc +++ b/jbmc/regression/jbmc-strings/java_char_at/test.desc @@ -1,6 +1,6 @@ CORE test_char_at.class ---refine-strings --string-max-length 1000 +--refine-strings --string-max-length 1000 --function test_char_at.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 5.* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/java_char_at/test_char_at.java b/jbmc/regression/jbmc-strings/java_char_at/test_char_at.java index 9ae02733fb8..17e73b6baf6 100644 --- a/jbmc/regression/jbmc-strings/java_char_at/test_char_at.java +++ b/jbmc/regression/jbmc-strings/java_char_at/test_char_at.java @@ -1,6 +1,6 @@ public class test_char_at { - public static void main(/*String[] argv*/) { + public static void main() { String s = new String("abc"); assert(s.charAt(2)!='c'); } diff --git a/jbmc/regression/jbmc-strings/java_code_point/test.desc b/jbmc/regression/jbmc-strings/java_code_point/test.desc deleted file mode 100644 index 322ead7c0a1..00000000000 --- a/jbmc/regression/jbmc-strings/java_code_point/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_code_point.class ---refine-strings --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 8.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_code_point/test_code_point.class b/jbmc/regression/jbmc-strings/java_code_point/test_code_point.class deleted file mode 100644 index f2f5fbad63a..00000000000 Binary files a/jbmc/regression/jbmc-strings/java_code_point/test_code_point.class and /dev/null differ diff --git a/jbmc/regression/jbmc-strings/java_code_point/test_code_point.java b/jbmc/regression/jbmc-strings/java_code_point/test_code_point.java deleted file mode 100644 index 345dc1fa08b..00000000000 --- a/jbmc/regression/jbmc-strings/java_code_point/test_code_point.java +++ /dev/null @@ -1,14 +0,0 @@ -public class test_code_point -{ - public static void main(/*String[] argv*/) - { - String s = "!𐤇𐤄𐤋𐤋𐤅"; - StringBuilder sb = new StringBuilder(); - sb.appendCodePoint(0x10907); - assert(s.codePointAt(1) != 67847 || - s.codePointBefore(3) != 67847 || - s.codePointCount(1,5) < 2 || - s.offsetByCodePoints(1,2) < 3 || - s.charAt(1) != sb.charAt(0)); - } -} diff --git a/jbmc/regression/jbmc-strings/java_compare/test.desc b/jbmc/regression/jbmc-strings/java_compare/test.desc index 6b8c890288d..0d7310590bc 100644 --- a/jbmc/regression/jbmc-strings/java_compare/test.desc +++ b/jbmc/regression/jbmc-strings/java_compare/test.desc @@ -1,6 +1,6 @@ CORE test_compare.class ---refine-strings --string-max-length 1000 +--refine-strings --string-max-length 1000 --function test_compare.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 7.* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/java_compare/test_compare.java b/jbmc/regression/jbmc-strings/java_compare/test_compare.java index 0a535fd0bf3..1c3c1de86d8 100644 --- a/jbmc/regression/jbmc-strings/java_compare/test_compare.java +++ b/jbmc/regression/jbmc-strings/java_compare/test_compare.java @@ -1,6 +1,6 @@ public class test_compare { - public static void main(/*String[] argv*/) + public static void main() { String s1 = "ab"; String s2 = "aa"; diff --git a/jbmc/regression/jbmc-strings/java_concat/test.desc b/jbmc/regression/jbmc-strings/java_concat/test.desc index 6063f361aa5..b1d47ce246d 100644 --- a/jbmc/regression/jbmc-strings/java_concat/test.desc +++ b/jbmc/regression/jbmc-strings/java_concat/test.desc @@ -1,6 +1,6 @@ CORE test_concat.class ---refine-strings --string-max-length 1000 +--refine-strings --string-max-length 1000 --function test_concat.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 10.* SUCCESS$ diff --git a/jbmc/regression/jbmc-strings/java_concat/test_concat.java b/jbmc/regression/jbmc-strings/java_concat/test_concat.java index 9f4d3f5e371..b4b9a54f242 100644 --- a/jbmc/regression/jbmc-strings/java_concat/test_concat.java +++ b/jbmc/regression/jbmc-strings/java_concat/test_concat.java @@ -1,6 +1,6 @@ public class test_concat { - public static void main(/*String[] argv*/) + public static void main() { String s = new String("pi"); int i = s.length(); diff --git a/jbmc/regression/jbmc-strings/java_contains/test.desc b/jbmc/regression/jbmc-strings/java_contains/test.desc deleted file mode 100644 index c5166216bb1..00000000000 --- a/jbmc/regression/jbmc-strings/java_contains/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_contains.class ---refine-strings --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 7.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_contains/test_contains.class b/jbmc/regression/jbmc-strings/java_contains/test_contains.class deleted file mode 100644 index 9bbccb03775..00000000000 Binary files a/jbmc/regression/jbmc-strings/java_contains/test_contains.class and /dev/null differ diff --git a/jbmc/regression/jbmc-strings/java_contains/test_contains.java b/jbmc/regression/jbmc-strings/java_contains/test_contains.java deleted file mode 100644 index 6f4c60a1a2e..00000000000 --- a/jbmc/regression/jbmc-strings/java_contains/test_contains.java +++ /dev/null @@ -1,9 +0,0 @@ -public class test_contains -{ - public static void main(/*String[] argv*/) - { - String s = new String("Abc"); - String u = "bc"; - assert(!s.contains(u)); - } -} diff --git a/jbmc/regression/jbmc-strings/java_delete/test.desc b/jbmc/regression/jbmc-strings/java_delete/test.desc index 721165e152d..44af4af9c68 100644 --- a/jbmc/regression/jbmc-strings/java_delete/test.desc +++ b/jbmc/regression/jbmc-strings/java_delete/test.desc @@ -1,6 +1,6 @@ CORE test_delete.class ---refine-strings --string-max-length 1000 +--refine-strings --string-max-length 1000 --function test_delete.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 8.* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/java_delete/test_delete.java b/jbmc/regression/jbmc-strings/java_delete/test_delete.java index 62ea5dbf9ce..86ffbb8593a 100644 --- a/jbmc/regression/jbmc-strings/java_delete/test_delete.java +++ b/jbmc/regression/jbmc-strings/java_delete/test_delete.java @@ -1,6 +1,6 @@ public class test_delete { - public static void main(/*String[] argv*/) + public static void main() { StringBuilder s = new StringBuilder("Abc"); org.cprover.CProverString.delete(s,1,2); diff --git a/jbmc/regression/jbmc-strings/java_delete_char_at/test.desc b/jbmc/regression/jbmc-strings/java_delete_char_at/test.desc deleted file mode 100644 index 2ec7b55da93..00000000000 --- a/jbmc/regression/jbmc-strings/java_delete_char_at/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_delete_char_at.class ---refine-strings --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 9.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class b/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class deleted file mode 100644 index 130e3d10f6c..00000000000 Binary files a/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class and /dev/null differ diff --git a/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java b/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java deleted file mode 100644 index d43a2845f95..00000000000 --- a/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java +++ /dev/null @@ -1,11 +0,0 @@ -public class test_delete_char_at -{ - public static void main(/*String[] argv*/) - { - StringBuilder s = new StringBuilder(); - s.append("Abc"); - org.cprover.CProverString.deleteCharAt(s, 1); - String str = s.toString(); - assert(!str.equals("Ac")); - } -} diff --git a/jbmc/regression/jbmc-strings/java_empty/test.desc b/jbmc/regression/jbmc-strings/java_empty/test.desc index 4c9cf9d82eb..32e54658d79 100644 --- a/jbmc/regression/jbmc-strings/java_empty/test.desc +++ b/jbmc/regression/jbmc-strings/java_empty/test.desc @@ -1,6 +1,6 @@ CORE test_empty.class ---refine-strings --string-max-length 1000 +--refine-strings --string-max-length 1000 --function test_empty.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 6.* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/java_empty/test_empty.java b/jbmc/regression/jbmc-strings/java_empty/test_empty.java index 18fde4a115e..734d9290ede 100644 --- a/jbmc/regression/jbmc-strings/java_empty/test_empty.java +++ b/jbmc/regression/jbmc-strings/java_empty/test_empty.java @@ -1,6 +1,6 @@ public class test_empty { - public static void main(/*String[] argv*/) + public static void main() { String empty = ""; assert(!empty.isEmpty()); diff --git a/jbmc/regression/jbmc-strings/java_endswith/test.desc b/jbmc/regression/jbmc-strings/java_endswith/test.desc deleted file mode 100644 index 10f8a8b0e2f..00000000000 --- a/jbmc/regression/jbmc-strings/java_endswith/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_endswith.class ---refine-strings --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 7.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_endswith/test_endswith.class b/jbmc/regression/jbmc-strings/java_endswith/test_endswith.class deleted file mode 100644 index e3d453c444f..00000000000 Binary files a/jbmc/regression/jbmc-strings/java_endswith/test_endswith.class and /dev/null differ diff --git a/jbmc/regression/jbmc-strings/java_endswith/test_endswith.java b/jbmc/regression/jbmc-strings/java_endswith/test_endswith.java deleted file mode 100644 index fabf6f8dde0..00000000000 --- a/jbmc/regression/jbmc-strings/java_endswith/test_endswith.java +++ /dev/null @@ -1,9 +0,0 @@ -public class test_endswith -{ - public static void main(/*String[] argv*/) - { - String s = new String("Abcd"); - String suff = "cd"; - assert(!s.endsWith(suff)); - } -} diff --git a/jbmc/regression/jbmc-strings/java_equal/test.desc b/jbmc/regression/jbmc-strings/java_equal/test.desc deleted file mode 100644 index bd4d1022d78..00000000000 --- a/jbmc/regression/jbmc-strings/java_equal/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_equal.class ---refine-strings --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 8.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_equal/test_equal.class b/jbmc/regression/jbmc-strings/java_equal/test_equal.class deleted file mode 100644 index e0fc6db8aaf..00000000000 Binary files a/jbmc/regression/jbmc-strings/java_equal/test_equal.class and /dev/null differ diff --git a/jbmc/regression/jbmc-strings/java_equal/test_equal.java b/jbmc/regression/jbmc-strings/java_equal/test_equal.java deleted file mode 100644 index e8c9ac7cb1a..00000000000 --- a/jbmc/regression/jbmc-strings/java_equal/test_equal.java +++ /dev/null @@ -1,9 +0,0 @@ -public class test_equal -{ - public static void main(String[] argv) - { - String s = new String("pi"); - String t = new String("po"); - assert(!s.equals(t)); - } -} diff --git a/jbmc/regression/jbmc-strings/java_float/test.desc b/jbmc/regression/jbmc-strings/java_float/test.desc deleted file mode 100644 index d79c25dab3a..00000000000 --- a/jbmc/regression/jbmc-strings/java_float/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -THOROUGH -test_float.class ---refine-strings --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 15.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_float/test_float.class b/jbmc/regression/jbmc-strings/java_float/test_float.class deleted file mode 100644 index 00e8622e2ac..00000000000 Binary files a/jbmc/regression/jbmc-strings/java_float/test_float.class and /dev/null differ diff --git a/jbmc/regression/jbmc-strings/java_float/test_float.java b/jbmc/regression/jbmc-strings/java_float/test_float.java deleted file mode 100644 index 312f1aeaf10..00000000000 --- a/jbmc/regression/jbmc-strings/java_float/test_float.java +++ /dev/null @@ -1,17 +0,0 @@ -public class test_float -{ - public static void main(/*String[] arg*/) - { - float inf = 100.0f / 0.0f; - float minus_inf = -100.0f / 0.0f; - float nan = 0.0f / 0.0f; - String inf_string = Float.toString(inf); - String mininf_string = Float.toString(minus_inf); - String nan_string = Float.toString(nan); - System.out.println(nan_string); - System.out.println(inf_string); - System.out.println(mininf_string); - assert(!nan_string.equals("NaN") || !inf_string.equals("Infinity") - || !mininf_string.equals("-Infinity")); - } -} diff --git a/jbmc/regression/jbmc-strings/java_hash_code/test.desc b/jbmc/regression/jbmc-strings/java_hash_code/test.desc deleted file mode 100644 index 70dfc7e6bbe..00000000000 --- a/jbmc/regression/jbmc-strings/java_hash_code/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_hash_code.class ---refine-strings --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 7.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.class b/jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.class deleted file mode 100644 index d9b3e2b2f3d..00000000000 Binary files a/jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.class and /dev/null differ diff --git a/jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.java b/jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.java deleted file mode 100644 index fbc15f0b4c2..00000000000 --- a/jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.java +++ /dev/null @@ -1,9 +0,0 @@ -public class test_hash_code -{ - public static void main(/*String[] argv*/) - { - String s1 = "ab"; - String s2 = "ab"; - assert(s1.hashCode() != s2.hashCode()); - } -} diff --git a/jbmc/regression/jbmc-strings/java_index_of/test.desc b/jbmc/regression/jbmc-strings/java_index_of/test.desc deleted file mode 100644 index b4289558902..00000000000 --- a/jbmc/regression/jbmc-strings/java_index_of/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_index_of.class ---refine-strings --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 8.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_index_of/test_index_of.class b/jbmc/regression/jbmc-strings/java_index_of/test_index_of.class deleted file mode 100644 index cae397a79fb..00000000000 Binary files a/jbmc/regression/jbmc-strings/java_index_of/test_index_of.class and /dev/null differ diff --git a/jbmc/regression/jbmc-strings/java_index_of/test_index_of.java b/jbmc/regression/jbmc-strings/java_index_of/test_index_of.java deleted file mode 100644 index b607ba79570..00000000000 --- a/jbmc/regression/jbmc-strings/java_index_of/test_index_of.java +++ /dev/null @@ -1,10 +0,0 @@ -public class test_index_of -{ - public static void main(/*String[] argv*/) - { - String s = "Abc"; - String bc = "bc"; - int i = s.indexOf(bc); - assert(i != 1); - } -} diff --git a/jbmc/regression/jbmc-strings/java_index_of_char/test.desc b/jbmc/regression/jbmc-strings/java_index_of_char/test.desc deleted file mode 100644 index e40554cc835..00000000000 --- a/jbmc/regression/jbmc-strings/java_index_of_char/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_index_of_char.class ---refine-strings --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 8.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.class b/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.class deleted file mode 100644 index bf4fa6e946e..00000000000 Binary files a/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.class and /dev/null differ diff --git a/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.java b/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.java deleted file mode 100644 index 92d75b3b07d..00000000000 --- a/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.java +++ /dev/null @@ -1,10 +0,0 @@ -public class test_index_of_char -{ - public static void main(/*String[] argv*/) - { - String s = "Abc"; - char c = 'c'; - int i = s.indexOf(c); - assert(i != 2); - } -} diff --git a/jbmc/regression/jbmc-strings/java_insert_char/test.desc b/jbmc/regression/jbmc-strings/java_insert_char/test.desc index cdda3eeae95..7cd1cde2df7 100644 --- a/jbmc/regression/jbmc-strings/java_insert_char/test.desc +++ b/jbmc/regression/jbmc-strings/java_insert_char/test.desc @@ -1,6 +1,6 @@ CORE test_insert_char.class ---refine-strings --string-max-length 1000 +--refine-strings --string-max-length 1000 --function test_insert_char.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 8.* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/java_insert_char/test_insert_char.java b/jbmc/regression/jbmc-strings/java_insert_char/test_insert_char.java index 12dcc8cdb90..12798d84aef 100644 --- a/jbmc/regression/jbmc-strings/java_insert_char/test_insert_char.java +++ b/jbmc/regression/jbmc-strings/java_insert_char/test_insert_char.java @@ -1,6 +1,6 @@ public class test_insert_char { - public static void main(/*String[] argv*/) + public static void main() { StringBuilder sb = new StringBuilder("ac"); org.cprover.CProverString.insert(sb, 1, 'b'); diff --git a/jbmc/regression/jbmc-strings/java_insert_char_array/test.desc b/jbmc/regression/jbmc-strings/java_insert_char_array/test.desc deleted file mode 100644 index 0fd3fc08bb0..00000000000 --- a/jbmc/regression/jbmc-strings/java_insert_char_array/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -test_insert_char_array.class ---refine-strings --string-max-length 1000 --function test_insert_char_array.main -^EXIT=10$ -^SIGNAL=0$ -assertion.* line 26.* SUCCESS$ -assertion.* line 28.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class b/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class deleted file mode 100644 index c19a742c0f4..00000000000 Binary files a/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class and /dev/null differ diff --git a/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java b/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java deleted file mode 100644 index f392655afc1..00000000000 --- a/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java +++ /dev/null @@ -1,30 +0,0 @@ -public class test_insert_char_array -{ - // These are models of the String methods manipulating char arrays - public static String stringOfCharArray(char arr[]) - { - StringBuilder sb=new StringBuilder(""); - for(int i=0; i1) + { + assert(args[0] != null); // must hold + assert(args[1] != null); // must hold + } + } +} diff --git a/jbmc/regression/jbmc/main-args-elements-non-null1/test.desc b/jbmc/regression/jbmc/main-args-elements-non-null1/test.desc new file mode 100644 index 00000000000..3866f268f76 --- /dev/null +++ b/jbmc/regression/jbmc/main-args-elements-non-null1/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/main-args-elements-non-null2/Main.class b/jbmc/regression/jbmc/main-args-elements-non-null2/Main.class new file mode 100644 index 00000000000..396d39badf4 Binary files /dev/null and b/jbmc/regression/jbmc/main-args-elements-non-null2/Main.class differ diff --git a/jbmc/regression/jbmc/main-args-elements-non-null2/Main.java b/jbmc/regression/jbmc/main-args-elements-non-null2/Main.java new file mode 100644 index 00000000000..498f6d43056 --- /dev/null +++ b/jbmc/regression/jbmc/main-args-elements-non-null2/Main.java @@ -0,0 +1,9 @@ +public class Main +{ + public static void main(String[] args) + { + if(args.length>0) { + assert(args[0] != null); // must not fail + } + } +} diff --git a/jbmc/regression/jbmc/main-args-elements-non-null2/test.desc b/jbmc/regression/jbmc/main-args-elements-non-null2/test.desc new file mode 100644 index 00000000000..3866f268f76 --- /dev/null +++ b/jbmc/regression/jbmc/main-args-elements-non-null2/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.class b/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.class new file mode 100644 index 00000000000..53745bf4248 Binary files /dev/null and b/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.class differ diff --git a/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.java b/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.java new file mode 100644 index 00000000000..3ecee27827a --- /dev/null +++ b/jbmc/regression/jbmc/main-args-non-null-with-function1/Main.java @@ -0,0 +1,7 @@ +public class Main +{ + public static void main(String[] args) + { + assert(args != null); // must hold + } +} diff --git a/jbmc/regression/jbmc/main-args-non-null-with-function1/test.desc b/jbmc/regression/jbmc/main-args-non-null-with-function1/test.desc new file mode 100644 index 00000000000..9e275150f52 --- /dev/null +++ b/jbmc/regression/jbmc/main-args-non-null-with-function1/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.main +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/main-args-non-null1/Main.class b/jbmc/regression/jbmc/main-args-non-null1/Main.class new file mode 100644 index 00000000000..53745bf4248 Binary files /dev/null and b/jbmc/regression/jbmc/main-args-non-null1/Main.class differ diff --git a/jbmc/regression/jbmc/main-args-non-null1/Main.java b/jbmc/regression/jbmc/main-args-non-null1/Main.java new file mode 100644 index 00000000000..3ecee27827a --- /dev/null +++ b/jbmc/regression/jbmc/main-args-non-null1/Main.java @@ -0,0 +1,7 @@ +public class Main +{ + public static void main(String[] args) + { + assert(args != null); // must hold + } +} diff --git a/jbmc/regression/jbmc/main-args-non-null1/test.desc b/jbmc/regression/jbmc/main-args-non-null1/test.desc new file mode 100644 index 00000000000..3866f268f76 --- /dev/null +++ b/jbmc/regression/jbmc/main-args-non-null1/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/method_parmeters1/method_parameters.class b/jbmc/regression/jbmc/method_parameters1/method_parameters.class similarity index 100% rename from jbmc/regression/jbmc/method_parmeters1/method_parameters.class rename to jbmc/regression/jbmc/method_parameters1/method_parameters.class diff --git a/jbmc/regression/jbmc/method_parmeters1/method_parameters.java b/jbmc/regression/jbmc/method_parameters1/method_parameters.java similarity index 100% rename from jbmc/regression/jbmc/method_parmeters1/method_parameters.java rename to jbmc/regression/jbmc/method_parameters1/method_parameters.java diff --git a/jbmc/regression/jbmc/method_parmeters1/test.desc b/jbmc/regression/jbmc/method_parameters1/test.desc similarity index 100% rename from jbmc/regression/jbmc/method_parmeters1/test.desc rename to jbmc/regression/jbmc/method_parameters1/test.desc diff --git a/jbmc/regression/jbmc/method_parmeters2/method_parameters.class b/jbmc/regression/jbmc/method_parameters2/method_parameters.class similarity index 100% rename from jbmc/regression/jbmc/method_parmeters2/method_parameters.class rename to jbmc/regression/jbmc/method_parameters2/method_parameters.class diff --git a/jbmc/regression/jbmc/method_parmeters2/method_parameters.java b/jbmc/regression/jbmc/method_parameters2/method_parameters.java similarity index 100% rename from jbmc/regression/jbmc/method_parmeters2/method_parameters.java rename to jbmc/regression/jbmc/method_parameters2/method_parameters.java diff --git a/jbmc/regression/jbmc/method_parmeters2/test.desc b/jbmc/regression/jbmc/method_parameters2/test.desc similarity index 100% rename from jbmc/regression/jbmc/method_parmeters2/test.desc rename to jbmc/regression/jbmc/method_parameters2/test.desc diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.class new file mode 100644 index 00000000000..6e052a7f6f2 Binary files /dev/null and b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.java new file mode 100644 index 00000000000..14e556fa2a2 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/Main.java @@ -0,0 +1,8 @@ +public class Main +{ + static void main(String[] args) // not public! + { + if(args != null && args.length>0) + assert(args[0] != null); // allowed to fail + } +} diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/test.desc new file mode 100644 index 00000000000..c23c81e2d8d --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-elements-maybe-null1/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.class b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.class new file mode 100644 index 00000000000..cd3d63768c1 Binary files /dev/null and b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.java b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.java new file mode 100644 index 00000000000..97ad6061c78 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/Main.java @@ -0,0 +1,9 @@ +public class Main +{ + static void main(String[] args) // not public! + { + if(args != null && args.length>0) { + assert(args[0] == null); // allowed to fail + } + } +} diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/test.desc new file mode 100644 index 00000000000..c23c81e2d8d --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.class new file mode 100644 index 00000000000..3131f084ffc Binary files /dev/null and b/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.java new file mode 100644 index 00000000000..aa61bf38859 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-maybe-null1/Main.java @@ -0,0 +1,7 @@ +public class Main +{ + public void main(String[] args) // not static! + { + assert(args != null); // allowed to fail + } +} diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-args-maybe-null1/test.desc new file mode 100644 index 00000000000..c23c81e2d8d --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-maybe-null1/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.class b/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.class new file mode 100644 index 00000000000..203057c9f92 Binary files /dev/null and b/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.java b/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.java new file mode 100644 index 00000000000..0fae3e13177 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-maybe-null2/Main.java @@ -0,0 +1,7 @@ +public class Main +{ + public void main(String[] args) // not static! + { + assert(args == null); // allowed to fail + } +} diff --git a/jbmc/regression/jbmc/no-main-args-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-args-maybe-null2/test.desc new file mode 100644 index 00000000000..c23c81e2d8d --- /dev/null +++ b/jbmc/regression/jbmc/no-main-args-maybe-null2/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.class new file mode 100644 index 00000000000..69f688d31f1 Binary files /dev/null and b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.java new file mode 100644 index 00000000000..956afcb9993 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/Main.java @@ -0,0 +1,16 @@ +public class Main +{ + public static void main(int[] args) + { + assert(args == null); // allowed to fail + assert(args != null); // allowed to fail + if(args != null && args.length > 0) { + try { + int i = args[0]; + } + catch(Exception e) { + assert false; // must hold + } + } + } +} diff --git a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc new file mode 100644 index 00000000000..46abab6236b --- /dev/null +++ b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc @@ -0,0 +1,12 @@ +CORE +Main.class +--function Main.main --java-throw-runtime-exceptions +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Main\.java line 5 function .* bytecode-index 6: FAILURE +assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE +assertion at file Main\.java line 12 function .* bytecode-index 31: SUCCESS +\*\* 2 of .* failed +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.class new file mode 100644 index 00000000000..5a56689bdfb Binary files /dev/null and b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.java new file mode 100644 index 00000000000..7841b610d1f --- /dev/null +++ b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/Main.java @@ -0,0 +1,11 @@ +public class Main +{ + public static void main(String[][] args) + { + assert(args == null || + args.length == 0 || + args[0] == null || + args[0].length == 0 || + args[0][0] != null); // allowed to fail + } +} diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc new file mode 100644 index 00000000000..a631452f5f6 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc @@ -0,0 +1,10 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE +\*\* 1 of .* failed +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.class b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.class new file mode 100644 index 00000000000..ee7b474bda8 Binary files /dev/null and b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.java b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.java new file mode 100644 index 00000000000..cf11207135f --- /dev/null +++ b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/Main.java @@ -0,0 +1,11 @@ +public class Main +{ + public static void main(String[][] args) + { + assert(args == null || + args.length == 0 || + args[0] == null || + args[0].length == 0 || + args[0][0] == null); // allowed to fail + } +} diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc new file mode 100644 index 00000000000..a631452f5f6 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc @@ -0,0 +1,10 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE +\*\* 1 of .* failed +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.class new file mode 100644 index 00000000000..3a9613e9e3c Binary files /dev/null and b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.java new file mode 100644 index 00000000000..f05363fe682 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/Main.java @@ -0,0 +1,9 @@ +public class Main +{ + public static void main(Main[] args) + { + if(args != null && args.length > 0) { + assert(args[0] == null); // allowed to fail + } + } +} diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc new file mode 100644 index 00000000000..145c918788c --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc @@ -0,0 +1,10 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Main\.java line 6 function .* bytecode-index 13: FAILURE +\*\* 1 of .* failed +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.class b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.class new file mode 100644 index 00000000000..1f0d7a7f55d Binary files /dev/null and b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.java b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.java new file mode 100644 index 00000000000..2e8139a9e42 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/Main.java @@ -0,0 +1,9 @@ +public class Main +{ + public static void main(Main[] args) + { + if(args != null && args.length > 0) { + assert(args[0] != null); // allowed to fail + } + } +} diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc new file mode 100644 index 00000000000..145c918788c --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc @@ -0,0 +1,10 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Main\.java line 6 function .* bytecode-index 13: FAILURE +\*\* 1 of .* failed +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main$A.class b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main$A.class new file mode 100644 index 00000000000..47ea25c867b Binary files /dev/null and b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main$A.class differ diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.class b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.class new file mode 100644 index 00000000000..a1dc746c063 Binary files /dev/null and b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.java b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.java new file mode 100644 index 00000000000..44b9b6e14f4 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/Main.java @@ -0,0 +1,18 @@ +public class Main +{ + public static class A { + int x; + } + public A a; + + public static void main(Main[] args) + { + assert(args != null); // allowed to fail + if(args != null && args.length > 0) { + Main m = args[0]; + if(m != null) { + assert(m.a == null); // allowed to fail + } + } + } +} diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc new file mode 100644 index 00000000000..58989b56c0c --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc @@ -0,0 +1,11 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE +assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE +\*\* 2 of .* failed +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main$A.class b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main$A.class new file mode 100644 index 00000000000..47ea25c867b Binary files /dev/null and b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main$A.class differ diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.class b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.class new file mode 100644 index 00000000000..59d39c36a21 Binary files /dev/null and b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.class differ diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.java b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.java new file mode 100644 index 00000000000..fd829647796 --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/Main.java @@ -0,0 +1,18 @@ +public class Main +{ + public static class A { + int x; + } + public A a; + + public static void main(Main[] args) + { + assert(args != null); // allowed to fail + if(args != null && args.length > 0) { + Main m = args[0]; + if(m != null) { + assert(m.a != null); // allowed to fail + } + } + } +} diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc new file mode 100644 index 00000000000..58989b56c0c --- /dev/null +++ b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc @@ -0,0 +1,11 @@ +CORE +Main.class +--function Main.main +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE +assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE +\*\* 2 of .* failed +-- +^warning: ignoring diff --git a/jbmc/regression/strings-smoke-tests/java_append_object/test.desc b/jbmc/regression/strings-smoke-tests/java_append_object/test.desc deleted file mode 100644 index c905a3990f6..00000000000 --- a/jbmc/regression/strings-smoke-tests/java_append_object/test.desc +++ /dev/null @@ -1,10 +0,0 @@ -FUTURE -test_append_object.class ---refine-strings --verbosity 10 --string-max-length 1000 -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -non equal types --- -Issue: diffblue/test-gen#82 diff --git a/jbmc/regression/strings-smoke-tests/java_append_object/test_append_object.class b/jbmc/regression/strings-smoke-tests/java_append_object/test_append_object.class deleted file mode 100644 index ed6942a1fa6..00000000000 Binary files a/jbmc/regression/strings-smoke-tests/java_append_object/test_append_object.class and /dev/null differ diff --git a/jbmc/regression/strings-smoke-tests/java_append_object/test_append_object.java b/jbmc/regression/strings-smoke-tests/java_append_object/test_append_object.java deleted file mode 100644 index 121690451ca..00000000000 --- a/jbmc/regression/strings-smoke-tests/java_append_object/test_append_object.java +++ /dev/null @@ -1,17 +0,0 @@ -public class test_append_object -{ - public static void main(/*String[] args*/) - { - Object diff = "diff"; - Object blue = "blue"; - - StringBuilder buffer = new StringBuilder(); - - buffer.append(diff) - .append(blue); - - String tmp=buffer.toString(); - System.out.println(tmp); - assert tmp.equals("diffblue"); - } -} diff --git a/jbmc/regression/strings-smoke-tests/java_char_array_init/test.desc b/jbmc/regression/strings-smoke-tests/java_char_array_init/test.desc deleted file mode 100644 index c5e050b4850..00000000000 --- a/jbmc/regression/strings-smoke-tests/java_char_array_init/test.desc +++ /dev/null @@ -1,10 +0,0 @@ -FUTURE -test_init.class ---refine-strings --verbosity 10 --string-max-length 1000 -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -non equal types --- -cbmc/test-gen#259 diff --git a/jbmc/regression/strings-smoke-tests/java_char_array_init/test_init.class b/jbmc/regression/strings-smoke-tests/java_char_array_init/test_init.class deleted file mode 100644 index 48075eb9187..00000000000 Binary files a/jbmc/regression/strings-smoke-tests/java_char_array_init/test_init.class and /dev/null differ diff --git a/jbmc/regression/strings-smoke-tests/java_char_array_init/test_init.java b/jbmc/regression/strings-smoke-tests/java_char_array_init/test_init.java deleted file mode 100644 index 8e0f656e3e8..00000000000 --- a/jbmc/regression/strings-smoke-tests/java_char_array_init/test_init.java +++ /dev/null @@ -1,21 +0,0 @@ -public class test_init { - - public static void main(/*String[] argv*/) - { - char [] str = new char[10]; - str[0] = 'H'; - str[1] = 'e'; - str[2] = 'l'; - str[3] = 'l'; - str[4] = 'o'; - String s = new String(str); - String t = new String(str,1,2); - - System.out.println(s.length()); - assert(s.length() == 10); - System.out.println(s); - System.out.println(t); - assert(t.equals("el")); - assert(s.startsWith("Hello")); - } -} diff --git a/jbmc/regression/strings-smoke-tests/java_char_at/test.desc b/jbmc/regression/strings-smoke-tests/java_char_at/test.desc index 5279f32726e..1b0d5054458 100644 --- a/jbmc/regression/strings-smoke-tests/java_char_at/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_char_at/test.desc @@ -1,6 +1,6 @@ CORE test_char_at.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_char_at.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_char_at/test_char_at.java b/jbmc/regression/strings-smoke-tests/java_char_at/test_char_at.java index c91fc7d1cff..7ac598b83f4 100644 --- a/jbmc/regression/strings-smoke-tests/java_char_at/test_char_at.java +++ b/jbmc/regression/strings-smoke-tests/java_char_at/test_char_at.java @@ -1,6 +1,6 @@ public class test_char_at { - public static void main(/*String[] argv*/) { + public static void main() { String s = new String("abc"); assert(org.cprover.CProverString.charAt(s, 2)=='c'); } diff --git a/jbmc/regression/strings-smoke-tests/java_code_point/test.desc b/jbmc/regression/strings-smoke-tests/java_code_point/test.desc index 2c3def77c28..31a1a0340e4 100644 --- a/jbmc/regression/strings-smoke-tests/java_code_point/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_code_point/test.desc @@ -1,6 +1,6 @@ CORE test_code_point.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_code_point.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_code_point/test_code_point.java b/jbmc/regression/strings-smoke-tests/java_code_point/test_code_point.java index ae782ecddfa..dc18dab2853 100644 --- a/jbmc/regression/strings-smoke-tests/java_code_point/test_code_point.java +++ b/jbmc/regression/strings-smoke-tests/java_code_point/test_code_point.java @@ -1,6 +1,6 @@ public class test_code_point { - public static void main(/*String[] argv*/) + public static void main() { String s = "!𐤇𐤄𐤋𐤋𐤅"; assert(org.cprover.CProverString.codePointAt(s, 1) == 67847); diff --git a/jbmc/regression/strings-smoke-tests/java_compare/test.desc b/jbmc/regression/strings-smoke-tests/java_compare/test.desc deleted file mode 100644 index 8f967c8dffb..00000000000 --- a/jbmc/regression/strings-smoke-tests/java_compare/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -test_compare.class ---refine-strings --verbosity 10 --string-max-length 1000 -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -non equal types diff --git a/jbmc/regression/strings-smoke-tests/java_compare/test_compare.class b/jbmc/regression/strings-smoke-tests/java_compare/test_compare.class deleted file mode 100644 index 3a807f4d203..00000000000 Binary files a/jbmc/regression/strings-smoke-tests/java_compare/test_compare.class and /dev/null differ diff --git a/jbmc/regression/strings-smoke-tests/java_compare/test_compare.java b/jbmc/regression/strings-smoke-tests/java_compare/test_compare.java deleted file mode 100644 index c052ed429bd..00000000000 --- a/jbmc/regression/strings-smoke-tests/java_compare/test_compare.java +++ /dev/null @@ -1,9 +0,0 @@ -public class test_compare -{ - public static void main(/*String[] argv*/) - { - String s1 = "ab"; - String s2 = "aa"; - assert(s1.compareTo(s2) == 1); - } -} diff --git a/jbmc/regression/strings-smoke-tests/java_concat/test.desc b/jbmc/regression/strings-smoke-tests/java_concat/test.desc deleted file mode 100644 index 2672b7502d2..00000000000 --- a/jbmc/regression/strings-smoke-tests/java_concat/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -CORE -test_concat.class ---refine-strings --verbosity 10 --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion.1\].* line 10.* SUCCESS$ -^\[.*assertion.2\].* line 11.* FAILURE$ --- -non equal types diff --git a/jbmc/regression/strings-smoke-tests/java_concat/test_concat.class b/jbmc/regression/strings-smoke-tests/java_concat/test_concat.class deleted file mode 100644 index 8802b3957d2..00000000000 Binary files a/jbmc/regression/strings-smoke-tests/java_concat/test_concat.class and /dev/null differ diff --git a/jbmc/regression/strings-smoke-tests/java_concat/test_concat.java b/jbmc/regression/strings-smoke-tests/java_concat/test_concat.java deleted file mode 100644 index 9e861e722bf..00000000000 --- a/jbmc/regression/strings-smoke-tests/java_concat/test_concat.java +++ /dev/null @@ -1,13 +0,0 @@ -public class test_concat -{ - public static void main(/*String[] argv*/) - { - String s = new String("pi"); - int i = s.length(); - String t = new String("ppo"); - String u = s.concat(t); - char c = org.cprover.CProverString.charAt(u, i); - assert(c == 'p'); - assert(c == 'o'); - } -} diff --git a/jbmc/regression/strings-smoke-tests/java_contains/test.desc b/jbmc/regression/strings-smoke-tests/java_contains/test.desc index a0b0afc6933..45af4256612 100644 --- a/jbmc/regression/strings-smoke-tests/java_contains/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_contains/test.desc @@ -1,6 +1,6 @@ CORE test_contains.class ---refine-strings --verbosity 10 --string-max-length 100 +--refine-strings --verbosity 10 --string-max-length 100 --function test_contains.main ^EXIT=0$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_contains/test_string_printable.desc b/jbmc/regression/strings-smoke-tests/java_contains/test_string_printable.desc index 2c0d8942b68..e8b0e0c7c24 100644 --- a/jbmc/regression/strings-smoke-tests/java_contains/test_string_printable.desc +++ b/jbmc/regression/strings-smoke-tests/java_contains/test_string_printable.desc @@ -1,6 +1,6 @@ KNOWNBUG test_contains.class ---refine-strings --verbosity 10 --string-max-length 100 --string-printable +--refine-strings --verbosity 10 --string-max-length 100 --string-printable --function test_contains.main ^EXIT=0$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_delete/test.desc b/jbmc/regression/strings-smoke-tests/java_delete/test.desc deleted file mode 100644 index 7fb479f198b..00000000000 --- a/jbmc/regression/strings-smoke-tests/java_delete/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -test_delete.class ---refine-strings --verbosity 10 --string-max-length 1000 -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -non equal types diff --git a/jbmc/regression/strings-smoke-tests/java_delete/test_delete.class b/jbmc/regression/strings-smoke-tests/java_delete/test_delete.class deleted file mode 100644 index 44a8fdc10db..00000000000 Binary files a/jbmc/regression/strings-smoke-tests/java_delete/test_delete.class and /dev/null differ diff --git a/jbmc/regression/strings-smoke-tests/java_delete/test_delete.java b/jbmc/regression/strings-smoke-tests/java_delete/test_delete.java deleted file mode 100644 index 99298e536c3..00000000000 --- a/jbmc/regression/strings-smoke-tests/java_delete/test_delete.java +++ /dev/null @@ -1,10 +0,0 @@ -public class test_delete -{ - public static void main(/*String[] argv*/) - { - StringBuilder s = new StringBuilder("Abc"); - org.cprover.CProverString.delete(s,1,2); - String str = s.toString(); - assert(str.equals("Ac")); - } -} diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc index 91710ffcf63..4f3d210102a 100644 --- a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc @@ -1,6 +1,6 @@ CORE test_delete_char_at.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_delete_char_at.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java index 2c56fb54b44..3121aab316c 100644 --- a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java +++ b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java @@ -1,6 +1,6 @@ public class test_delete_char_at { - public static void main(/*String[] argv*/) + public static void main() { StringBuilder s = new StringBuilder(); s.append("Abc"); diff --git a/jbmc/regression/strings-smoke-tests/java_empty/test.desc b/jbmc/regression/strings-smoke-tests/java_empty/test.desc deleted file mode 100644 index c1dae21b4d5..00000000000 --- a/jbmc/regression/strings-smoke-tests/java_empty/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -test_empty.class ---refine-strings --verbosity 10 --string-max-length 1000 -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -non equal types diff --git a/jbmc/regression/strings-smoke-tests/java_empty/test_empty.class b/jbmc/regression/strings-smoke-tests/java_empty/test_empty.class deleted file mode 100644 index 8e9a17d387e..00000000000 Binary files a/jbmc/regression/strings-smoke-tests/java_empty/test_empty.class and /dev/null differ diff --git a/jbmc/regression/strings-smoke-tests/java_empty/test_empty.java b/jbmc/regression/strings-smoke-tests/java_empty/test_empty.java deleted file mode 100644 index 47c335e16fa..00000000000 --- a/jbmc/regression/strings-smoke-tests/java_empty/test_empty.java +++ /dev/null @@ -1,8 +0,0 @@ -public class test_empty -{ - public static void main(/*String[] argv*/) - { - String empty = ""; - assert(empty.isEmpty()); - } -} diff --git a/jbmc/regression/strings-smoke-tests/java_endswith/test.desc b/jbmc/regression/strings-smoke-tests/java_endswith/test.desc index 2dec4153ff7..4e04e6544ee 100644 --- a/jbmc/regression/strings-smoke-tests/java_endswith/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_endswith/test.desc @@ -1,6 +1,6 @@ CORE test_endswith.class ---refine-strings --verbosity 10 --string-max-length 100 +--refine-strings --verbosity 10 --string-max-length 100 --function test_endswith.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_endswith/test_endswith.java b/jbmc/regression/strings-smoke-tests/java_endswith/test_endswith.java index f7729ef6a40..6d7ac2191d1 100644 --- a/jbmc/regression/strings-smoke-tests/java_endswith/test_endswith.java +++ b/jbmc/regression/strings-smoke-tests/java_endswith/test_endswith.java @@ -1,6 +1,6 @@ public class test_endswith { - public static void main(/*String[] argv*/) + public static void main() { String s = new String("Abcd"); String suff = "cd"; diff --git a/jbmc/regression/strings-smoke-tests/java_float/test.desc b/jbmc/regression/strings-smoke-tests/java_float/test.desc index e9df3330ee1..c0a002b0ede 100644 --- a/jbmc/regression/strings-smoke-tests/java_float/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_float/test.desc @@ -1,6 +1,6 @@ FUTURE test_float.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_float.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_float/test_float.java b/jbmc/regression/strings-smoke-tests/java_float/test_float.java index d2791d5c343..1e7e78d50c3 100644 --- a/jbmc/regression/strings-smoke-tests/java_float/test_float.java +++ b/jbmc/regression/strings-smoke-tests/java_float/test_float.java @@ -1,6 +1,6 @@ public class test_float { - public static void main(/*String[] arg*/) + public static void main() { float inf = 100.0f / 0.0f; float minus_inf = -100.0f / 0.0f; diff --git a/jbmc/regression/strings-smoke-tests/java_format/test.desc b/jbmc/regression/strings-smoke-tests/java_format/test.desc index e688c95b140..e8e8666c160 100644 --- a/jbmc/regression/strings-smoke-tests/java_format/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_format/test.desc @@ -1,6 +1,6 @@ CORE test.class ---refine-strings --verbosity 10 --string-max-length 20 +--refine-strings --verbosity 10 --string-max-length 20 --function test.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 6.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_format2/test.desc b/jbmc/regression/strings-smoke-tests/java_format2/test.desc index 0ea5e37ca19..f81c6fa17e1 100644 --- a/jbmc/regression/strings-smoke-tests/java_format2/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_format2/test.desc @@ -1,6 +1,6 @@ CORE test.class ---refine-strings --verbosity 10 --string-max-length 20 +--refine-strings --verbosity 10 --string-max-length 20 --function test.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 6.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_format3/test.desc b/jbmc/regression/strings-smoke-tests/java_format3/test.desc index 5aeac5fb776..e0a0de54aa4 100644 --- a/jbmc/regression/strings-smoke-tests/java_format3/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_format3/test.desc @@ -1,6 +1,6 @@ CORE test.class ---refine-strings --verbosity 10 --string-max-length 20 +--refine-strings --verbosity 10 --string-max-length 20 --function test.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 7.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc b/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc index 54d6734c0ba..1392b360f66 100644 --- a/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_hash_code/test.desc @@ -1,6 +1,6 @@ CORE test_hash_code.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_hash_code.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_hash_code/test_hash_code.java b/jbmc/regression/strings-smoke-tests/java_hash_code/test_hash_code.java index d9f42b7ff9d..04c33087e49 100644 --- a/jbmc/regression/strings-smoke-tests/java_hash_code/test_hash_code.java +++ b/jbmc/regression/strings-smoke-tests/java_hash_code/test_hash_code.java @@ -1,6 +1,6 @@ public class test_hash_code { - public static void main(/*String[] argv*/) + public static void main() { String s1 = "ab"; String s2 = "ab"; diff --git a/jbmc/regression/strings-smoke-tests/java_if/test.desc b/jbmc/regression/strings-smoke-tests/java_if/test.desc index a652d884b11..635e7c094cd 100644 --- a/jbmc/regression/strings-smoke-tests/java_if/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_if/test.desc @@ -1,6 +1,6 @@ CORE test.class ---refine-strings --verbosity 10 --string-max-length 100 +--refine-strings --verbosity 10 --string-max-length 100 --function test.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 11.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_index_of/test.desc b/jbmc/regression/strings-smoke-tests/java_index_of/test.desc index e5b6c994424..6fd524b72c1 100644 --- a/jbmc/regression/strings-smoke-tests/java_index_of/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_index_of/test.desc @@ -1,6 +1,6 @@ CORE test_index_of.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_index_of.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_index_of/test_index_of.java b/jbmc/regression/strings-smoke-tests/java_index_of/test_index_of.java index 3568dab9696..d5d9a766b66 100644 --- a/jbmc/regression/strings-smoke-tests/java_index_of/test_index_of.java +++ b/jbmc/regression/strings-smoke-tests/java_index_of/test_index_of.java @@ -1,6 +1,6 @@ public class test_index_of { - public static void main(/*String[] argv*/) + public static void main() { String s = "Abc"; String bc = "bc"; diff --git a/jbmc/regression/strings-smoke-tests/java_index_of2/test.desc b/jbmc/regression/strings-smoke-tests/java_index_of2/test.desc index a3744c3a776..954e794efde 100644 --- a/jbmc/regression/strings-smoke-tests/java_index_of2/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_index_of2/test.desc @@ -1,6 +1,6 @@ CORE test_index_of2.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_index_of2.main ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/strings-smoke-tests/java_index_of_char/test.desc b/jbmc/regression/strings-smoke-tests/java_index_of_char/test.desc index c457e8cd7d0..30ce1a9a702 100644 --- a/jbmc/regression/strings-smoke-tests/java_index_of_char/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_index_of_char/test.desc @@ -1,10 +1,8 @@ CORE test_index_of_char.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_index_of_char.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- non equal types --- -Issue: cbmc/test-gen#77 diff --git a/jbmc/regression/strings-smoke-tests/java_index_of_char/test_index_of_char.java b/jbmc/regression/strings-smoke-tests/java_index_of_char/test_index_of_char.java index 6a5d3d60bd6..ea395edc9f2 100644 --- a/jbmc/regression/strings-smoke-tests/java_index_of_char/test_index_of_char.java +++ b/jbmc/regression/strings-smoke-tests/java_index_of_char/test_index_of_char.java @@ -1,6 +1,6 @@ public class test_index_of_char { - public static void main(/*String[] argv*/) + public static void main() { String s = "Abc"; char c = 'c'; diff --git a/jbmc/regression/strings-smoke-tests/java_insert_char/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_char/test.desc index 3281b3d629b..bcae9bf0ea6 100644 --- a/jbmc/regression/strings-smoke-tests/java_insert_char/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_insert_char/test.desc @@ -1,6 +1,6 @@ CORE test_insert_char.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_insert_char.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_insert_char/test_insert_char.java b/jbmc/regression/strings-smoke-tests/java_insert_char/test_insert_char.java index 940292296f1..068b0ab5acc 100644 --- a/jbmc/regression/strings-smoke-tests/java_insert_char/test_insert_char.java +++ b/jbmc/regression/strings-smoke-tests/java_insert_char/test_insert_char.java @@ -1,6 +1,6 @@ public class test_insert_char { - public static void main(/*String[] argv*/) + public static void main() { StringBuilder sb = new StringBuilder("ac"); org.cprover.CProverString.insert(sb, 1, 'b'); diff --git a/jbmc/regression/strings-smoke-tests/java_insert_int/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_int/test.desc deleted file mode 100644 index 66c81170630..00000000000 --- a/jbmc/regression/strings-smoke-tests/java_insert_int/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -test_insert_int.class ---refine-strings --verbosity 10 --string-max-length 1000 -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -non equal types diff --git a/jbmc/regression/strings-smoke-tests/java_insert_int/test_insert_int.class b/jbmc/regression/strings-smoke-tests/java_insert_int/test_insert_int.class deleted file mode 100644 index 2ba5491c536..00000000000 Binary files a/jbmc/regression/strings-smoke-tests/java_insert_int/test_insert_int.class and /dev/null differ diff --git a/jbmc/regression/strings-smoke-tests/java_insert_int/test_insert_int.java b/jbmc/regression/strings-smoke-tests/java_insert_int/test_insert_int.java deleted file mode 100644 index e480683821f..00000000000 --- a/jbmc/regression/strings-smoke-tests/java_insert_int/test_insert_int.java +++ /dev/null @@ -1,10 +0,0 @@ -public class test_insert_int -{ - public static void main(/*String[] argv*/) - { - StringBuilder sb = new StringBuilder("ac"); - org.cprover.CProverString.insert(sb, 1, 42); - String s = sb.toString(); - assert(s.equals("a42c")); - } -} diff --git a/jbmc/regression/strings-smoke-tests/java_insert_multiple/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_multiple/test.desc index 5b77efb0d46..d36dc796a31 100644 --- a/jbmc/regression/strings-smoke-tests/java_insert_multiple/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_insert_multiple/test.desc @@ -1,6 +1,6 @@ CORE test_insert_multiple.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_insert_multiple.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java b/jbmc/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java index b505e24020e..c74177eda80 100644 --- a/jbmc/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java +++ b/jbmc/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java @@ -1,6 +1,6 @@ public class test_insert_multiple { - public static void main(/*String[] argv*/) + public static void main() { StringBuilder sb = new StringBuilder("ad"); org.cprover.CProverString.insert(sb, 1, 'c'); diff --git a/jbmc/regression/strings-smoke-tests/java_insert_string/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_string/test.desc index 93596bf62ac..066e26a74b2 100644 --- a/jbmc/regression/strings-smoke-tests/java_insert_string/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_insert_string/test.desc @@ -1,6 +1,6 @@ CORE test_insert_string.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_insert_string.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_insert_string/test_insert_string.java b/jbmc/regression/strings-smoke-tests/java_insert_string/test_insert_string.java index 547b89ae569..9053fa97d9d 100644 --- a/jbmc/regression/strings-smoke-tests/java_insert_string/test_insert_string.java +++ b/jbmc/regression/strings-smoke-tests/java_insert_string/test_insert_string.java @@ -1,6 +1,6 @@ public class test_insert_string { - public static void main(/*String[] argv*/) + public static void main() { StringBuilder sb = new StringBuilder("ad"); org.cprover.CProverString.insert(sb, 1, "bc"); diff --git a/jbmc/regression/strings-smoke-tests/java_intern/test.desc b/jbmc/regression/strings-smoke-tests/java_intern/test.desc index 05b26307bb2..778cfffeae4 100644 --- a/jbmc/regression/strings-smoke-tests/java_intern/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_intern/test.desc @@ -1,6 +1,6 @@ CORE test_intern.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_intern.main ^EXIT=0$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_intern/test_intern.java b/jbmc/regression/strings-smoke-tests/java_intern/test_intern.java index 7f9d5283597..b8abb9f1f2c 100644 --- a/jbmc/regression/strings-smoke-tests/java_intern/test_intern.java +++ b/jbmc/regression/strings-smoke-tests/java_intern/test_intern.java @@ -1,6 +1,6 @@ public class test_intern { - public static void main(/*String[] argv*/) + public static void main() { String s1 = "abc"; String s3 = "abc"; diff --git a/jbmc/regression/strings-smoke-tests/java_last_index_of/test.desc b/jbmc/regression/strings-smoke-tests/java_last_index_of/test.desc index 9fd0a299a7c..917218b59dd 100644 --- a/jbmc/regression/strings-smoke-tests/java_last_index_of/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_last_index_of/test.desc @@ -1,6 +1,6 @@ CORE test_last_index_of.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_last_index_of.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java b/jbmc/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java index 59b9f5ab36d..c4aecdfc718 100644 --- a/jbmc/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java +++ b/jbmc/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java @@ -1,6 +1,6 @@ public class test_last_index_of { - public static void main(/*String[] argv*/) + public static void main() { String s = "abcab"; String ab = "ab"; diff --git a/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test.desc b/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test.desc index a1ddc2cf440..451966cbac1 100644 --- a/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test.desc @@ -1,6 +1,6 @@ CORE test_last_index_of_char.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_last_index_of_char.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test_last_index_of_char.java b/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test_last_index_of_char.java index 029d59c9d68..fec963b8bf2 100644 --- a/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test_last_index_of_char.java +++ b/jbmc/regression/strings-smoke-tests/java_last_index_of_char/test_last_index_of_char.java @@ -1,6 +1,6 @@ public class test_last_index_of_char { - public static void main(/*String[] argv*/) + public static void main() { String s = "abcab"; int n = s.lastIndexOf('a'); diff --git a/jbmc/regression/strings-smoke-tests/java_length/test.desc b/jbmc/regression/strings-smoke-tests/java_length/test.desc index 59184450019..f3a7b3e99c7 100644 --- a/jbmc/regression/strings-smoke-tests/java_length/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_length/test.desc @@ -1,6 +1,6 @@ CORE test_length.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_length.main ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/strings-smoke-tests/java_length/test_length.java b/jbmc/regression/strings-smoke-tests/java_length/test_length.java index 620bdc448e9..ce844e67ea7 100644 --- a/jbmc/regression/strings-smoke-tests/java_length/test_length.java +++ b/jbmc/regression/strings-smoke-tests/java_length/test_length.java @@ -1,6 +1,6 @@ public class test_length { - public static void main(/*String[] argv*/) + public static void main() { String s = new String("Abc"); int l = s.length(); diff --git a/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc b/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc index f95b66184a8..4f888659004 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc @@ -1,6 +1,6 @@ CORE Test3.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test3.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 7.* FAILURE$ diff --git a/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc b/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc index ba11fa1f7e5..cae6c9a525b 100644 --- a/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc @@ -1,6 +1,6 @@ CORE test_replace_char.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_replace_char.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_replace_char/test_replace_char.java b/jbmc/regression/strings-smoke-tests/java_replace_char/test_replace_char.java index 82a023924e2..0059c309ebe 100644 --- a/jbmc/regression/strings-smoke-tests/java_replace_char/test_replace_char.java +++ b/jbmc/regression/strings-smoke-tests/java_replace_char/test_replace_char.java @@ -1,6 +1,6 @@ public class test_replace_char { - public static void main(/*String[] argv*/) + public static void main() { String s = new String("abcabd"); String t = s.replace('b','m'); diff --git a/jbmc/regression/strings-smoke-tests/java_set_char_at/test.desc b/jbmc/regression/strings-smoke-tests/java_set_char_at/test.desc index bfb3be131a5..0adb430c3b3 100644 --- a/jbmc/regression/strings-smoke-tests/java_set_char_at/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_set_char_at/test.desc @@ -1,6 +1,6 @@ CORE test_set_char_at.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_set_char_at.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java b/jbmc/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java index 9e67eba0de7..7151c9ba177 100644 --- a/jbmc/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java +++ b/jbmc/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java @@ -1,6 +1,6 @@ public class test_set_char_at { - public static void main(/*String[] argv*/) + public static void main() { String s = new String("Abc"); char c = org.cprover.CProverString.charAt(s, 1); diff --git a/jbmc/regression/strings-smoke-tests/java_set_length/test.desc b/jbmc/regression/strings-smoke-tests/java_set_length/test.desc index 92b178f222a..21dd8d95a49 100644 --- a/jbmc/regression/strings-smoke-tests/java_set_length/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_set_length/test.desc @@ -1,6 +1,6 @@ CORE test_set_length.class ---refine-strings --verbosity 10 --string-max-length 100 +--refine-strings --verbosity 10 --string-max-length 100 --function test_set_length.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_set_length/test_set_length.java b/jbmc/regression/strings-smoke-tests/java_set_length/test_set_length.java index 5894b27beeb..37c60a9912a 100644 --- a/jbmc/regression/strings-smoke-tests/java_set_length/test_set_length.java +++ b/jbmc/regression/strings-smoke-tests/java_set_length/test_set_length.java @@ -1,6 +1,6 @@ public class test_set_length { - public static void main(/*String[] argv*/) + public static void main() { StringBuilder s = new StringBuilder("abc"); s.setLength(10); diff --git a/jbmc/regression/strings-smoke-tests/java_starts_with/test.desc b/jbmc/regression/strings-smoke-tests/java_starts_with/test.desc index 96348e08f11..5a0ca5ea703 100644 --- a/jbmc/regression/strings-smoke-tests/java_starts_with/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_starts_with/test.desc @@ -1,6 +1,6 @@ CORE test_starts_with.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_starts_with.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_starts_with/test_starts_with.java b/jbmc/regression/strings-smoke-tests/java_starts_with/test_starts_with.java index aba79d846c0..def31ed6709 100644 --- a/jbmc/regression/strings-smoke-tests/java_starts_with/test_starts_with.java +++ b/jbmc/regression/strings-smoke-tests/java_starts_with/test_starts_with.java @@ -1,6 +1,6 @@ public class test_starts_with { - public static void main(/*String[] argv*/) + public static void main() { String s = new String("Abcd"); String pref = "Ab"; diff --git a/jbmc/regression/strings-smoke-tests/java_string_builder_length/test.desc b/jbmc/regression/strings-smoke-tests/java_string_builder_length/test.desc index 8fbbb04690c..2debae07cf9 100644 --- a/jbmc/regression/strings-smoke-tests/java_string_builder_length/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_string_builder_length/test.desc @@ -1,6 +1,6 @@ CORE test_sb_length.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_sb_length.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_string_builder_length/test_sb_length.java b/jbmc/regression/strings-smoke-tests/java_string_builder_length/test_sb_length.java index b616749ffb4..e09d8807949 100644 --- a/jbmc/regression/strings-smoke-tests/java_string_builder_length/test_sb_length.java +++ b/jbmc/regression/strings-smoke-tests/java_string_builder_length/test_sb_length.java @@ -1,6 +1,6 @@ public class test_sb_length { - public static void main(/*String[] argv*/) + public static void main() { StringBuilder x = new StringBuilder("abc"); x.append("de"); diff --git a/jbmc/regression/strings-smoke-tests/java_subsequence/test.desc b/jbmc/regression/strings-smoke-tests/java_subsequence/test.desc index b0949a841ea..e16da196007 100644 --- a/jbmc/regression/strings-smoke-tests/java_subsequence/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_subsequence/test.desc @@ -1,6 +1,6 @@ CORE test_subsequence.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_subsequence.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_subsequence/test_subsequence.java b/jbmc/regression/strings-smoke-tests/java_subsequence/test_subsequence.java index 6fdc3e6735e..0a6c18176da 100644 --- a/jbmc/regression/strings-smoke-tests/java_subsequence/test_subsequence.java +++ b/jbmc/regression/strings-smoke-tests/java_subsequence/test_subsequence.java @@ -1,6 +1,6 @@ public class test_subsequence { - public static void main(/*String[] argv*/) + public static void main() { String abcdef = "AbcDef"; CharSequence cde = org.cprover.CProverString.subSequence(abcdef,2,5); diff --git a/jbmc/regression/strings-smoke-tests/java_substring/test.desc b/jbmc/regression/strings-smoke-tests/java_substring/test.desc index 762b0237086..5787d80275d 100644 --- a/jbmc/regression/strings-smoke-tests/java_substring/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_substring/test.desc @@ -1,6 +1,6 @@ CORE test_substring.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_substring.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/strings-smoke-tests/java_substring/test_substring.java b/jbmc/regression/strings-smoke-tests/java_substring/test_substring.java index e94ee9c51cb..88278f455b9 100644 --- a/jbmc/regression/strings-smoke-tests/java_substring/test_substring.java +++ b/jbmc/regression/strings-smoke-tests/java_substring/test_substring.java @@ -1,6 +1,6 @@ public class test_substring { - public static void main(/*String[] argv*/) + public static void main() { String abcdef = "AbcDef"; String cde = org.cprover.CProverString.substring(abcdef, 2,5); diff --git a/jbmc/regression/strings-smoke-tests/java_trim/test.desc b/jbmc/regression/strings-smoke-tests/java_trim/test.desc index 94142169895..d60e82f050e 100644 --- a/jbmc/regression/strings-smoke-tests/java_trim/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_trim/test.desc @@ -1,6 +1,6 @@ CORE test_trim.class ---refine-strings --verbosity 10 --string-max-length 100 +--refine-strings --verbosity 10 --string-max-length 100 --function test_trim.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 6.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_trim/test_trim.java b/jbmc/regression/strings-smoke-tests/java_trim/test_trim.java index 20dd7ba2796..679a0f821e9 100644 --- a/jbmc/regression/strings-smoke-tests/java_trim/test_trim.java +++ b/jbmc/regression/strings-smoke-tests/java_trim/test_trim.java @@ -1,6 +1,6 @@ public class test_trim { - public static void main(/*String[] argv*/) + public static void main() { String empty = " "; assert(empty.trim().isEmpty()); diff --git a/jbmc/regression/strings-smoke-tests/max_input_length/Test.class b/jbmc/regression/strings-smoke-tests/max_input_length/Test.class index 37d68870ec9..d07682d2cf6 100644 Binary files a/jbmc/regression/strings-smoke-tests/max_input_length/Test.class and b/jbmc/regression/strings-smoke-tests/max_input_length/Test.class differ diff --git a/jbmc/regression/strings-smoke-tests/max_input_length/Test.java b/jbmc/regression/strings-smoke-tests/max_input_length/Test.java index 9c6e8839f58..308da33a348 100644 --- a/jbmc/regression/strings-smoke-tests/max_input_length/Test.java +++ b/jbmc/regression/strings-smoke-tests/max_input_length/Test.java @@ -3,7 +3,7 @@ public static void main(String s) { // This prevent anything from happening if we were to add a constraints on strings // being smaller than 40 String t = new String("0123456789012345678901234567890123456789"); - if (s.length() >= 30) + if (s != null && s.length() >= 30) // This should not happen when string-max-input length is smaller // than 30 assert false; diff --git a/jbmc/regression/strings-smoke-tests/max_input_length/test1.desc b/jbmc/regression/strings-smoke-tests/max_input_length/test1.desc index c5252f6c564..0943fca690c 100644 --- a/jbmc/regression/strings-smoke-tests/max_input_length/test1.desc +++ b/jbmc/regression/strings-smoke-tests/max_input_length/test1.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 31 +--refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 31 --function Test.main ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/strings-smoke-tests/max_input_length/test2.desc b/jbmc/regression/strings-smoke-tests/max_input_length/test2.desc index 0edaf226ccc..307bc7db2fc 100644 --- a/jbmc/regression/strings-smoke-tests/max_input_length/test2.desc +++ b/jbmc/regression/strings-smoke-tests/max_input_length/test2.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 20 +--refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 20 --function Test.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/src/java_bytecode/convert_java_nondet.cpp b/jbmc/src/java_bytecode/convert_java_nondet.cpp index 735ba4400ba..acc3d9bff51 100644 --- a/jbmc/src/java_bytecode/convert_java_nondet.cpp +++ b/jbmc/src/java_bytecode/convert_java_nondet.cpp @@ -36,7 +36,7 @@ static goto_programt::targett insert_nondet_init_code( const goto_programt::targett &target, symbol_table_baset &symbol_table, message_handlert &message_handler, - const object_factory_parameterst &object_factory_parameters, + object_factory_parameterst object_factory_parameters, const irep_idt &mode) { // Return if the instruction isn't an assignment @@ -76,7 +76,8 @@ static goto_programt::targett insert_nondet_init_code( } // Check whether the nondet object may be null - const auto nullable=to_side_effect_expr_nondet(side_effect).get_nullable(); + if(!to_side_effect_expr_nondet(side_effect).get_nullable()) + object_factory_parameters.max_nonnull_tree_depth = 1; // Get the symbol to nondet-init const auto source_loc=target->source_location; @@ -92,7 +93,6 @@ static goto_programt::targett insert_nondet_init_code( source_loc, true, allocation_typet::DYNAMIC, - nullable, object_factory_parameters, update_in_placet::NO_UPDATE_IN_PLACE); diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 7d250b92ec7..a6fc3018f7e 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -22,6 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_string_literals.h" #include "java_utils.h" +#define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V" + static void create_initialize(symbol_table_baset &symbol_table) { // If __CPROVER_initialize already exists, replace it. It may already exist @@ -217,6 +219,10 @@ static void java_static_lifetime_init( if(allow_null && is_non_null_library_global(nameid)) allow_null = false; } + object_factory_parameterst parameters = object_factory_parameters; + if(!allow_null) + parameters.max_nonnull_tree_depth = 1; + gen_nondet_init( sym.symbol_expr(), code_block, @@ -224,8 +230,7 @@ static void java_static_lifetime_init( source_location, false, allocation_typet::GLOBAL, - allow_null, - object_factory_parameters, + parameters, pointer_type_selector, update_in_placet::NO_UPDATE_IN_PLACE); } @@ -239,6 +244,27 @@ static void java_static_lifetime_init( } } +/// Checks whether the given symbol is a valid java main method +/// i.e. it must be public, static, called 'main' and +/// have signature void(String[]) +/// \param function: the function symbol +/// \return true if it is a valid main method +bool is_java_main(const symbolt &function) +{ + bool named_main = has_suffix(id2string(function.name), JAVA_MAIN_METHOD); + const code_typet &function_type = to_code_type(function.type); + const typet &string_array_type = java_type_from_string("[Ljava/lang/String;"); + // checks whether the function is static and has a single String[] parameter + bool is_static = !function_type.has_this(); + // this should be implied by the signature + const code_typet::parameterst ¶meters = function_type.parameters(); + bool has_correct_type = function_type.return_type().id() == ID_empty && + parameters.size() == 1 && + parameters[0].type().full_eq(string_array_type); + bool public_access = function_type.get(ID_access) == ID_public; + return named_main && is_static && has_correct_type && public_access; +} + /// Extends \p init_code with code that allocates the objects used as test /// arguments for the function under test (\p function) and /// non-deterministically initializes them. @@ -265,22 +291,7 @@ exprt::operandst java_build_arguments( // certain method arguments cannot be allowed to be null, we set the following // variable to true iff the method under test is the "main" method, which will // be called (by the jvm) with arguments that are never null - bool is_default_entry_point(config.main.empty()); - bool is_main=is_default_entry_point; - - // if walks like a duck and quacks like a duck, it is a duck! - if(!is_main) - { - bool named_main=has_suffix(config.main, ".main"); - const typet &string_array_type= - java_type_from_string("[Ljava.lang.String;"); - bool has_correct_type= - to_code_type(function.type).return_type().id()==ID_empty && - (!to_code_type(function.type).has_this()) && - parameters.size()==1 && - parameters[0].type().full_eq(string_array_type); - is_main=(named_main && has_correct_type); - } + bool is_main = is_java_main(function); // we iterate through all the parameters of the function under test, allocate // an object for that parameter (recursively allocating other objects @@ -297,10 +308,14 @@ exprt::operandst java_build_arguments( // be null bool is_this=(param_number==0) && parameters[param_number].get_this(); - bool allow_null= - !assume_init_pointers_not_null && !is_main && !is_this; - object_factory_parameterst parameters = object_factory_parameters; + // only pointer must be non-null + if(assume_init_pointers_not_null || is_this) + parameters.max_nonnull_tree_depth = 1; + // in main() also the array elements of the argument must be non-null + if(is_main) + parameters.max_nonnull_tree_depth = 2; + parameters.function_id = goto_functionst::entry_point(); // generate code to allocate and non-deterministicaly initialize the @@ -309,7 +324,6 @@ exprt::operandst java_build_arguments( p.type(), base_name, init_code, - allow_null, symbol_table, parameters, allocation_typet::LOCAL, @@ -447,37 +461,25 @@ main_function_resultt get_main_symbol( // are we given a main class? if(main_class.empty()) - return main_function_resultt::NotFound; // silently ignore - - std::string entry_method = id2string(main_class) + ".main"; - - std::string prefix="java::"+entry_method+":"; - - // look it up - std::set matches; - - for(const auto &named_symbol : symbol_table.symbols) { - if(named_symbol.second.type.id() == ID_code - && has_prefix(id2string(named_symbol.first), prefix)) - { - matches.insert(&named_symbol.second); - } + // no, but we allow this situation to output symbol table, + // goto functions, etc + return main_function_resultt::NotFound; } - if(matches.empty()) - // Not found, silently ignore - return main_function_resultt::NotFound; + std::string entry_method = + "java::" + id2string(main_class) + "." + JAVA_MAIN_METHOD; + const symbolt *symbol = symbol_table.lookup(entry_method); - if(matches.size() > 1) + // has the class a correct main method? + if(!symbol || !is_java_main(*symbol)) { - message.error() - << "main method in `" << main_class - << "' is ambiguous" << messaget::eom; - return main_function_resultt::Error; // give up with error, no main + // no, but we allow this situation to output symbol table, + // goto functions, etc + return main_function_resultt::NotFound; } - return **matches.begin(); // Return found function + return *symbol; } } diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 3f5a95f879d..29935ebedfc 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -113,7 +113,6 @@ class java_object_factoryt allocation_typet alloc_type, bool override_, const typet &override_type, - bool allow_null, size_t depth, update_in_placet); @@ -124,7 +123,6 @@ class java_object_factoryt const irep_idt &class_identifier, allocation_typet alloc_type, const pointer_typet &pointer_type, - bool allow_null, size_t depth, const update_in_placet &update_in_place); @@ -434,7 +432,6 @@ void java_object_factoryt::gen_pointer_target_init( alloc_type, false, // override typet(), // override type immaterial - true, // allow_null always enabled in sub-objects depth+1, update_in_place); } @@ -686,7 +683,8 @@ static bool add_nondet_string_pointer_initialization( const struct_typet &struct_type = to_struct_type(ns.follow(to_symbol_type(obj.type()))); - if(!struct_type.has_component("data") || !struct_type.has_component("length")) + // if no String model is loaded then we cannot construct a String object + if(struct_type.get_bool(ID_incomplete_class)) return true; const exprt malloc_site = allocate_dynamic_object_with_decl( @@ -717,11 +715,6 @@ static bool add_nondet_string_pointer_initialization( /// others. /// \param alloc_type: /// Allocation type (global, local or dynamic) -/// \param allow_null: -/// true iff the the non-det initialization code is allowed to set null as a -/// value to the pointer \p expr; note that the current value of allow_null is -/// _not_ inherited by subsequent recursive calls; those will always be -/// authorized to assign null to a pointer /// \param depth: /// Number of times that a pointer has been dereferenced from the root of the /// object tree that we are initializing. @@ -738,7 +731,6 @@ void java_object_factoryt::gen_nondet_pointer_init( const irep_idt &class_identifier, allocation_typet alloc_type, const pointer_typet &pointer_type, - bool allow_null, size_t depth, const update_in_placet &update_in_place) { @@ -843,7 +835,6 @@ void java_object_factoryt::gen_nondet_pointer_init( // Note string-type-specific initialization might fail, e.g. if java.lang.CharSequence does not // have the expected fields (typically this happens if --refine-strings was not passed). In this // case we fall back to normal pointer target init. - bool string_init_succeeded = false; if(java_string_library_preprocesst::implements_java_char_sequence_pointer( @@ -873,10 +864,12 @@ void java_object_factoryt::gen_nondet_pointer_init( auto set_null_inst=get_null_assignment(expr, pointer_type); + const bool allow_null = + depth > object_factory_parameters.max_nonnull_tree_depth; + // Alternatively, if this is a void* we *must* initialise with null: // (This can currently happen for some cases of #exception_value) - bool must_be_null= - subtype==empty_typet(); + bool must_be_null = subtype == empty_typet(); if(must_be_null) { @@ -977,7 +970,6 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init( alloc_type, false, // override typet(), // override_type - true, // allow_null depth, update_in_placet::NO_UPDATE_IN_PLACE); @@ -1099,7 +1091,6 @@ void java_object_factoryt::gen_nondet_struct_init( alloc_type, false, // override typet(), // override_type - true, // allow_null always true for sub-objects depth, substruct_in_place); } @@ -1149,9 +1140,6 @@ void java_object_factoryt::gen_nondet_struct_init( /// If true, initialize with `override_type` instead of `expr.type()`. Used at /// the moment for reference arrays, which are implemented as void* arrays but /// should be init'd as their true type with appropriate casts. -/// \param allow_null: -/// True iff the the non-det initialization code is allowed to set null as a -/// value to a pointer. /// \param depth: /// Number of times that a pointer has been dereferenced from the root of the /// object tree that we are initializing. @@ -1171,7 +1159,6 @@ void java_object_factoryt::gen_nondet_init( allocation_typet alloc_type, bool override_, const typet &override_type, - bool allow_null, size_t depth, update_in_placet update_in_place) { @@ -1198,7 +1185,6 @@ void java_object_factoryt::gen_nondet_init( class_identifier, alloc_type, pointer_type, - allow_null, depth, update_in_place); } @@ -1278,14 +1264,13 @@ void java_object_factoryt::allocate_nondet_length_array( gen_nondet_init( assignments, length_sym_expr, - false, // is_sub + false, // is_sub irep_idt(), - false, // skip_classid + false, // skip_classid allocation_typet::LOCAL, // immaterial, type is primitive - false, // override - typet(), // override type is immaterial - false, // allow_null - 0, // depth is immaterial + false, // override + typet(), // override type is immaterial + 0, // depth is immaterial, always non-null update_in_placet::NO_UPDATE_IN_PLACE); // Insert assumptions to bound its length: @@ -1436,7 +1421,6 @@ void java_object_factoryt::gen_nondet_array_init( allocation_typet::DYNAMIC, true, // override element_type, - true, // allow_null depth, child_update_in_place); @@ -1486,7 +1470,6 @@ exprt object_factory( const typet &type, const irep_idt base_name, code_blockt &init_code, - bool allow_null, symbol_table_baset &symbol_table, const object_factory_parameterst ¶meters, allocation_typet alloc_type, @@ -1522,14 +1505,13 @@ exprt object_factory( state.gen_nondet_init( assignments, object, - false, // is_sub - "", // class_identifier - false, // skip_classid + false, // is_sub + "", // class_identifier + false, // skip_classid alloc_type, false, // override typet(), // override_type is immaterial - allow_null, - 0, // initial depth + 1, // initial depth update_in_placet::NO_UPDATE_IN_PLACE); declare_created_symbols(symbols_created, loc, init_code); @@ -1538,7 +1520,7 @@ exprt object_factory( return object; } -/// Initializes a primitive-typed or referece-typed object tree rooted at +/// Initializes a primitive-typed or reference-typed object tree rooted at /// `expr`, allocating child objects as necessary and nondet-initializing their /// members, or if MAY_ or MUST_UPDATE_IN_PLACE is set, re-initializing /// already-allocated objects. @@ -1560,13 +1542,6 @@ exprt object_factory( /// \param alloc_type: /// Allocate new objects as global objects (GLOBAL) or as local variables /// (LOCAL) or using malloc (DYNAMIC). -/// \param allow_null: -/// When \p expr is a pointer, the non-det initializing code will -/// unconditionally set \p expr to a non-null object iff \p allow_null is -/// true. Note that other references down the object hierarchy *can* be null -/// when \p allow_null is false (as this parameter is not inherited by -/// subsequent recursive calls). Has no effect when \p expr is not -/// pointer-typed. /// \param object_factory_parameters: /// Parameters for the generation of non deterministic objects. /// \param pointer_type_selector: @@ -1587,7 +1562,6 @@ void gen_nondet_init( const source_locationt &loc, bool skip_classid, allocation_typet alloc_type, - bool allow_null, const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place) @@ -1604,14 +1578,13 @@ void gen_nondet_init( state.gen_nondet_init( assignments, expr, - false, // is_sub - "", // class_identifier + false, // is_sub + "", // class_identifier skip_classid, alloc_type, false, // override typet(), // override_type is immaterial - allow_null, - 0, // initial depth + 1, // initial depth update_in_place); declare_created_symbols(symbols_created, loc, init_code); @@ -1624,7 +1597,6 @@ exprt object_factory( const typet &type, const irep_idt base_name, code_blockt &init_code, - bool allow_null, symbol_tablet &symbol_table, const object_factory_parameterst &object_factory_parameters, allocation_typet alloc_type, @@ -1635,7 +1607,6 @@ exprt object_factory( type, base_name, init_code, - allow_null, symbol_table, object_factory_parameters, alloc_type, @@ -1651,7 +1622,6 @@ void gen_nondet_init( const source_locationt &loc, bool skip_classid, allocation_typet alloc_type, - bool allow_null, const object_factory_parameterst &object_factory_parameters, update_in_placet update_in_place) { @@ -1663,7 +1633,6 @@ void gen_nondet_init( loc, skip_classid, alloc_type, - allow_null, object_factory_parameters, pointer_type_selector, update_in_place); diff --git a/jbmc/src/java_bytecode/java_object_factory.h b/jbmc/src/java_bytecode/java_object_factory.h index 0d8ec5f0995..4c69f282bea 100644 --- a/jbmc/src/java_bytecode/java_object_factory.h +++ b/jbmc/src/java_bytecode/java_object_factory.h @@ -90,7 +90,6 @@ exprt object_factory( const typet &type, const irep_idt base_name, code_blockt &init_code, - bool allow_null, symbol_table_baset &symbol_table, const object_factory_parameterst ¶meters, allocation_typet alloc_type, @@ -101,7 +100,6 @@ exprt object_factory( const typet &type, const irep_idt base_name, code_blockt &init_code, - bool allow_null, symbol_tablet &symbol_table, const object_factory_parameterst &object_factory_parameters, allocation_typet alloc_type, @@ -121,7 +119,6 @@ void gen_nondet_init( const source_locationt &loc, bool skip_classid, allocation_typet alloc_type, - bool allow_null, const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place); @@ -133,7 +130,6 @@ void gen_nondet_init( const source_locationt &loc, bool skip_classid, allocation_typet alloc_type, - bool allow_null, const object_factory_parameterst &object_factory_parameters, update_in_placet update_in_place); diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index 9cc276f6400..a5dfd289cfa 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -781,6 +781,12 @@ codet stub_global_initializer_factoryt::get_stub_initializer_body( { const symbol_exprt new_global_symbol = symbol_table.lookup_ref(it->second).symbol_expr(); + + parameters.max_nonnull_tree_depth = + is_non_null_library_global(it->second) + ? object_factory_parameters.max_nonnull_tree_depth + 1 + : object_factory_parameters.max_nonnull_tree_depth; + gen_nondet_init( new_global_symbol, static_init_body, @@ -788,7 +794,6 @@ codet stub_global_initializer_factoryt::get_stub_initializer_body( source_locationt(), false, allocation_typet::DYNAMIC, - !is_non_null_library_global(it->second), parameters, pointer_type_selector, update_in_placet::NO_UPDATE_IN_PLACE); diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index dc838eadd8d..7970f8a9d1d 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -256,7 +256,7 @@ std::string erase_type_arguments(const std::string &src) /// Returns the full class name, skipping over the generics. /// \param src: a type descriptor or signature /// 1. Signature: Lcom/package/OuterClass.Inner; -/// 2. Descriptor: Lcom.pacakge.OuterClass$Inner; +/// 2. Descriptor: Lcom.package.OuterClass$Inner; /// \return The full name of the class like com.package.OuterClass.Inner (for /// both examples). std::string gather_full_class_name(const std::string &src) diff --git a/jbmc/src/java_bytecode/object_factory_parameters.h b/jbmc/src/java_bytecode/object_factory_parameters.h index 17b838242c2..13eb09bf030 100644 --- a/jbmc/src/java_bytecode/object_factory_parameters.h +++ b/jbmc/src/java_bytecode/object_factory_parameters.h @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5 #define MAX_NONDET_STRING_LENGTH std::numeric_limits::max() #define MAX_NONDET_TREE_DEPTH 5 +#define MAX_NONNULL_TREE_DEPTH 0 struct object_factory_parameterst final { @@ -34,6 +35,18 @@ struct object_factory_parameterst final /// such depth becomes >= than this maximum value. size_t max_nondet_tree_depth=MAX_NONDET_TREE_DEPTH; + /// To force a certain depth of non-null objects. + /// The default is that objects are 'maybe null' up to the nondet tree depth. + /// Examples: + /// * max_nondet_tree_depth=0, max_nonnull_tree_depth irrelevant + /// pointer initialized to null + /// * max_nondet_tree_depth=n, max_nonnull_tree_depth=0 + /// pointer and children up to depth n maybe-null, beyond n null + /// * max_nondet_tree_depth=n >=m, max_nonnull_tree_depth=m + /// pointer and children up to depth m initialized to non-null, + /// children up to n maybe-null, beyond n null + size_t max_nonnull_tree_depth = MAX_NONNULL_TREE_DEPTH; + /// Force string content to be ASCII printable characters when set to true. bool string_printable = false; diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp index 8bd484ed7e5..16a52370fee 100644 --- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp +++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp @@ -106,6 +106,10 @@ void java_simple_method_stubst::create_method_stub_at( if(is_constructor) to_init = dereference_exprt(to_init, expected_base); + object_factory_parameterst parameters = object_factory_parameters; + if(assume_non_null) + parameters.max_nonnull_tree_depth = 1; + // Generate new instructions. code_blockt new_instructions; gen_nondet_init( @@ -115,8 +119,7 @@ void java_simple_method_stubst::create_method_stub_at( loc, is_constructor, allocation_typet::DYNAMIC, - !assume_non_null, - object_factory_parameters, + parameters, update_in_place ? update_in_placet::MUST_UPDATE_IN_PLACE : update_in_placet::NO_UPDATE_IN_PLACE); @@ -189,6 +192,10 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol) const exprt &to_return = to_return_symbol.symbol_expr(); if(to_return_symbol.type.id() != ID_pointer) { + object_factory_parameterst parameters = object_factory_parameters; + if(assume_non_null) + parameters.max_nonnull_tree_depth = 1; + gen_nondet_init( to_return, new_instructions, @@ -196,8 +203,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol) source_locationt(), false, allocation_typet::LOCAL, // Irrelevant as type is primitive - !assume_non_null, - object_factory_parameters, + parameters, update_in_placet::NO_UPDATE_IN_PLACE); } else