Merge pull request #1849 from smowton/smowton/cleanup/java-main-function-types

Cleanup tests with anomalous main functions

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$