Fix java harness for main()

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

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

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$

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";

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$

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

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$

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

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$

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

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$

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