Fix tests with missing EXIT or SIGNAL tests

Some tests had previously been passing despite actually causing a crash, due
to the required output being too loosely specified. This ensures the bare minimum:
that every test has an expected EXIT code and SIGNAL result.

The codes suggested were taken from the test's current output, and only applied for
CORE tests, but hand inspection suggests these choices are reasonable.

Author: smowton

regression/ansi-c/Forward_Declaration2/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
 
+^EXIT=(1|64)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
 --

regression/ansi-c/Incomplete_Type1/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
 
+^EXIT=(1|64)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
 --

regression/ansi-c/function_return1/test.desc

@@ -2,6 +2,7 @@ CORE
 main.c
 --verbosity 2
 ^main.c:3:1: warning: function has return void but a return statement returning signed int$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/ansi-c/static2/test.desc

@@ -2,5 +2,7 @@ CORE
 main.c
 main2.c --function foo
 ^main symbol `foo' is ambiguous$
+^EXIT=(1|64)$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/ansi-c/static3/test.desc

@@ -2,5 +2,7 @@ CORE
 main.c
 main2.c --function foo
 ^main symbol `foo' is ambiguous$
+^EXIT=(1|64)$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetArray/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetArray.class
 --function NondetArray.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetArray2/test.desc

@@ -2,6 +2,8 @@ CORE
 NondetArray2.class
 --function NondetArray2.main --unwind 5
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 --
 Disabled pending fixing warnings for array-of with zero length:

regression/cbmc-java/NondetArray3/test.desc

@@ -2,6 +2,8 @@ CORE
 NondetArray3.class
 --function NondetArray3.main --unwind 5
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 --
 Disabled pending fixing warnings for array-of with zero length:

regression/cbmc-java/NondetArray4/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetArray4.class
 --function NondetArray4.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetAssume1/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetAssume1.class
 --function NondetAssume1.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetAssume2/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetAssume2.class
 --function NondetAssume2.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetBoolean/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetBoolean.class
 --function NondetBoolean.main
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetByte/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetByte.class
 --function NondetByte.main
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetCastToObject/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetCastToObject.class
 --function NondetCastToObject.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetChar/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetChar.class
 --function NondetChar.main
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetDirectFromMethod/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetDirectFromMethod.class
 --function NondetDirectFromMethod.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetDouble/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetDouble.class
 --function NondetDouble.main
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetFloat/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetFloat.class
 --function NondetFloat.main
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetGenericArray/test.desc

@@ -2,6 +2,8 @@ CORE
 NondetGenericArray.class
 --function NondetGenericArray.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 --
 Disabled pending fixing warnings for array-of with zero length:

regression/cbmc-java/NondetGenericRecursive/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetGenericRecursive.class
 --function NondetGenericRecursive.main
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetGenericRecursive2/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetGenericRecursive2.class
 --function NondetGenericRecursive2.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetGenericWithNull/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetGenericWithNull.class
 --function NondetGenericWithNull.main
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetGenericWithoutNull/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetGenericWithoutNull.class
 --function NondetGenericWithoutNull.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetInit/test.desc

@@ -2,4 +2,6 @@ CORE
 Test.class
 --function Test.check
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --

regression/cbmc-java/NondetInit/test_lazy.desc

@@ -2,4 +2,6 @@ CORE
 Test.class
 --function Test.check --lazy-methods
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --

regression/cbmc-java/NondetInit2/test.desc

@@ -2,3 +2,5 @@ CORE
 Test.class
 --function Test.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java/NondetInit3/test.desc

@@ -2,3 +2,5 @@ CORE
 Test.class
 --function Test.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java/NondetInt/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetInt.class
 --function NondetInt.main
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetLong/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetLong.class
 --function NondetLong.main
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/NondetShort/test.desc

@@ -2,5 +2,7 @@ CORE
 NondetShort.class
 --function NondetShort.main
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/address_space_size_limit1/test.desc

@@ -2,4 +2,6 @@ CORE
 Test.class
 --object-bits 4
 too many addressed objects
+^EXIT=6$
+^SIGNAL=0$
 --

regression/cbmc-java/array2/test.desc

