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.

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,6 +2,8 @@ CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --function Test.check --lazy-methods
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
 --
 --
 This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

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 symex-driven-lazy-loading-expected-failure
 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,6 +2,8 @@ CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --lazy-methods --function Test.main
 VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
 --
 --
 This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

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$

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc

@@ -1,6 +1,8 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --lazy-methods --show-goto-functions --function Test.main
+^EXIT=0$
+^SIGNAL=0$
 --
 java::Unused1::clinit_wrapper
 java::Unused2::clinit_wrapper

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc

@@ -2,6 +2,8 @@ CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --lazy-methods --function Test.main
 VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
 --
 --
 This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc

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

regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc

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

regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc

@@ -2,6 +2,8 @@ CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --lazy-methods --function Test.main
 VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
 --
 --
 This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/lots_local_variables_manual/test.desc

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

regression/cbmc-java/lots_of_local_variables/test.desc

@@ -3,4 +3,5 @@ TooManyLocals.class
 --function TooManyLocals.test
 VERIFICATION SUCCESSFUL
 \[java::TooManyLocals\.test:\(\)V\.assertion\.1\] .*: SUCCESS
-EXIT=0
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java/remove_virtual_function_typecast/test.desc

@@ -5,6 +5,8 @@ VirtualFunctions.class
  a \. VirtualFunctions\$A\.f:\(\)V\(\);$
  b \. VirtualFunctions\$B\.f:\(\)V\(\);$
  \(struct VirtualFunctions\$B \*\)c \. VirtualFunctions\$B\.f:\(\)V\(\);$
+^EXIT=0$
+^SIGNAL=0$
 --
 --
 This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/removed_virtual_functions/test.desc

@@ -2,6 +2,8 @@ CORE symex-driven-lazy-loading-expected-failure
 ArrayListEquals.class
 --lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --cover location --function ArrayListEquals.check2 --show-goto-functions
 e2 . ArrayList\$Itr.hasNext:\(\)Z\(\);
+^EXIT=0$
+^SIGNAL=0$
 --
 e2 . ListIterator.hasNext:\(\)Z\(\);
 --

regression/cbmc-java/very-long-jumps/test.desc

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

regression/cbmc-java/virtual10/test.desc

@@ -4,3 +4,5 @@ E.class
 IF.*"java::D"
 IF.*"java::O"
 IF.*"java::C"
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc/Free3/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
 --pointer-check
+^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --

regression/cbmc/Free4/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
 --pointer-check
+^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --

regression/cbmc/Overflow_Addition1/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
 --signed-overflow-check
+^EXIT=10$
 ^SIGNAL=0$
 ^\[.*\] arithmetic overflow on signed \+ in .*: FAILURE$
 ^VERIFICATION FAILED$

regression/cbmc/Overflow_Leftshift1/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
 --signed-overflow-check
+^EXIT=10$
 ^SIGNAL=0$
 ^\[.*\] arithmetic overflow on signed shl in .*: FAILURE$
 ^\*\* 2 of 4 failed

regression/cbmc/Pointer_Arithmetic5/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
 --pointer-check --bounds-check --function f
+^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --

regression/cbmc/Pointer_Arithmetic8/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
 --pointer-check --bounds-check
+^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --

regression/cbmc/Quantifiers-assertion/test.desc

@@ -10,3 +10,5 @@ main.c
 ^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$
 ^\*\* 2 of 6 failed
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$

regression/cbmc/Quantifiers-assignment/test.desc

@@ -8,3 +8,5 @@ main.c
 ^\[main.assertion.4\] assertion z2: SUCCESS$
 ^\*\* 1 of 4 failed
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$

regression/cbmc/Quantifiers-copy/test.desc

@@ -9,3 +9,5 @@ main.c
 ^\[main.assertion.5\] assertion b\[.*\] == 4: SUCCESS$
 ^\*\* 0 of 5 failed
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc/Quantifiers-if/test.desc

@@ -9,3 +9,5 @@ main.c
 ^\[main.assertion.5\] success 2: SUCCESS$
 ^\*\* 3 of 5 failed
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$

