Fix tests with incorrect main methods

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_case/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_case.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_case.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$

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

@@ -1,6 +1,6 @@
 public class test_case
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = new String("Ab");
       String l = s.toLowerCase();

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

@@ -1,6 +1,6 @@
 CORE
 test_char_array.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_char_array.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 9.* FAILURE$

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

@@ -1,6 +1,6 @@
 public class test_char_array
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = "abc";
       char [] str = s.toCharArray();

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_code_point/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_code_point.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_code_point.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$

jbmc/regression/jbmc-strings/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 = "!𐤇𐤄𐤋𐤋𐤅";
       StringBuilder sb = new StringBuilder();