Cleanup tests with anomalous main functions

A forthcoming PR will make jbmc only recognise 'public static void main(String[])' as a main
entry point (anything named 'main' but not matching that type will need explicit --function
nomination. This adds the extra argument where required.

One test (NondetInit3) is fixed as it was previously assuming that its parameter couldn't be
null, which only happens when main(Subclass) is handled like it was main(String[]), where the
String[] reference really cannot be null.

Author: smowton

regression/cbmc-java/ArithmeticException6/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--java-throw-runtime-exceptions --function ArithmeticExceptionTest.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 7 function.*: FAILURE$

regression/cbmc-java/LocalVarTable5/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---show-goto-functions
+--show-goto-functions --function test.main
 dead anonlocal::1i
 dead anonlocal::2i
 dead anonlocal::3a

regression/cbmc-java/NondetInit2/test.desc

@@ -1,5 +1,4 @@
 CORE
 Test.class
-
+--function Test.main
 ^VERIFICATION SUCCESSFUL$
-

regression/cbmc-java/NondetInit3/Subclass.class

@@ -14,7 +14,8 @@ public static void main(Subclass nondetInput) {
         // The condition enforced by cproverNondetInitialize should hold
         // even though the parameter is a subtype of Test, not directly an
         // instance of Test itself.
-        assert nondetInput.arr.length == 1;
+        if(nondetInput != null)
+            assert nondetInput.arr.length == 1;
     }
 
 }

regression/cbmc-java/NondetInit3/Test.class

@@ -1,5 +1,4 @@
 CORE
 Test.class
-
+--function Test.main
 ^VERIFICATION SUCCESSFUL$
-

regression/cbmc-java/NondetInit3/Test.java

@@ -1,6 +1,6 @@
 CORE
 VarLengthArrayTrace1.class
---trace
+--trace --function VarLengthArrayTrace1.main
 ^EXIT=10$
 ^SIGNAL=0$
 dynamic_3_array\[1.*\]=10

regression/cbmc-java/NondetInit3/test.desc

@@ -1,6 +1,6 @@
 CORE
 arrayread1.class
---unwind 3 --no-propagation
+--unwind 3 --no-propagation --function arrayread1.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-java/VarLengthArrayTrace1/test.desc

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

regression/cbmc-java/arrayread1/test.desc

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

regression/cbmc-java/cast_null1/test.desc

@@ -1,6 +1,6 @@
 CORE
 Break.class
---show-goto-functions
+--show-goto-functions --function Break.main
 ^EXIT=0$
 ^SIGNAL=0$
 dead i;

regression/cbmc-java/cast_null2/test.desc

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

regression/cbmc-java/destructor1/test.desc

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

regression/cbmc-java/exceptions22/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---show-symbol-table
+--show-symbol-table --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^pc7:

regression/cbmc-java/external_getstatic1/test.desc

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

regression/cbmc-java/inferlexicalscope1/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 Stub static field x found for non-stub type java::Test\. In future this will be a fatal error\.
 assertion at file Test\.java line 6 .* FAILURE
 ^VERIFICATION FAILED$

regression/cbmc-java/inherited_static_field1/test.desc

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

regression/cbmc-java/inherited_static_field10/test.desc

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

regression/cbmc-java/inherited_static_field2/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 assertion at file Test\.java line 6 .* FAILURE
 ^VERIFICATION FAILED$
 --

regression/cbmc-java/inherited_static_field3/test.desc

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

regression/cbmc-java/inherited_static_field4/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 assertion at file Test\.java line 6 .* FAILURE
 ^VERIFICATION FAILED$
 --

regression/cbmc-java/inherited_static_field5/test.desc

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

regression/cbmc-java/inherited_static_field6/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 assertion at file Test\.java line 6 .* SUCCESS
 assertion at file Test\.java line 7 .* FAILURE
 ^VERIFICATION FAILED$

regression/cbmc-java/inherited_static_field7/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 Stub static field x found for non-stub type java::Test\. In future this will be a fatal error\.
 Stub static field x found for non-stub type java::Parent\. In future this will be a fatal error\.
 assertion at file Test\.java line 6 .* FAILURE

regression/cbmc-java/inherited_static_field8/test.desc

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