regression/cbmc/Quantifiers-initialisation/test.desc

@@ -9,3 +9,5 @@ main.c
 ^\[main.assertion.5\] assertion a\[.*\] == 5: SUCCESS$
 ^\*\* 0 of 5 failed
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc/Quantifiers-initialisation2/test.desc

@@ -9,3 +9,5 @@ main.c
 ^\[main.assertion.5\] assertion c\[.*\] >= c\[.*\]: SUCCESS$
 ^\*\* 1 of 5 failed
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$

regression/cbmc/Quantifiers-invalid-var-range/test.desc

@@ -4,3 +4,5 @@ main.c
 ^\*\* Results:$
 ^\*\* 0 of 1 failed
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc/Quantifiers-not-exists/test.desc

@@ -10,3 +10,5 @@ main.c
 ^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$
 ^\*\* 0 of 6 failed
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc/Quantifiers-not/test.desc

@@ -9,3 +9,5 @@ main.c
 ^\[main.assertion.5\] failure 2: FAILURE$
 ^\*\* 2 of 5 failed
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$

regression/cbmc/Quantifiers-two-dimension-array/test.desc

@@ -9,3 +9,5 @@ main.c
 ^\[main.assertion.5\] assertion tmp_if_expr\$3: SUCCESS$
 ^\*\* 0 of 5 failed
 ^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc/Quantifiers-type/test.desc

@@ -6,3 +6,5 @@ main.c
 ^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$
 ^\*\* 1 of 2 failed
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$

regression/cbmc/Undefined_Function1/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
 
+^EXIT=10$
 ^SIGNAL=0$
 ^\*\*\*\* WARNING: no body for function f$
 ^VERIFICATION FAILED$

regression/cbmc/Undefined_Function2/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
 
+^EXIT=10$
 ^SIGNAL=0$
 ^\*\*\*\* WARNING: no body for function asd$
 ^VERIFICATION FAILED$

regression/cbmc/Undefined_Shift1/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
 --undefined-shift-check
+^EXIT=10$
 ^SIGNAL=0$
 ^\[.*\] shift operand is negative in .*: FAILURE$
 ^\*\* 1 of 2 failed

regression/cbmc/address_space_size_limit1/test.desc

@@ -2,4 +2,6 @@ CORE
 test.c
 --no-simplify --unwind 300 --object-bits 8
 too many addressed objects
+^EXIT=6$
+^SIGNAL=0$
 --

regression/cbmc/pointer-function-parameters-2/test.desc

@@ -7,5 +7,7 @@ main.c
 ^a=&tmp\$\d+!0, tmp\$\d+=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
 ^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=([012356789][0-9]*|4[0-9]+)$
 ^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=4$
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc/pointer-function-parameters/test.desc

@@ -6,5 +6,7 @@ main.c
 ^a=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
 ^a=&tmp\$\d+!0, tmp\$\d+=4$
 ^a=&tmp\$\d+!0, tmp\$\d+=([012356789][0-9]*|4[0-9]+)$
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc/typedef-return-type3/test.desc

@@ -3,8 +3,9 @@ main.c
 --show-symbol-table --function fun
 // Enable multi-line checking
 activate-multi-line-match
-EXIT=0
 Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(\)
 Base name\.+: fun2\nMode\.+: C\nType\.+: CHAINEDINT \(\)
+EXIT=0\n
+SIGNAL=0\n
 --
 warning: ignoring

regression/goto-analyzer/approx-array-variable-const-fp/test.desc

@@ -5,6 +5,7 @@ main.c
 ^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f2 THEN GOTO [0-9]$
 ^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f3 THEN GOTO [0-9]$
 ^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f4 THEN GOTO [0-9]$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f1 THEN GOTO [0-9]$

regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc

@@ -5,6 +5,7 @@ main.c
 ^\s*IF fp == f2 THEN GOTO [0-9]$
 ^\s*IF fp == f3 THEN GOTO [0-9]$
 ^\s*IF fp == f4 THEN GOTO [0-9]$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc

