Merge pull request diffblue#1768 from peterschrammel/fix-java-main-harness

Fix java harness for main()

Author: peterschrammel

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$

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$

jbmc/regression/jbmc-strings/java_append_string/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$

jbmc/regression/jbmc-strings/java_append_string/test_append_string.class

@@ -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');
   }

jbmc/regression/jbmc-strings/java_append_string/test_append_string.java

@@ -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$

jbmc/regression/jbmc-strings/java_case/test.desc

@@ -1,6 +1,6 @@
 public class test_compare
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s1 = "ab";
       String s2 = "aa";

jbmc/regression/jbmc-strings/java_case/test_case.class

@@ -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$

jbmc/regression/jbmc-strings/java_case/test_case.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();

jbmc/regression/jbmc-strings/java_char_array/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$

jbmc/regression/jbmc-strings/java_char_array/test_char_array.class

@@ -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);

jbmc/regression/jbmc-strings/java_char_array/test_char_array.java

@@ -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$

jbmc/regression/jbmc-strings/java_char_at/test.desc

@@ -1,6 +1,6 @@
 public class test_empty
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String empty = "";
       assert(!empty.isEmpty());

jbmc/regression/jbmc-strings/java_char_at/test_char_at.java

@@ -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$

jbmc/regression/jbmc-strings/java_code_point/test.desc

@@ -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');