regression/cbmc-java/inherited_static_field9/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---cover location --trace --json-ui
+--cover location --trace --json-ui --function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc-java/isnan1/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---cover location --trace --json-ui --unwind 5
+--cover location --trace --json-ui --unwind 5 --function Test.main
 activate-multi-line-match
 EXIT=0
 SIGNAL=0

regression/cbmc-java/json_trace1/test.desc

@@ -1,6 +1,5 @@
 CORE
 Test.class
---show-goto-functions
+--show-goto-functions --function Test.main
 java::Unused::clinit_wrapper
 Unused\.<clinit>\(\)
-

regression/cbmc-java/json_trace3/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---lazy-methods --show-goto-functions
+--lazy-methods --show-goto-functions --function Test.main
 --
 java::Unused::clinit_wrapper
 Unused\.<clinit>\(\)

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc

@@ -1,5 +1,4 @@
 CORE
 Test.class
---lazy-methods
+--lazy-methods --function Test.main
 VERIFICATION SUCCESSFUL
-

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc

@@ -1,7 +1,6 @@
 CORE
 Test.class
---show-goto-functions
+--show-goto-functions --function Test.main
 java::Unused1::clinit_wrapper
 java::Unused2::clinit_wrapper
 Unused2\.<clinit>\(\)
-

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---lazy-methods --show-goto-functions
+--lazy-methods --show-goto-functions --function Test.main
 --
 java::Unused1::clinit_wrapper
 java::Unused2::clinit_wrapper

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc

@@ -1,5 +1,4 @@
 CORE
 Test.class
---lazy-methods
+--lazy-methods --function Test.main
 VERIFICATION SUCCESSFUL
-

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc

@@ -1,5 +1,5 @@
 CORE
 Test.class
---show-goto-functions
+--show-goto-functions --function Test.main
 java::Opaque\.<clinit>:\(\)V
 java::Opaque::clinit_wrapper

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---lazy-methods --show-goto-functions
+--lazy-methods --show-goto-functions --function Test.main
 --
 java::Opaque\.<clinit>:\(\)V
 java::Opaque::clinit_wrapper

regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc

@@ -1,5 +1,4 @@
 CORE
 Test.class
---lazy-methods
+--lazy-methods --function Test.main
 VERIFICATION SUCCESSFUL
-

regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---show-goto-functions
+--show-goto-functions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 test\.java line 5 function java::test.main:\(\)V bytecode-index 1

regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc

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

regression/cbmc-java/putstatic_source_location/test.desc

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

regression/cbmc-java/static_init1/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---trace --json-ui --trace-json-extended
+--trace --json-ui --trace-json-extended --function Test.main
 ^EXIT=10$
 ^SIGNAL=0$
 rawLhs

regression/cbmc-java/static_init2/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---trace --json-ui
+--trace --json-ui --function Test.main
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/cbmc-java/trace_options_json_extended/extended.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---show-goto-functions
+--show-goto-functions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 IF.*"java::C".*THEN GOTO [12]

regression/cbmc-java/trace_options_json_extended/non-extended.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---program-only
+--program-only --function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 C\.f

regression/cbmc-java/virtual7/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_append_char.class
---refine-strings --string-max-length 1000 --no-core-models
+--refine-strings --string-max-length 1000 --no-core-models --function test_append_char.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-java/virtual8/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_init.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_init.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_init.java line 31 .* SUCCESS$

regression/jbmc-strings/java_append_char/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_insert_char_array.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_insert_char_array.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 28.* SUCCESS$

regression/jbmc-strings/java_char_array_init/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_append_string.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_append_string.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/jbmc-strings/java_insert_char_array/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_case.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_case.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_case.java line 10 .* SUCCESS$

regression/strings-smoke-tests/java_append_string/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_char_array.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_char_array.main
 ^EXIT=10$
 ^SIGNAL=0$
 .*assertion.* test_char_array.java line 7 .* SUCCESS$

regression/strings-smoke-tests/java_case/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_insert_char_array.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_insert_char_array.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_insert_char_array.java line 20 .* SUCCESS$

regression/strings-smoke-tests/java_char_array/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test1.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test1.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$