@@ -6,6 +6,7 @@ main.c
 ^\s*IF fp == f3 THEN GOTO [0-9]$
 ^\s*IF fp == f4 THEN GOTO [0-9]$
 replacing function pointer by 3 possible targets
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc

@@ -5,6 +5,7 @@ main.c
 ^\s*IF fp == f2 THEN GOTO [0-9]$
 ^\s*IF fp == f3 THEN GOTO [0-9]$
 ^\s*IF fp == f4 THEN GOTO [0-9]$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc

@@ -5,6 +5,7 @@ main.c
 ^\s*IF fp == f2 THEN GOTO [0-9]$
 ^\s*IF fp == f3 THEN GOTO [0-9]$
 ^\s*IF fp == f4 THEN GOTO [0-9]$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc

@@ -5,6 +5,7 @@ main.c
 ^\s*IF fp == f2 THEN GOTO [0-9]$
 ^\s*IF fp == f3 THEN GOTO [0-9]$
 ^\s*IF fp == f4 THEN GOTO [0-9]$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc

@@ -5,6 +5,7 @@ main.c
 ^\s*IF fp == \(.*\)f2 THEN GOTO [0-9]$
 ^\s*IF fp == \(.*\)f3 THEN GOTO [0-9]$
 ^\s*IF fp == \(.*\)f4 THEN GOTO [0-9]$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc

@@ -6,6 +6,7 @@ main.c
 ^\s*IF fp == f3 THEN GOTO [0-9]$
 ^\s*IF fp == f4 THEN GOTO [0-9]$
 ^\s*ASSERT FALSE // invalid function pointer$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc

@@ -3,6 +3,7 @@ main.c
 --show-goto-functions --verbosity 10 --pointer-check
 ^Removing function pointers and virtual functions$
 ^\s*ASSERT FALSE // invalid function pointer$
+^EXIT=0$
 ^SIGNAL=0$
 function func: replacing function pointer by 0 possible targets
 --

regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc

@@ -11,5 +11,7 @@ main.c
 ^\s*IF \*fp == f7 THEN GOTO [0-9]$
 ^\s*IF \*fp == f8 THEN GOTO [0-9]$
 ^\s*IF \*fp == f9 THEN GOTO [0-9]$
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc

@@ -11,6 +11,7 @@ main.c
 ^\s*IF fp == f7 THEN GOTO [0-9]$
 ^\s*IF fp == f8 THEN GOTO [0-9]$
 ^\s*IF fp == f9 THEN GOTO [0-9]$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc

@@ -11,6 +11,7 @@ main.c
 ^\s*IF fp == f7 THEN GOTO [0-9]$
 ^\s*IF fp == f8 THEN GOTO [0-9]$
 ^\s*IF fp == f9 THEN GOTO [0-9]$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc

@@ -11,6 +11,7 @@ main.c
 ^\s*IF fp2 == f7 THEN GOTO [0-9]$
 ^\s*IF fp2 == f8 THEN GOTO [0-9]$
 ^\s*IF fp2 == f9 THEN GOTO [0-9]$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc

@@ -11,6 +11,7 @@ main.c
 ^\s*IF fp2 == f7 THEN GOTO [0-9]$
 ^\s*IF fp2 == f8 THEN GOTO [0-9]$
 ^\s*IF fp2 == f9 THEN GOTO [0-9]$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc

@@ -11,5 +11,7 @@ main.c
 ^\s*IF fp == f7 THEN GOTO [0-9]$
 ^\s*IF fp == f8 THEN GOTO [0-9]$
 ^\s*IF fp == f9 THEN GOTO [0-9]$
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc

@@ -11,5 +11,7 @@ main.c
 ^\s*IF \*fp == f7 THEN GOTO [0-9]$
 ^\s*IF \*fp == f8 THEN GOTO [0-9]$
 ^\s*IF \*fp == f9 THEN GOTO [0-9]$
+^EXIT=0$
+^SIGNAL=0$
 --
 ^warning: ignoring