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$