Fix tests with incorrect main methods

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

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

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

jbmc/regression/jbmc-strings/java_contains/test_contains.java

@@ -1,6 +1,6 @@
 public class test_contains
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       String s = new String("Abc");
       String u = "bc";

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

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

jbmc/regression/jbmc-strings/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");

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

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

jbmc/regression/jbmc-strings/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";

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

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

jbmc/regression/jbmc-strings/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";

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

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

jbmc/regression/jbmc-strings/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";

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

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

jbmc/regression/jbmc-strings/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';

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

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

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

jbmc/regression/jbmc-strings/java_insert_int/test_insert_int.java

@@ -1,6 +1,6 @@
 public class test_insert_int
 {
-   public static void main(/*String[] argv*/)
+   public static void main()
    {
       StringBuilder sb = new StringBuilder("ac");
       org.cprover.CProverString.insert(sb, 1, 42);

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

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

jbmc/regression/jbmc-strings/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');

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

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

jbmc/regression/jbmc-strings/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");

jbmc/regression/jbmc/NondetCharSequence/test.desc

@@ -1,6 +1,6 @@
 CORE
 NondetCharSequence.class
-
+--function NondetCharSequence.main
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc/NondetString/test.desc

@@ -1,6 +1,6 @@
 CORE
 NondetString.class
-
+--function NondetString.main
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc/NondetStringBuffer/test.desc

@@ -1,6 +1,6 @@
 CORE
 NondetStringBuffer.class
-
+--function NondetStringBuffer.main
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc/NondetStringBuilder/test.desc

@@ -1,6 +1,6 @@
 CORE
 NondetStringBuilder.class
-
+--function NondetStringBuilder.main
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc

@@ -1,6 +1,6 @@
 CORE
 annotations.class
---verbosity 10 --show-symbol-table
+--verbosity 10 --show-symbol-table --function annotations.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^Type\.\.\.\.\.\.\.\.: @java::ClassAnnotation struct annotations

jbmc/regression/jbmc/class-fields/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc/class-literals/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc/class-literals/test_lazy.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---lazy-methods
+--lazy-methods --function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc/classtest1/classtest1.java

@@ -1,6 +1,6 @@
 public class classtest1
 {
-  static void main(String[] args)
+  public static void main(String[] args)
   {
     g(classtest1.class);
   }

jbmc/regression/jbmc/exceptions23/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions
+--java-throw-runtime-exceptions --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED

jbmc/regression/jbmc/exceptions24/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions
+--java-throw-runtime-exceptions --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED

jbmc/regression/jbmc/finally1/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
-
+--function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: FAILURE