@@ -2,5 +2,7 @@ CORE
 test.class
 --function test.f --cover location
 \d+ of \d+ covered
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-java/exceptions26/test.desc

@@ -2,6 +2,8 @@ CORE
 test.class
 
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring
 --

regression/cbmc-java/exceptions27/test.desc

@@ -2,6 +2,8 @@ CORE
 test.class
 
 VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring
 --

regression/cbmc-java/inherited_static_field1/test.desc

@@ -2,6 +2,8 @@ CORE
 Test.class
 --function Test.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 --
 This checks that jbmc knows that test.x and parent.x refer to the same field.

regression/cbmc-java/inherited_static_field10/test.desc

@@ -4,6 +4,8 @@ Test.class
 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$
+^EXIT=10$
+^SIGNAL=0$
 --
 Stub static field x found for non-stub type java::Parent\. In future this will be a fatal error\.
 --

regression/cbmc-java/inherited_static_field2/test.desc

@@ -2,6 +2,8 @@ CORE
 Test.class
 --function Test.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 --
 This checks that jbmc knows that Test.x and InterfaceWithStatic.x are the same field.

regression/cbmc-java/inherited_static_field3/test.desc

@@ -2,6 +2,8 @@ CORE
 Test.class
 --function Test.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 --
 This is the same as test inherited_static_field1, except Test's parent is opaque.

regression/cbmc-java/inherited_static_field4/test.desc

@@ -3,6 +3,8 @@ Test.class
 --function Test.main
 assertion at file Test\.java line 6 .* FAILURE
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 --
 This checks that jbmc knows that the hidden field Grandparent.x is not the same

regression/cbmc-java/inherited_static_field5/test.desc

@@ -2,6 +2,8 @@ CORE
 Test.class
 --function Test.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 --
 This is the same as inherited_static_field2, except that Test's parent is opaque. It must pass because

regression/cbmc-java/inherited_static_field6/test.desc

@@ -3,6 +3,8 @@ Test.class
 --function Test.main
 assertion at file Test\.java line 6 .* FAILURE
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 --
 This test is the same as inherited_static_field4, except that Test's parent is opaque.

regression/cbmc-java/inherited_static_field7/test.desc

@@ -2,6 +2,8 @@ CORE
 Test.class
 --function Test.main
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 --
 This test must pass, as there is only one opaque parent (interface_with_static).

regression/cbmc-java/inherited_static_field8/test.desc

@@ -4,6 +4,8 @@ Test.class
 assertion at file Test\.java line 6 .* SUCCESS
 assertion at file Test\.java line 7 .* FAILURE
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 --
 This test is the same as inherited_static_field4, except that Test's grandparent is opaque.

regression/cbmc-java/inherited_static_field9/test.desc

@@ -5,6 +5,8 @@ Stub static field x found for non-stub type java::Test\. In future this will be
 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
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 --
 This tests the corner case where static fields are found on non-stub types, here caused

regression/cbmc-java/lambda1/test.desc

@@ -10,3 +10,5 @@ lambda function reference lambda\$k\$5 in class \"Lambdatest\"
 lambda function reference lambda\$l\$6 in class \"Lambdatest\"
 lambda function reference lambda\$m\$7 in class \"Lambdatest\"
 lambda function reference lambda\$static\$0 in class \"B\"
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc

@@ -3,3 +3,5 @@ Test.class
 --show-goto-functions --function Test.main
 java::Unused::clinit_wrapper
 Unused\.<clinit>\(\)
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc

@@ -1,6 +1,8 @@
 CORE
 Test.class
 --lazy-methods --show-goto-functions --function Test.main
+^EXIT=0$
+^SIGNAL=0$
 --
 java::Unused::clinit_wrapper
 Unused\.<clinit>\(\)

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc

@@ -2,3 +2,5 @@ CORE
 Test.class
 --lazy-methods --function Test.main
 VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc

@@ -4,3 +4,5 @@ Test.class
 java::Unused1::clinit_wrapper
 java::Unused2::clinit_wrapper
 Unused2\.<clinit>\(\)
+^EXIT=0$
+^SIGNAL=0$