From 3b00bdc08561b7b5cb6ca08fb4bb8601bf577090 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 22 Mar 2018 12:16:30 +0000 Subject: [PATCH 1/2] 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 + regression/ansi-c/Incomplete_Type1/test.desc | 1 + regression/ansi-c/function_return1/test.desc | 1 + regression/ansi-c/static2/test.desc | 2 ++ regression/ansi-c/static3/test.desc | 2 ++ regression/cbmc-java/NondetArray/test.desc | 2 ++ regression/cbmc-java/NondetArray2/test.desc | 2 ++ regression/cbmc-java/NondetArray3/test.desc | 2 ++ regression/cbmc-java/NondetArray4/test.desc | 2 ++ regression/cbmc-java/NondetAssume1/test.desc | 2 ++ regression/cbmc-java/NondetAssume2/test.desc | 2 ++ regression/cbmc-java/NondetBoolean/test.desc | 2 ++ regression/cbmc-java/NondetByte/test.desc | 2 ++ regression/cbmc-java/NondetCastToObject/test.desc | 2 ++ regression/cbmc-java/NondetChar/test.desc | 2 ++ regression/cbmc-java/NondetDirectFromMethod/test.desc | 2 ++ regression/cbmc-java/NondetDouble/test.desc | 2 ++ regression/cbmc-java/NondetFloat/test.desc | 2 ++ regression/cbmc-java/NondetGenericArray/test.desc | 2 ++ regression/cbmc-java/NondetGenericRecursive/test.desc | 2 ++ regression/cbmc-java/NondetGenericRecursive2/test.desc | 2 ++ regression/cbmc-java/NondetGenericWithNull/test.desc | 2 ++ regression/cbmc-java/NondetGenericWithoutNull/test.desc | 2 ++ regression/cbmc-java/NondetInit/test.desc | 2 ++ regression/cbmc-java/NondetInit/test_lazy.desc | 2 ++ regression/cbmc-java/NondetInit2/test.desc | 2 ++ regression/cbmc-java/NondetInit3/test.desc | 2 ++ regression/cbmc-java/NondetInt/test.desc | 2 ++ regression/cbmc-java/NondetLong/test.desc | 2 ++ regression/cbmc-java/NondetShort/test.desc | 2 ++ regression/cbmc-java/address_space_size_limit1/test.desc | 2 ++ regression/cbmc-java/array2/test.desc | 2 ++ regression/cbmc-java/exceptions26/test.desc | 2 ++ regression/cbmc-java/exceptions27/test.desc | 2 ++ regression/cbmc-java/inherited_static_field1/test.desc | 2 ++ regression/cbmc-java/inherited_static_field10/test.desc | 2 ++ regression/cbmc-java/inherited_static_field2/test.desc | 2 ++ regression/cbmc-java/inherited_static_field3/test.desc | 2 ++ regression/cbmc-java/inherited_static_field4/test.desc | 2 ++ regression/cbmc-java/inherited_static_field5/test.desc | 2 ++ regression/cbmc-java/inherited_static_field6/test.desc | 2 ++ regression/cbmc-java/inherited_static_field7/test.desc | 2 ++ regression/cbmc-java/inherited_static_field8/test.desc | 2 ++ regression/cbmc-java/inherited_static_field9/test.desc | 2 ++ regression/cbmc-java/lambda1/test.desc | 2 ++ .../check_clinit_normally_present.desc | 2 ++ .../check_clinit_removed_by_lazy_loading.desc | 2 ++ .../check_runs_with_lazy_loading.desc | 2 ++ .../check_clinit_normally_present.desc | 2 ++ .../check_clinit_removed_by_lazy_loading.desc | 2 ++ .../check_runs_with_lazy_loading.desc | 2 ++ .../check_clinit_normally_present.desc | 2 ++ .../check_clinit_removed_by_lazy_loading.desc | 2 ++ .../check_runs_with_lazy_loading.desc | 2 ++ regression/cbmc-java/lots_local_variables_manual/test.desc | 2 ++ regression/cbmc-java/lots_of_local_variables/test.desc | 3 ++- .../cbmc-java/remove_virtual_function_typecast/test.desc | 2 ++ regression/cbmc-java/removed_virtual_functions/test.desc | 2 ++ regression/cbmc-java/very-long-jumps/test.desc | 2 ++ regression/cbmc-java/virtual10/test.desc | 2 ++ regression/cbmc/Free3/test.desc | 1 + regression/cbmc/Free4/test.desc | 1 + regression/cbmc/Overflow_Addition1/test.desc | 1 + regression/cbmc/Overflow_Leftshift1/test.desc | 1 + regression/cbmc/Pointer_Arithmetic5/test.desc | 1 + regression/cbmc/Pointer_Arithmetic8/test.desc | 1 + regression/cbmc/Quantifiers-assertion/test.desc | 2 ++ regression/cbmc/Quantifiers-assignment/test.desc | 2 ++ regression/cbmc/Quantifiers-copy/test.desc | 2 ++ regression/cbmc/Quantifiers-if/test.desc | 2 ++ regression/cbmc/Quantifiers-initialisation/test.desc | 2 ++ regression/cbmc/Quantifiers-initialisation2/test.desc | 2 ++ regression/cbmc/Quantifiers-invalid-var-range/test.desc | 2 ++ regression/cbmc/Quantifiers-not-exists/test.desc | 2 ++ regression/cbmc/Quantifiers-not/test.desc | 2 ++ regression/cbmc/Quantifiers-two-dimension-array/test.desc | 2 ++ regression/cbmc/Quantifiers-type/test.desc | 2 ++ regression/cbmc/Undefined_Function1/test.desc | 1 + regression/cbmc/Undefined_Function2/test.desc | 1 + regression/cbmc/Undefined_Shift1/test.desc | 1 + regression/cbmc/address_space_size_limit1/test.desc | 2 ++ regression/cbmc/pointer-function-parameters-2/test.desc | 2 ++ regression/cbmc/pointer-function-parameters/test.desc | 2 ++ regression/cbmc/typedef-return-type3/test.desc | 3 ++- .../goto-analyzer/approx-array-variable-const-fp/test.desc | 1 + .../approx-const-fp-array-variable-cast-const-fp/test.desc | 1 + .../test.desc | 1 + .../approx-const-fp-array-variable-const-fp/test.desc | 1 + .../test.desc | 1 + .../test.desc | 1 + .../test.desc | 1 + .../test.desc | 1 + .../no-match-array-literal-const-fp-null/test.desc | 1 + .../test.desc | 2 ++ .../test.desc | 1 + .../test.desc | 1 + .../no-match-const-fp-array-literal-non-const-fp/test.desc | 1 + .../no-match-const-fp-array-non-const-fp/test.desc | 1 + .../no-match-const-fp-binary-op-const-lost/test.desc | 2 ++ .../no-match-const-fp-const-array-index-lost/test.desc | 2 ++ .../goto-analyzer/no-match-const-fp-const-array-lost/test.desc | 2 ++ .../goto-analyzer/no-match-const-fp-const-cast/test.desc | 2 ++ .../goto-analyzer/no-match-const-fp-const-fp-null/test.desc | 1 + .../goto-analyzer/no-match-const-fp-const-lost/test.desc | 2 ++ .../test.desc | 1 + .../test.desc | 1 + .../no-match-const-fp-dereference-const-pointer-null/test.desc | 1 + .../test.desc | 1 + .../no-match-const-fp-dynamic-array-non-const-fp/test.desc | 1 + .../no-match-const-fp-non-const-fp-direct-assignment/test.desc | 1 + .../test.desc | 1 + .../no-match-const-fp-non-const-struct-const-fp/test.desc | 1 + .../no-match-const-fp-non-const-struct-non-const-fp/test.desc | 1 + regression/goto-analyzer/no-match-const-fp-null/test.desc | 2 ++ .../no-match-const-fp-ternerary-op-const-lost/test.desc | 2 ++ .../test.desc | 1 + .../no-match-const-pointer-non-const-struct-const-fp/test.desc | 1 + .../no-match-const-struct-non-const-fp-null/test.desc | 1 + .../test.desc | 1 + .../test.desc | 1 + .../test.desc | 1 + .../no-match-non-const-fp-const-fp-direct-assignment/test.desc | 1 + regression/goto-analyzer/no-match-non-const-fp/test.desc | 1 + regression/goto-analyzer/no-match-parameter-const-fp/test.desc | 1 + regression/goto-analyzer/no-match-parameter-fp/test.desc | 1 + .../test.desc | 1 + .../goto-analyzer/precise-array-calculation-const-fp/test.desc | 1 + .../goto-analyzer/precise-array-literal-const-fp/test.desc | 1 + .../precise-const-fp-array-const-variable-const-fp/test.desc | 1 + .../precise-const-fp-array-literal-const-fp-run-time/test.desc | 2 ++ .../precise-const-fp-array-literal-const-fp/test.desc | 1 + .../test.desc | 1 + .../test.desc | 1 + regression/goto-analyzer/precise-const-fp-const-fp/test.desc | 1 + .../test.desc | 1 + .../test.desc | 1 + .../precise-const-fp-const-struct-non-const-fp/test.desc | 1 + .../test.desc | 1 + .../precise-const-fp-supurious-const-loss/test.desc | 2 ++ regression/goto-analyzer/precise-const-fp/test.desc | 2 ++ .../precise-const-pointer-const-struct-fp/test.desc | 1 + .../goto-analyzer/precise-const-struct-non-const-fp/test.desc | 1 + .../precise-derefence-const-pointer-const-fp/test.desc | 1 + regression/goto-analyzer/precise-derefence/test.desc | 2 ++ .../precise-dereference-address-pointer-const-fp/test.desc | 1 + .../test.desc | 1 + .../test.desc | 1 + .../test.desc | 1 + .../goto-analyzer/reachable-functions-basic-json/test.desc | 2 ++ .../goto-analyzer/reachable-functions-basic-text/test.desc | 2 ++ .../goto-analyzer/unreachable-functions-basic-json/test.desc | 2 ++ .../goto-analyzer/unreachable-functions-basic-text/test.desc | 2 ++ .../unreachable-instructions-basic-json/test.desc | 2 ++ .../goto-instrument-typedef/typedef-return-type3/test.desc | 3 ++- .../approx-array-variable-const-fp-only-remove-const/test.desc | 1 + .../approx-array-variable-const-fp-remove-all-fp/test.desc | 1 + regression/goto-instrument/is-threaded1/test.desc | 2 ++ .../no-match-non-const-fp-only-remove-const/test.desc | 1 + .../no-match-non-const-fp-remove-all-fp/test.desc | 1 + .../precise-const-fp-only-remove-const/test.desc | 2 ++ .../goto-instrument/precise-const-fp-remove-all-fp/test.desc | 2 ++ regression/goto-instrument/unwind-assert2/test.desc | 1 + regression/goto-instrument/unwind-assume1/test.desc | 1 + regression/test-script/excluded-line/test.desc | 2 ++ regression/test-script/multi-line/test.desc | 2 ++ regression/test-script/single-line-windows-line-ends/test.desc | 2 ++ regression/test-script/single-line/test.desc | 2 ++ 167 files changed, 264 insertions(+), 3 deletions(-) diff --git a/regression/ansi-c/Forward_Declaration2/test.desc b/regression/ansi-c/Forward_Declaration2/test.desc index 66d458643e7..4010615af79 100644 --- a/regression/ansi-c/Forward_Declaration2/test.desc +++ b/regression/ansi-c/Forward_Declaration2/test.desc @@ -1,6 +1,7 @@ CORE main.c +^EXIT=(1|64)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -- diff --git a/regression/ansi-c/Incomplete_Type1/test.desc b/regression/ansi-c/Incomplete_Type1/test.desc index 66d458643e7..4010615af79 100644 --- a/regression/ansi-c/Incomplete_Type1/test.desc +++ b/regression/ansi-c/Incomplete_Type1/test.desc @@ -1,6 +1,7 @@ CORE main.c +^EXIT=(1|64)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -- diff --git a/regression/ansi-c/function_return1/test.desc b/regression/ansi-c/function_return1/test.desc index f49480a607f..a60637303f3 100644 --- a/regression/ansi-c/function_return1/test.desc +++ b/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 diff --git a/regression/ansi-c/static2/test.desc b/regression/ansi-c/static2/test.desc index 490502d10c5..3fcca6ed4ce 100644 --- a/regression/ansi-c/static2/test.desc +++ b/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 diff --git a/regression/ansi-c/static3/test.desc b/regression/ansi-c/static3/test.desc index 490502d10c5..3fcca6ed4ce 100644 --- a/regression/ansi-c/static3/test.desc +++ b/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 diff --git a/regression/cbmc-java/NondetArray/test.desc b/regression/cbmc-java/NondetArray/test.desc index 63cf6d4cbc0..e4cb3eac34c 100644 --- a/regression/cbmc-java/NondetArray/test.desc +++ b/regression/cbmc-java/NondetArray/test.desc @@ -2,5 +2,7 @@ CORE NondetArray.class --function NondetArray.main ^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetArray2/test.desc b/regression/cbmc-java/NondetArray2/test.desc index 2a274211c6c..a6b99542454 100644 --- a/regression/cbmc-java/NondetArray2/test.desc +++ b/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: diff --git a/regression/cbmc-java/NondetArray3/test.desc b/regression/cbmc-java/NondetArray3/test.desc index de192436903..f6c3db8d443 100644 --- a/regression/cbmc-java/NondetArray3/test.desc +++ b/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: diff --git a/regression/cbmc-java/NondetArray4/test.desc b/regression/cbmc-java/NondetArray4/test.desc index fd419bab2d4..c12d5e6b1a2 100644 --- a/regression/cbmc-java/NondetArray4/test.desc +++ b/regression/cbmc-java/NondetArray4/test.desc @@ -2,5 +2,7 @@ CORE NondetArray4.class --function NondetArray4.main ^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetAssume1/test.desc b/regression/cbmc-java/NondetAssume1/test.desc index bbff9abb9f2..e53695ebd19 100644 --- a/regression/cbmc-java/NondetAssume1/test.desc +++ b/regression/cbmc-java/NondetAssume1/test.desc @@ -2,5 +2,7 @@ CORE NondetAssume1.class --function NondetAssume1.main ^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetAssume2/test.desc b/regression/cbmc-java/NondetAssume2/test.desc index 19abaa63e8a..3e80cdc3698 100644 --- a/regression/cbmc-java/NondetAssume2/test.desc +++ b/regression/cbmc-java/NondetAssume2/test.desc @@ -2,5 +2,7 @@ CORE NondetAssume2.class --function NondetAssume2.main ^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetBoolean/test.desc b/regression/cbmc-java/NondetBoolean/test.desc index c0bfc954449..2c1a3cdef54 100644 --- a/regression/cbmc-java/NondetBoolean/test.desc +++ b/regression/cbmc-java/NondetBoolean/test.desc @@ -2,5 +2,7 @@ CORE NondetBoolean.class --function NondetBoolean.main ^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetByte/test.desc b/regression/cbmc-java/NondetByte/test.desc index d05a462245a..fd2583a2aa5 100644 --- a/regression/cbmc-java/NondetByte/test.desc +++ b/regression/cbmc-java/NondetByte/test.desc @@ -2,5 +2,7 @@ CORE NondetByte.class --function NondetByte.main ^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetCastToObject/test.desc b/regression/cbmc-java/NondetCastToObject/test.desc index 5d3b98bb583..db11cd2c7a1 100644 --- a/regression/cbmc-java/NondetCastToObject/test.desc +++ b/regression/cbmc-java/NondetCastToObject/test.desc @@ -2,5 +2,7 @@ CORE NondetCastToObject.class --function NondetCastToObject.main ^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetChar/test.desc b/regression/cbmc-java/NondetChar/test.desc index 96ecd2f6735..be8fe26a5ed 100644 --- a/regression/cbmc-java/NondetChar/test.desc +++ b/regression/cbmc-java/NondetChar/test.desc @@ -2,5 +2,7 @@ CORE NondetChar.class --function NondetChar.main ^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetDirectFromMethod/test.desc b/regression/cbmc-java/NondetDirectFromMethod/test.desc index 10989391e46..ffcfc8bbc9f 100644 --- a/regression/cbmc-java/NondetDirectFromMethod/test.desc +++ b/regression/cbmc-java/NondetDirectFromMethod/test.desc @@ -2,5 +2,7 @@ CORE NondetDirectFromMethod.class --function NondetDirectFromMethod.main ^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetDouble/test.desc b/regression/cbmc-java/NondetDouble/test.desc index 631edbe5024..a29ddf0044a 100644 --- a/regression/cbmc-java/NondetDouble/test.desc +++ b/regression/cbmc-java/NondetDouble/test.desc @@ -2,5 +2,7 @@ CORE NondetDouble.class --function NondetDouble.main ^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetFloat/test.desc b/regression/cbmc-java/NondetFloat/test.desc index 27bc33761b6..bf3916d2475 100644 --- a/regression/cbmc-java/NondetFloat/test.desc +++ b/regression/cbmc-java/NondetFloat/test.desc @@ -2,5 +2,7 @@ CORE NondetFloat.class --function NondetFloat.main ^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetGenericArray/test.desc b/regression/cbmc-java/NondetGenericArray/test.desc index 9abfffc4b9f..3467d3688d3 100644 --- a/regression/cbmc-java/NondetGenericArray/test.desc +++ b/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: diff --git a/regression/cbmc-java/NondetGenericRecursive/test.desc b/regression/cbmc-java/NondetGenericRecursive/test.desc index 34af1b2e6c1..c1bed1d7faa 100644 --- a/regression/cbmc-java/NondetGenericRecursive/test.desc +++ b/regression/cbmc-java/NondetGenericRecursive/test.desc @@ -2,5 +2,7 @@ CORE NondetGenericRecursive.class --function NondetGenericRecursive.main ^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetGenericRecursive2/test.desc b/regression/cbmc-java/NondetGenericRecursive2/test.desc index 52558889313..87c2e5bac6c 100644 --- a/regression/cbmc-java/NondetGenericRecursive2/test.desc +++ b/regression/cbmc-java/NondetGenericRecursive2/test.desc @@ -2,5 +2,7 @@ CORE NondetGenericRecursive2.class --function NondetGenericRecursive2.main ^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetGenericWithNull/test.desc b/regression/cbmc-java/NondetGenericWithNull/test.desc index c2feb23068d..72ca48ee909 100644 --- a/regression/cbmc-java/NondetGenericWithNull/test.desc +++ b/regression/cbmc-java/NondetGenericWithNull/test.desc @@ -2,5 +2,7 @@ CORE NondetGenericWithNull.class --function NondetGenericWithNull.main ^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetGenericWithoutNull/test.desc b/regression/cbmc-java/NondetGenericWithoutNull/test.desc index e9ada8b935c..ed0d2ae3961 100644 --- a/regression/cbmc-java/NondetGenericWithoutNull/test.desc +++ b/regression/cbmc-java/NondetGenericWithoutNull/test.desc @@ -2,5 +2,7 @@ CORE NondetGenericWithoutNull.class --function NondetGenericWithoutNull.main ^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetInit/test.desc b/regression/cbmc-java/NondetInit/test.desc index aac61dbb85f..b02576cd87e 100644 --- a/regression/cbmc-java/NondetInit/test.desc +++ b/regression/cbmc-java/NondetInit/test.desc @@ -2,4 +2,6 @@ CORE Test.class --function Test.check ^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ -- diff --git a/regression/cbmc-java/NondetInit/test_lazy.desc b/regression/cbmc-java/NondetInit/test_lazy.desc index 6840ea97697..bf052725744 100644 --- a/regression/cbmc-java/NondetInit/test_lazy.desc +++ b/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 diff --git a/regression/cbmc-java/NondetInit2/test.desc b/regression/cbmc-java/NondetInit2/test.desc index 4d752d2f54a..01cbe9f70f3 100644 --- a/regression/cbmc-java/NondetInit2/test.desc +++ b/regression/cbmc-java/NondetInit2/test.desc @@ -2,3 +2,5 @@ CORE Test.class --function Test.main ^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/cbmc-java/NondetInit3/test.desc b/regression/cbmc-java/NondetInit3/test.desc index 4d752d2f54a..01cbe9f70f3 100644 --- a/regression/cbmc-java/NondetInit3/test.desc +++ b/regression/cbmc-java/NondetInit3/test.desc @@ -2,3 +2,5 @@ CORE Test.class --function Test.main ^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/cbmc-java/NondetInt/test.desc b/regression/cbmc-java/NondetInt/test.desc index 324d69b8c91..9965a71094a 100644 --- a/regression/cbmc-java/NondetInt/test.desc +++ b/regression/cbmc-java/NondetInt/test.desc @@ -2,5 +2,7 @@ CORE NondetInt.class --function NondetInt.main ^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetLong/test.desc b/regression/cbmc-java/NondetLong/test.desc index f92db994e00..0129d963f70 100644 --- a/regression/cbmc-java/NondetLong/test.desc +++ b/regression/cbmc-java/NondetLong/test.desc @@ -2,5 +2,7 @@ CORE NondetLong.class --function NondetLong.main ^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NondetShort/test.desc b/regression/cbmc-java/NondetShort/test.desc index 24ac39c540b..2f010bd1874 100644 --- a/regression/cbmc-java/NondetShort/test.desc +++ b/regression/cbmc-java/NondetShort/test.desc @@ -2,5 +2,7 @@ CORE NondetShort.class --function NondetShort.main ^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/address_space_size_limit1/test.desc b/regression/cbmc-java/address_space_size_limit1/test.desc index d08ff5b05c1..ca2cc316d3e 100644 --- a/regression/cbmc-java/address_space_size_limit1/test.desc +++ b/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$ -- diff --git a/regression/cbmc-java/array2/test.desc b/regression/cbmc-java/array2/test.desc index 6d2226bb26b..4998d1faa84 100644 --- a/regression/cbmc-java/array2/test.desc +++ b/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 diff --git a/regression/cbmc-java/exceptions26/test.desc b/regression/cbmc-java/exceptions26/test.desc index eb2dc18d2cb..a935e57be55 100644 --- a/regression/cbmc-java/exceptions26/test.desc +++ b/regression/cbmc-java/exceptions26/test.desc @@ -2,6 +2,8 @@ CORE test.class ^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring -- diff --git a/regression/cbmc-java/exceptions27/test.desc b/regression/cbmc-java/exceptions27/test.desc index 459f879662b..aa680f8c04e 100644 --- a/regression/cbmc-java/exceptions27/test.desc +++ b/regression/cbmc-java/exceptions27/test.desc @@ -2,6 +2,8 @@ CORE test.class VERIFICATION SUCCESSFUL +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring -- diff --git a/regression/cbmc-java/inherited_static_field1/test.desc b/regression/cbmc-java/inherited_static_field1/test.desc index 6d1cf2a4270..e31ff15cc64 100644 --- a/regression/cbmc-java/inherited_static_field1/test.desc +++ b/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. diff --git a/regression/cbmc-java/inherited_static_field10/test.desc b/regression/cbmc-java/inherited_static_field10/test.desc index 63e8c8db02d..117647f5c36 100644 --- a/regression/cbmc-java/inherited_static_field10/test.desc +++ b/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\. -- diff --git a/regression/cbmc-java/inherited_static_field2/test.desc b/regression/cbmc-java/inherited_static_field2/test.desc index c6fde2b99c7..5c3f06d132f 100644 --- a/regression/cbmc-java/inherited_static_field2/test.desc +++ b/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. diff --git a/regression/cbmc-java/inherited_static_field3/test.desc b/regression/cbmc-java/inherited_static_field3/test.desc index a56e09480bc..1894e8a4ba2 100644 --- a/regression/cbmc-java/inherited_static_field3/test.desc +++ b/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. diff --git a/regression/cbmc-java/inherited_static_field4/test.desc b/regression/cbmc-java/inherited_static_field4/test.desc index 63d3b477175..bc5658599ec 100644 --- a/regression/cbmc-java/inherited_static_field4/test.desc +++ b/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 diff --git a/regression/cbmc-java/inherited_static_field5/test.desc b/regression/cbmc-java/inherited_static_field5/test.desc index 9351c137b97..062b6178544 100644 --- a/regression/cbmc-java/inherited_static_field5/test.desc +++ b/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 diff --git a/regression/cbmc-java/inherited_static_field6/test.desc b/regression/cbmc-java/inherited_static_field6/test.desc index 1fc8f3e76cd..7f8a7c59b09 100644 --- a/regression/cbmc-java/inherited_static_field6/test.desc +++ b/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. diff --git a/regression/cbmc-java/inherited_static_field7/test.desc b/regression/cbmc-java/inherited_static_field7/test.desc index 606f5f04f93..c9e77558971 100644 --- a/regression/cbmc-java/inherited_static_field7/test.desc +++ b/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). diff --git a/regression/cbmc-java/inherited_static_field8/test.desc b/regression/cbmc-java/inherited_static_field8/test.desc index 501b3260dd2..9ee512c13ce 100644 --- a/regression/cbmc-java/inherited_static_field8/test.desc +++ b/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. diff --git a/regression/cbmc-java/inherited_static_field9/test.desc b/regression/cbmc-java/inherited_static_field9/test.desc index 01318dfb9ec..327b22e692f 100644 --- a/regression/cbmc-java/inherited_static_field9/test.desc +++ b/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 diff --git a/regression/cbmc-java/lambda1/test.desc b/regression/cbmc-java/lambda1/test.desc index 9ec5bd91cbd..0895e3afe64 100644 --- a/regression/cbmc-java/lambda1/test.desc +++ b/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$ diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc index f05b7408521..56fb8f416a6 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc +++ b/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\.\(\) +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc index 49c88acd878..78f4c4ccdb4 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc +++ b/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\.\(\) diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc index 0c6c32b0319..3a9e95ea6e9 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc +++ b/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 diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc index 18c1eda7556..3bb1dc48487 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc +++ b/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\.\(\) +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc index 7a6c066bf9d..d0cc65b168d 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc +++ b/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 diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc index 0c6c32b0319..3a9e95ea6e9 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc +++ b/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 diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc index 81312c026c4..a52f8d6cd60 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc +++ b/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\.:\(\)V java::Opaque::clinit_wrapper +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc index b0256ccbad8..ee136e386e8 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc +++ b/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\.:\(\)V java::Opaque::clinit_wrapper diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc index 0c6c32b0319..3a9e95ea6e9 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc +++ b/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 diff --git a/regression/cbmc-java/lots_local_variables_manual/test.desc b/regression/cbmc-java/lots_local_variables_manual/test.desc index 4d5140cf86d..c7c549bfade 100644 --- a/regression/cbmc-java/lots_local_variables_manual/test.desc +++ b/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$ diff --git a/regression/cbmc-java/lots_of_local_variables/test.desc b/regression/cbmc-java/lots_of_local_variables/test.desc index eaa7d76f397..cbe9e269ccc 100644 --- a/regression/cbmc-java/lots_of_local_variables/test.desc +++ b/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$ diff --git a/regression/cbmc-java/remove_virtual_function_typecast/test.desc b/regression/cbmc-java/remove_virtual_function_typecast/test.desc index 05841fcdc63..8bbea6300ec 100644 --- a/regression/cbmc-java/remove_virtual_function_typecast/test.desc +++ b/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 diff --git a/regression/cbmc-java/removed_virtual_functions/test.desc b/regression/cbmc-java/removed_virtual_functions/test.desc index 93a66232f62..cf36ec36380 100644 --- a/regression/cbmc-java/removed_virtual_functions/test.desc +++ b/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\(\); -- diff --git a/regression/cbmc-java/very-long-jumps/test.desc b/regression/cbmc-java/very-long-jumps/test.desc index c8283835a66..6ebcaf81907 100644 --- a/regression/cbmc-java/very-long-jumps/test.desc +++ b/regression/cbmc-java/very-long-jumps/test.desc @@ -2,3 +2,5 @@ CORE NopJumps.class --function NopJumps.test VERIFICATION SUCCESSFUL +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/cbmc-java/virtual10/test.desc b/regression/cbmc-java/virtual10/test.desc index ea746c52c19..ab07b0a117f 100644 --- a/regression/cbmc-java/virtual10/test.desc +++ b/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$ diff --git a/regression/cbmc/Free3/test.desc b/regression/cbmc/Free3/test.desc index ab702ffaf7f..950f6791fef 100644 --- a/regression/cbmc/Free3/test.desc +++ b/regression/cbmc/Free3/test.desc @@ -1,6 +1,7 @@ CORE main.c --pointer-check +^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -- diff --git a/regression/cbmc/Free4/test.desc b/regression/cbmc/Free4/test.desc index ab702ffaf7f..950f6791fef 100644 --- a/regression/cbmc/Free4/test.desc +++ b/regression/cbmc/Free4/test.desc @@ -1,6 +1,7 @@ CORE main.c --pointer-check +^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -- diff --git a/regression/cbmc/Overflow_Addition1/test.desc b/regression/cbmc/Overflow_Addition1/test.desc index 850b22d1a46..979e031e3f8 100644 --- a/regression/cbmc/Overflow_Addition1/test.desc +++ b/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$ diff --git a/regression/cbmc/Overflow_Leftshift1/test.desc b/regression/cbmc/Overflow_Leftshift1/test.desc index 04360e32357..85c5de77e74 100644 --- a/regression/cbmc/Overflow_Leftshift1/test.desc +++ b/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 diff --git a/regression/cbmc/Pointer_Arithmetic5/test.desc b/regression/cbmc/Pointer_Arithmetic5/test.desc index 3623f8499b3..f9c919bbdc2 100644 --- a/regression/cbmc/Pointer_Arithmetic5/test.desc +++ b/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$ -- diff --git a/regression/cbmc/Pointer_Arithmetic8/test.desc b/regression/cbmc/Pointer_Arithmetic8/test.desc index 521480bbd98..4b9176a942e 100644 --- a/regression/cbmc/Pointer_Arithmetic8/test.desc +++ b/regression/cbmc/Pointer_Arithmetic8/test.desc @@ -1,6 +1,7 @@ CORE main.c --pointer-check --bounds-check +^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -- diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc index e332559487b..018411f7345 100644 --- a/regression/cbmc/Quantifiers-assertion/test.desc +++ b/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$ diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc index d6a61824499..41148962905 100644 --- a/regression/cbmc/Quantifiers-assignment/test.desc +++ b/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$ diff --git a/regression/cbmc/Quantifiers-copy/test.desc b/regression/cbmc/Quantifiers-copy/test.desc index 8e25d406497..e6138e282c0 100644 --- a/regression/cbmc/Quantifiers-copy/test.desc +++ b/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$ diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc index 1748c6f9785..92ad6e0bb93 100644 --- a/regression/cbmc/Quantifiers-if/test.desc +++ b/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$ diff --git a/regression/cbmc/Quantifiers-initialisation/test.desc b/regression/cbmc/Quantifiers-initialisation/test.desc index 9ef836b08b1..3dfc3721b41 100644 --- a/regression/cbmc/Quantifiers-initialisation/test.desc +++ b/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$ diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc index 16fa7993bc3..760a1c959e9 100644 --- a/regression/cbmc/Quantifiers-initialisation2/test.desc +++ b/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$ diff --git a/regression/cbmc/Quantifiers-invalid-var-range/test.desc b/regression/cbmc/Quantifiers-invalid-var-range/test.desc index a3da377cadf..e160567e531 100644 --- a/regression/cbmc/Quantifiers-invalid-var-range/test.desc +++ b/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$ diff --git a/regression/cbmc/Quantifiers-not-exists/test.desc b/regression/cbmc/Quantifiers-not-exists/test.desc index 30634de97cb..e4fd61a058f 100644 --- a/regression/cbmc/Quantifiers-not-exists/test.desc +++ b/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$ diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc index bb6f94910fe..884b944ec24 100644 --- a/regression/cbmc/Quantifiers-not/test.desc +++ b/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$ diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc index 755c40a10df..2c1c7dab05f 100644 --- a/regression/cbmc/Quantifiers-two-dimension-array/test.desc +++ b/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$ diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc index 449a653d9f6..1451871c4ec 100644 --- a/regression/cbmc/Quantifiers-type/test.desc +++ b/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$ diff --git a/regression/cbmc/Undefined_Function1/test.desc b/regression/cbmc/Undefined_Function1/test.desc index 859b6e34d6e..431b8dc42b1 100644 --- a/regression/cbmc/Undefined_Function1/test.desc +++ b/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$ diff --git a/regression/cbmc/Undefined_Function2/test.desc b/regression/cbmc/Undefined_Function2/test.desc index dfc2542dd35..bf3843459f5 100644 --- a/regression/cbmc/Undefined_Function2/test.desc +++ b/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$ diff --git a/regression/cbmc/Undefined_Shift1/test.desc b/regression/cbmc/Undefined_Shift1/test.desc index e82c3b92690..8e4d9120b06 100644 --- a/regression/cbmc/Undefined_Shift1/test.desc +++ b/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 diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/regression/cbmc/address_space_size_limit1/test.desc index d0d0ed3c04e..161958f9d5d 100644 --- a/regression/cbmc/address_space_size_limit1/test.desc +++ b/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$ -- diff --git a/regression/cbmc/pointer-function-parameters-2/test.desc b/regression/cbmc/pointer-function-parameters-2/test.desc index 584e452fc11..cacad593080 100644 --- a/regression/cbmc/pointer-function-parameters-2/test.desc +++ b/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 diff --git a/regression/cbmc/pointer-function-parameters/test.desc b/regression/cbmc/pointer-function-parameters/test.desc index 809730ea5f1..2ea09c85011 100644 --- a/regression/cbmc/pointer-function-parameters/test.desc +++ b/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 diff --git a/regression/cbmc/typedef-return-type3/test.desc b/regression/cbmc/typedef-return-type3/test.desc index 7cfecafece9..f94976bdbc8 100644 --- a/regression/cbmc/typedef-return-type3/test.desc +++ b/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 diff --git a/regression/goto-analyzer/approx-array-variable-const-fp/test.desc b/regression/goto-analyzer/approx-array-variable-const-fp/test.desc index c0e6ab6bfc2..d31ea7196bf 100644 --- a/regression/goto-analyzer/approx-array-variable-const-fp/test.desc +++ b/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]$ diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc index 0d2ddf970da..1e35e023c98 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc +++ b/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 diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc index 383f5ad956c..1ff684bf0a6 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc +++ b/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 diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc index 0d2ddf970da..1e35e023c98 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc +++ b/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 diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc index 0d2ddf970da..1e35e023c98 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc +++ b/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 diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc index 0d2ddf970da..1e35e023c98 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc +++ b/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 diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc index da896db86eb..c4ac12fc4cd 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc +++ b/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 diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc index fab84bc077c..381af514314 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc +++ b/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 diff --git a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc index 90a60c56a40..593448f852c 100644 --- a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc +++ b/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 -- diff --git a/regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc b/regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc index cb389930278..64e365b7f58 100644 --- a/regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc +++ b/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 diff --git a/regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc b/regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc index a73805f5730..c2598de9fd0 100644 --- a/regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc +++ b/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 diff --git a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc b/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc index a73805f5730..c2598de9fd0 100644 --- a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc +++ b/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 diff --git a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc index 13d0c5353ce..396d68e504f 100644 --- a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc +++ b/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 diff --git a/regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc index 13d0c5353ce..396d68e504f 100644 --- a/regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc +++ b/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 diff --git a/regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc index b9a72f79cfe..c2598de9fd0 100644 --- a/regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc +++ b/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 diff --git a/regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc index cb389930278..64e365b7f58 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc +++ b/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 diff --git a/regression/goto-analyzer/no-match-const-fp-const-array-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-const-array-lost/test.desc index cb389930278..64e365b7f58 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-array-lost/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-array-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 diff --git a/regression/goto-analyzer/no-match-const-fp-const-cast/test.desc b/regression/goto-analyzer/no-match-const-fp-const-cast/test.desc index b9a72f79cfe..c2598de9fd0 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-cast/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-cast/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 diff --git a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc index 1299353033d..43eb5d910b1 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-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$ replacing function pointer by 0 possible targets -- diff --git a/regression/goto-analyzer/no-match-const-fp-const-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-const-lost/test.desc index b9a72f79cfe..c2598de9fd0 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-lost/test.desc +++ b/regression/goto-analyzer/no-match-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 diff --git a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc index 40a2b941d75..d6679373525 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc @@ -4,6 +4,7 @@ main.c ^Removing function pointers and virtual functions$ ^\s*ASSERT FALSE // invalid function pointer$ replacing function pointer by 9 possible targets +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/test.desc index a73805f5730..c2598de9fd0 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/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 diff --git a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc index 40a2b941d75..d6679373525 100644 --- a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc @@ -4,6 +4,7 @@ main.c ^Removing function pointers and virtual functions$ ^\s*ASSERT FALSE // invalid function pointer$ replacing function pointer by 9 possible targets +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc index f7f42277bae..c4e86a43f86 100644 --- a/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc @@ -11,6 +11,7 @@ main.c ^\s*IF final_fp == f7 THEN GOTO [0-9]$ ^\s*IF final_fp == f8 THEN GOTO [0-9]$ ^\s*IF final_fp == f9 THEN GOTO [0-9]$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc index a73805f5730..c2598de9fd0 100644 --- a/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/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 diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/test.desc index 13d0c5353ce..396d68e504f 100644 --- a/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/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 diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/test.desc index a73805f5730..c2598de9fd0 100644 --- a/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/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 diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/test.desc index a73805f5730..c2598de9fd0 100644 --- a/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/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 diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/test.desc index a73805f5730..c2598de9fd0 100644 --- a/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/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 diff --git a/regression/goto-analyzer/no-match-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-null/test.desc index bea1fb7c356..45ac178fd97 100644 --- a/regression/goto-analyzer/no-match-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-null/test.desc @@ -4,5 +4,7 @@ main.c ^Removing function pointers and virtual functions$ ^\s*ASSERT FALSE // invalid function pointer$ function func: replacing function pointer by 0 possible targets +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/no-match-const-fp-ternerary-op-const-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-ternerary-op-const-lost/test.desc index b9a72f79cfe..c2598de9fd0 100644 --- a/regression/goto-analyzer/no-match-const-fp-ternerary-op-const-lost/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-ternerary-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 diff --git a/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc b/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc index 4e6fda43498..3706e30d09c 100644 --- a/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc +++ b/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc @@ -11,6 +11,7 @@ main.c ^\s*IF container_pointer->fp == f7 THEN GOTO [0-9]$ ^\s*IF container_pointer->fp == f8 THEN GOTO [0-9]$ ^\s*IF container_pointer->fp == f9 THEN GOTO [0-9]$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc index eaad08aafe0..cc52bb1739a 100644 --- a/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc @@ -11,6 +11,7 @@ main.c ^\s*IF pts->go == f7 THEN GOTO [0-9]$ ^\s*IF pts->go == f8 THEN GOTO [0-9]$ ^\s*IF pts->go == f9 THEN GOTO [0-9]$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc index 1299353033d..43eb5d910b1 100644 --- a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-struct-non-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$ replacing function pointer by 0 possible targets -- diff --git a/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc index ef491f67113..635fe8c055d 100644 --- a/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc @@ -11,6 +11,7 @@ main.c ^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f7 THEN GOTO [0-9]$ ^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f8 THEN GOTO [0-9]$ ^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f9 THEN GOTO [0-9]$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc index 662bd323844..3e98fc6c9b9 100644 --- a/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc @@ -11,6 +11,7 @@ main.c ^\s*IF \*container_container\.container == f7 THEN GOTO [0-9]$ ^\s*IF \*container_container\.container == f8 THEN GOTO [0-9]$ ^\s*IF \*container_container\.container == f9 THEN GOTO [0-9]$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc index 662bd323844..3e98fc6c9b9 100644 --- a/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc @@ -11,6 +11,7 @@ main.c ^\s*IF \*container_container\.container == f7 THEN GOTO [0-9]$ ^\s*IF \*container_container\.container == f8 THEN GOTO [0-9]$ ^\s*IF \*container_container\.container == f9 THEN GOTO [0-9]$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/test.desc b/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/test.desc index 13d0c5353ce..396d68e504f 100644 --- a/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/test.desc +++ b/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/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 diff --git a/regression/goto-analyzer/no-match-non-const-fp/test.desc b/regression/goto-analyzer/no-match-non-const-fp/test.desc index a73805f5730..c2598de9fd0 100644 --- a/regression/goto-analyzer/no-match-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-non-const-fp/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 diff --git a/regression/goto-analyzer/no-match-parameter-const-fp/test.desc b/regression/goto-analyzer/no-match-parameter-const-fp/test.desc index a73805f5730..c2598de9fd0 100644 --- a/regression/goto-analyzer/no-match-parameter-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-parameter-const-fp/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 diff --git a/regression/goto-analyzer/no-match-parameter-fp/test.desc b/regression/goto-analyzer/no-match-parameter-fp/test.desc index a73805f5730..c2598de9fd0 100644 --- a/regression/goto-analyzer/no-match-parameter-fp/test.desc +++ b/regression/goto-analyzer/no-match-parameter-fp/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 diff --git a/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc b/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc index a85714b51a1..7570d9d8ef6 100644 --- a/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc @@ -11,6 +11,7 @@ main.c ^\s*IF container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f7 THEN GOTO [0-9]$ ^\s*IF container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f8 THEN GOTO [0-9]$ ^\s*IF container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f9 THEN GOTO [0-9]$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc b/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc index 98fc0ff815c..398b0d84c6f 100644 --- a/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc +++ b/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f3\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-array-literal-const-fp/test.desc b/regression/goto-analyzer/precise-array-literal-const-fp/test.desc index 98fc0ff815c..398b0d84c6f 100644 --- a/regression/goto-analyzer/precise-array-literal-const-fp/test.desc +++ b/regression/goto-analyzer/precise-array-literal-const-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f3\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc index 98fc0ff815c..398b0d84c6f 100644 --- a/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f3\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc index bb3ac1b5cf1..398b0d84c6f 100644 --- a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc @@ -3,6 +3,8 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f3\(\);$ +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc index 98fc0ff815c..398b0d84c6f 100644 --- a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f3\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc index 98fc0ff815c..398b0d84c6f 100644 --- a/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f3\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc index 153ca97de3b..77e1ff4d791 100644 --- a/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f2\(\); +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-const-fp-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-fp/test.desc index 27df5bd2f67..897c8f615f3 100644 --- a/regression/goto-analyzer/precise-const-fp-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f2\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc index 98fc0ff815c..398b0d84c6f 100644 --- a/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f3\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc index 98fc0ff815c..398b0d84c6f 100644 --- a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f3\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc index 153ca97de3b..77e1ff4d791 100644 --- a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f2\(\); +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc index 98fc0ff815c..398b0d84c6f 100644 --- a/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f3\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc b/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc index 76734999981..acf8a25b97f 100644 --- a/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc +++ b/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc @@ -3,6 +3,8 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f2\(\); +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring ^\s*\d+:\s*f1\(\); diff --git a/regression/goto-analyzer/precise-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp/test.desc index 402774c29b7..77e1ff4d791 100644 --- a/regression/goto-analyzer/precise-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp/test.desc @@ -3,6 +3,8 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f2\(\); +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc b/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc index 27df5bd2f67..897c8f615f3 100644 --- a/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc +++ b/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f2\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc index 153ca97de3b..77e1ff4d791 100644 --- a/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f2\(\); +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc index 98fc0ff815c..398b0d84c6f 100644 --- a/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f3\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-derefence/test.desc b/regression/goto-analyzer/precise-derefence/test.desc index 402774c29b7..77e1ff4d791 100644 --- a/regression/goto-analyzer/precise-derefence/test.desc +++ b/regression/goto-analyzer/precise-derefence/test.desc @@ -3,6 +3,8 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f2\(\); +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc index 98fc0ff815c..398b0d84c6f 100644 --- a/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f3\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc index 98fc0ff815c..398b0d84c6f 100644 --- a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f3\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc index 98fc0ff815c..398b0d84c6f 100644 --- a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f3\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc index 98fc0ff815c..398b0d84c6f 100644 --- a/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*f3\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/reachable-functions-basic-json/test.desc b/regression/goto-analyzer/reachable-functions-basic-json/test.desc index c7c9455ee76..78060f012c4 100644 --- a/regression/goto-analyzer/reachable-functions-basic-json/test.desc +++ b/regression/goto-analyzer/reachable-functions-basic-json/test.desc @@ -5,6 +5,8 @@ CORE "function": "dead_inside",$ "function": "obviously_dead",$ "function": "not_obviously_dead",$ +^EXIT=0$ +^SIGNAL=0$ -- "last line":[[:space:]]*$ ^warning: ignoring diff --git a/regression/goto-analyzer/reachable-functions-basic-text/test.desc b/regression/goto-analyzer/reachable-functions-basic-text/test.desc index 86a1a62015c..2ef6e1898c8 100644 --- a/regression/goto-analyzer/reachable-functions-basic-text/test.desc +++ b/regression/goto-analyzer/reachable-functions-basic-text/test.desc @@ -5,5 +5,7 @@ unreachable.c main 35 42$ unreachable.c dead_inside 8 14$ unreachable.c obviously_dead 16 23$ unreachable.c not_obviously_dead 25 31$ +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/unreachable-functions-basic-json/test.desc b/regression/goto-analyzer/unreachable-functions-basic-json/test.desc index 8828b4bbb17..bc0e912bd23 100644 --- a/regression/goto-analyzer/unreachable-functions-basic-json/test.desc +++ b/regression/goto-analyzer/unreachable-functions-basic-json/test.desc @@ -5,6 +5,8 @@ CORE "first line": 3, "function": "not_called", "last line": 6 +^EXIT=0$ +^SIGNAL=0$ -- "last line":[[:space:]]*$ ^warning: ignoring diff --git a/regression/goto-analyzer/unreachable-functions-basic-text/test.desc b/regression/goto-analyzer/unreachable-functions-basic-text/test.desc index a6918166e71..d59eff8448f 100644 --- a/regression/goto-analyzer/unreachable-functions-basic-text/test.desc +++ b/regression/goto-analyzer/unreachable-functions-basic-text/test.desc @@ -2,5 +2,7 @@ CORE ../unreachable-instructions-basic-text/unreachable.c --unreachable-functions unreachable.c not_called 3 6$ +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/unreachable-instructions-basic-json/test.desc b/regression/goto-analyzer/unreachable-instructions-basic-json/test.desc index e5e0a7d1a91..830458c1c3f 100644 --- a/regression/goto-analyzer/unreachable-instructions-basic-json/test.desc +++ b/regression/goto-analyzer/unreachable-instructions-basic-json/test.desc @@ -17,5 +17,7 @@ CORE "function": "dead_inside", "line": "12", "statement": "y = y \+ 1;" +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-return-type3/test.desc b/regression/goto-instrument-typedef/typedef-return-type3/test.desc index 2ce71940ee5..eec53efe82a 100644 --- a/regression/goto-instrument-typedef/typedef-return-type3/test.desc +++ b/regression/goto-instrument-typedef/typedef-return-type3/test.desc @@ -3,8 +3,9 @@ main.c --show-symbol-table // 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 diff --git a/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc b/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc index bc553fa5a0f..bf47edf8dbd 100644 --- a/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc +++ b/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc @@ -4,6 +4,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]$ diff --git a/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc b/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc index e9ede02a296..a88ad48002a 100644 --- a/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc +++ b/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc @@ -4,6 +4,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]$ diff --git a/regression/goto-instrument/is-threaded1/test.desc b/regression/goto-instrument/is-threaded1/test.desc index a9bc6080e8d..834c8a61e9f 100644 --- a/regression/goto-instrument/is-threaded1/test.desc +++ b/regression/goto-instrument/is-threaded1/test.desc @@ -3,5 +3,7 @@ main.c --show-threaded activate-multi-line-match x = 2;\nIs threaded: True +EXIT=0\n +SIGNAL=0\n -- ^warning: ignoring diff --git a/regression/goto-instrument/no-match-non-const-fp-only-remove-const/test.desc b/regression/goto-instrument/no-match-non-const-fp-only-remove-const/test.desc index 9c23726e83c..299b001c84c 100644 --- a/regression/goto-instrument/no-match-non-const-fp-only-remove-const/test.desc +++ b/regression/goto-instrument/no-match-non-const-fp-only-remove-const/test.desc @@ -2,6 +2,7 @@ CORE main.c --verbosity 10 --pointer-check --remove-const-function-pointers ^\s*fp\(\);$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/test.desc b/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/test.desc index 46c2f8cd2d4..4b121b442af 100644 --- a/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/test.desc +++ b/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/test.desc @@ -10,6 +10,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 diff --git a/regression/goto-instrument/precise-const-fp-only-remove-const/test.desc b/regression/goto-instrument/precise-const-fp-only-remove-const/test.desc index cdf49005c0b..a5698a20b9a 100644 --- a/regression/goto-instrument/precise-const-fp-only-remove-const/test.desc +++ b/regression/goto-instrument/precise-const-fp-only-remove-const/test.desc @@ -2,5 +2,7 @@ CORE main.c --verbosity 10 --pointer-check --remove-const-function-pointers ^\s*f2\(\); +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-instrument/precise-const-fp-remove-all-fp/test.desc b/regression/goto-instrument/precise-const-fp-remove-all-fp/test.desc index a559b2b1747..20e26789801 100644 --- a/regression/goto-instrument/precise-const-fp-remove-all-fp/test.desc +++ b/regression/goto-instrument/precise-const-fp-remove-all-fp/test.desc @@ -2,5 +2,7 @@ CORE main.c --verbosity 10 --pointer-check --remove-function-pointers ^\s*f2\(\); +^EXIT=0$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-instrument/unwind-assert2/test.desc b/regression/goto-instrument/unwind-assert2/test.desc index 1c4d4739f3a..10b5fdc40dd 100644 --- a/regression/goto-instrument/unwind-assert2/test.desc +++ b/regression/goto-instrument/unwind-assert2/test.desc @@ -1,6 +1,7 @@ CORE main.c --unwind 9 --unwinding-assertions +^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -- diff --git a/regression/goto-instrument/unwind-assume1/test.desc b/regression/goto-instrument/unwind-assume1/test.desc index 178d0f4fbd6..b7edd8e4152 100644 --- a/regression/goto-instrument/unwind-assume1/test.desc +++ b/regression/goto-instrument/unwind-assume1/test.desc @@ -1,6 +1,7 @@ CORE main.c --unwind 10 +^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -- diff --git a/regression/test-script/excluded-line/test.desc b/regression/test-script/excluded-line/test.desc index 7fa478ad232..4a566861e89 100644 --- a/regression/test-script/excluded-line/test.desc +++ b/regression/test-script/excluded-line/test.desc @@ -2,5 +2,7 @@ CORE test.txt ^Hello$ +^EXIT=0$ +^SIGNAL=0$ -- ^Goodbye$ diff --git a/regression/test-script/multi-line/test.desc b/regression/test-script/multi-line/test.desc index 2ef644c2082..3e872a0080d 100644 --- a/regression/test-script/multi-line/test.desc +++ b/regression/test-script/multi-line/test.desc @@ -3,4 +3,6 @@ test.txt activate-multi-line-match Hello\nWorld +EXIT=0\n +SIGNAL=0\n -- diff --git a/regression/test-script/single-line-windows-line-ends/test.desc b/regression/test-script/single-line-windows-line-ends/test.desc index d7c83bd851e..7bce1e7408d 100644 --- a/regression/test-script/single-line-windows-line-ends/test.desc +++ b/regression/test-script/single-line-windows-line-ends/test.desc @@ -2,4 +2,6 @@ CORE test.txt ^Hello$ +^EXIT=0$ +^SIGNAL=0$ -- diff --git a/regression/test-script/single-line/test.desc b/regression/test-script/single-line/test.desc index d7c83bd851e..7bce1e7408d 100644 --- a/regression/test-script/single-line/test.desc +++ b/regression/test-script/single-line/test.desc @@ -2,4 +2,6 @@ CORE test.txt ^Hello$ +^EXIT=0$ +^SIGNAL=0$ -- From 706ffa78ddcff88565914605b0b190adfc4f7d8c Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 23 Mar 2018 13:32:30 +0000 Subject: [PATCH 2/2] Make test lambda1 compatible with symex-driven loading Previously it didn't have an entry-point, and so relied on the normal load process loading all functions. The added entry-point mimics that behaviour when loading is on-demand. --- regression/cbmc-java/lambda1/B.class | Bin 1349 -> 1226 bytes regression/cbmc-java/lambda1/C.class | Bin 582 -> 458 bytes .../cbmc-java/lambda1/Lambdatest$A.class | Bin 401 -> 328 bytes regression/cbmc-java/lambda1/Lambdatest.class | Bin 4959 -> 4192 bytes regression/cbmc-java/lambda1/Lambdatest.java | 17 +++++++++++++++-- regression/cbmc-java/lambda1/test.desc | 7 ++++++- 6 files changed, 21 insertions(+), 3 deletions(-) diff --git a/regression/cbmc-java/lambda1/B.class b/regression/cbmc-java/lambda1/B.class index ee0d07a678c0a5129273c7af562f1ebb91bc452a..8d177c6dc03b161a696191e2b05d8b6eca17492b 100644 GIT binary patch delta 359 zcmZ8ayG{a85Iy(qvddm>;s#JbL4$74 zNtyZ3Trg2KQMqw%6I$O381!%mvpp|3@sIi= z1{Q5BQES@BNGxMTy|H7hg|@2lI$Ko-yq0h!*03cpj*PnIZMLmG_$S*@1MT864@LlD z&Lh|z4Gd|jMkI#TD8{I!NGpO9$a8Y{;D1>WsU~8G+ai4On=e6+u1MzrS{nN46O6&X l4>28aWYw46s7#Q>k;5i+L5u6?U;|kch)d!{XqZI_b3ai}Fs%Rp delta 452 zcmYk1J5K^Z6ot?1E{|O{k*o+Rh@zsf@(|^rA`ejt6H2894N)QqiBQ;CnAlhtGC#vc z3m>sCHa7eVOA8Z!f${D_BF&k5@0|JWnZEp?Wct6aZvc`gD^L)SA!A;_0v4@BInaN< z(%MEB)X1}9Tt;k&+7Rny?h;z1eOzx<>*vk-QLAxa2!qr;ZFU&MN-0a)X>@56+7DM5 z*hTL<$29I{1xH-PDiSKzu+D4D?Myn68nYtpgil2V8~mD`h@05rKP<|!+%H5N+bVL{ zQQ?J;9||e9%Ws4)X^$buKLroJ6>FDq&=v}6(VxK{s1V>HwVFeQ398kB0d9DxW0=Gg z={VJSatnrA_dY`Sf328P8!WJ!1oyx-BpCE*gX&aJrf5T08j`t4)t?}`Af3IydQb4t qK+;Gcl^`>8Z-<|Eq*!>?^vzESQsSP8Kl@5q}dr{CMswt2>IkEC+37D z7G)+T<)nsy2u22$l8nq^Mh0ddXX}X`$`Xv3j10m)S&3zd`ZH3~|C8_DDMb;BD zr!n&}@K0u9bgb8BU<5)223D=@42&Cr3?>FHAjt+63}D~}vUwm1fHW_V$H)NG3M4s! zY%?Iu1f-c*)__PPok3uoVh~xVPLK)#20;c!0Y{)2LSQpI7#NI!!XQI9wX_c~Fl}RC XMmG!D6`WABm>7h?Hi|Haf@v`Te-b3? diff --git a/regression/cbmc-java/lambda1/Lambdatest$A.class b/regression/cbmc-java/lambda1/Lambdatest$A.class index 71fae8c53b3a761a908f28c6e739fed80a8b05ad..0556baf0fb4f40f3433d1a6a3a1587e711c3212e 100644 GIT binary patch delta 141 zcmbQpe1b{p)W2Q(7#J8#7$i6um>KxF7+4qt*cpV_8AK;ag-zU`rY6SDAkN6ZvCfjpo> gAjt-#85mfB^1MKriGhzn1W0oMMVT1{8H5=a02Kfi6#xJL delta 213 zcmYk0u?m7v7=_QhT9%lVmX)myQEOWuNK+uRgwS{`A;Ap1zKD;~5J5z9^ia`XE%Cz# z=R0TkAG}oD=j(b0FvGA81sxqKx*B>K`lTCsR&d;kG!%IvqBLHAz@QfUL^3d+!B}Ql zoG(%#WlYKp0&$3TqKIWN^5akUg)wUY3rLNL6DI5Dxld&~6W6P2wjYuGA zvouSaec!h(>6$i6!GLKgZL^)6{!Kmo?#x&k!`RTC{xEm$opsK$fBJrqR^ zPKfHm^@!tbip!yW_!CcNP^kJFJ{#@1ht_ z3@g<1=QGT*F>U3{eWj@pvv9x|$?}UDXS8vjugk=WikLV|Z&QYqll6OiRUWbnR&G2c+Z)O{Jsq2hZB>W|qWBEwkSliC*bNn7GPb26 zOvE-<1S_^lArT)8zzQz)TwG%@CY=h3>x!XtFU6esU~GfJc0bsHJsTXAA8I|b8_Jgo zqvn7m=b^E3qSna_(6J5M6(YOydAn#AjOo3meKembHrC$m}1HM}QFZz(LhWXMGDKCM59V85t*sNo}dzpvwC z{G1EF5b2jXeuYmOHT+tn-{>6LTXg&uoA~K>I)3jkf1vQGjz8j0jJ@K$nj=(9s8m+%II0keh@I2sw#U^Kkc%OqioKM{flx))&GIPG58! zT*Xx4u*~l>3bj`8zC6!QB%YWzfH}do`FGf}^L5J{(xsmS`YfT1>FMlog$_bH6_(L{-ThK`|gs|JA~d3)zSL3Y`@%R_<7S((G~jmuK7!E}Fa6NxR*7D&{KxC@ybN|x;%p=p%Uft!$9KHz zBx)joB36|T*E>w1NN?65G6!SaMv_+(w4*CL+JAmI+$Nn zihLEJmM;qBCbovb#F<=zK)g0QxO*9n1hj>4^#a#KxMsrnw$52<;L^g;x_jD97whO^ z6WZ82F?NrV%PAo8va74FAoA^m?IrAu1iG0U>~3_Ng^&_OzQi?2ZzEb}(E1s_xsB$w z$sS6BxYe`jX0~G0CjaUjUB8UnNBPr&JgJVw&q<} ziD9hfI8EXZHgL9X#o~y>gh`?nv<{?qKup zBo3$X<#A@PItZtSIO~bCfjAuP9!`0$ym+D~an;dzQMmPs(~7r(XSLcZ_)^cRF36-K z5|Z1*GwJk9LSoVyq~A_`UO|B_XcJ`8OcP#R7n^j=V2!xBKOm71O?c&bCarwStgNcJ zxMAwKO^0O#_n?b!`QIMr+(?lB2foHXx!w1Yzmr@4L+aj#`(Zd-1}4TFE{|zE;Bm*w R-0?E^qcZnsnR^Tm{0A@bwZ;Gd literal 4959 zcmb_g`CA*;6+KS^#z+H<)Qr2ZoPa`6daKfW(m*K&0~r~V<8V+ha5;ep9*g5scszzUo=6~y zC#Cn91RC&^h<>gad+_-L8f9qU=>(eaRDwNs_$32hj-eA@iQ}vIn&5vuhHu~r1K%|8 ztbuPSsN)LeRH2Y9P2}xzIa^j}nyZwZ;)+7+^n}}+wpV5|_J~6BOm3lIJC#ya;hwt1 z(di}ovOSo$3k!o&1t+_ZEsczEN7T+_6n1;76(^S;oUat-oLsRmIG#J{cPaPK))G4W z$$ZgvMnd$3ObG?`7=Kgz*Xv(OODgy>@|(%3OQ$t!&Lf$Lc>HcLo3^+ zbA{}g%F1lEbl#rLb0#reoU`*6>{3p~{$zu*n4{-R4PL+(Xjn?4^)}Qu^-o&EsCt+1 zR}{8uD;_%M*A#YW^R*pOI$xoq-h#E&suj=vAGp5zliI|{d4=J3z^g6-(>(U5v$D!| zrIJ_J<$0yv&sr3o*lJz3tm@JbFS{X^V*sV5T=nzCB9CN=zh(YNLNT)xlcHU>YO+{i zG>xPuCBSN_&HzTz@UL2%F+u=^IAyw z2V~(z?taO_c@g=Mfgj8FMH4^4Pr2|j8U5VEFYwDY1HY2duTAX7fQcjM=hSaZjJTcO za_~D7FN2|H)zo;AXX5wxgMn9s^>Zd(#cKv$rypvj*KImGyOf=Cqz<|v=T+Gl{)nqL zg}Wy>lD-(@9d=EjF;{-1$o#NU>AGu$Mf5@aApLz>P*jm_of7DELffmWc~-<;Lc8YG zXMf!-v};QNg?%Ah^bqpNi011Ghji&`UWJm-N>FzQh3YcPK(63iu=5p$AFrt?QS^qw z9+sLg+p7EMMdPyUI?H0(5eV0nN`bne(4W$;u&q&L%Z4;>O7ka{yo_6A;~BS@)p#

f z++9P+6)qQ-vx8m$G6U^-d(J7A7y$8=+Q`5^c;inOi^~;W4*$^)$_Mb0_mo}8Z9LCg_1!IcD!1ON$DFTr!p`Ssa!z){z&{oC-r|rjdlc^4S`NKD z*xh`xHuA@k#V6}t_9EEFmgOoKr#WWjVhbrU?w19O-yM`;U1WQRqglRS6~C#z>rj0g zM8Y*h*=dkYW1khfhNiwZVLW^t+peMcHOfYCm~Ds4Axgn!v>?WD96e~|!x}I>Obp?E zjualigWM(h=Bba+FbDeg-#{#izasuB$59uv$=$cz#pv_odGB)%umXOmfL|)$m*N?Wa<7G*7-z46yW22xKwaR({fu_XoXp!U(Y6rG;dX!Hg&dVLz!Ei}9tkH!ZA8qd=ValjC1Gz*P( z(&!)!EiK%oRxWMs9WP%7NbLZr9Y#0FB}q#1#q-oqKyfIbxYs?Snx`yA_9=K2rvr+* zrvi$1-iD`+kj^ma9MfpLQ%{}786KM?*dz~3Lcn?*JNx}m?OaFKE1dI+hL_-zuC@+O zHZat*#qKBNNzcRVi*xv7Hb|U<)OPP}YvX0^YYR@)w=HoM zI~MCK@=i3RdCLmCWx0h=yu~+yk9gd7eT$FS6b9F;!Lgw?nNVuP3xn&>;9A_G&cmgLtJL^7x*4u-9lM0yr4Yx(>fjz>qq!E;pR|nb}_s=H^L+urBswRy9C`FYcU}Iw%Ws&LofS(!QXkmbt23D oIc#%p foo = (y) -> y * a.x; return foo.apply(x); } - + public int l(int x) { b.y = 10; Function foo = (y) -> { @@ -75,6 +75,19 @@ public int capture2(Float a) { public boolean custom(Integer i) { return custom.is_ok(i); } + + public static void main(String[] args) { + // Uses all of the above test functions, to ensure they are loaded under + // symex-driven loading: + + Lambdatest lt = new Lambdatest(); + lt.f(0.0f, 0, 0); + lt.i(0); + lt.j(0); + lt.k(0); + lt.l(0); + lt.m(0); + } } class C implements CustomLambda { diff --git a/regression/cbmc-java/lambda1/test.desc b/regression/cbmc-java/lambda1/test.desc index 0895e3afe64..f94b77de051 100644 --- a/regression/cbmc-java/lambda1/test.desc +++ b/regression/cbmc-java/lambda1/test.desc @@ -1,6 +1,6 @@ CORE Lambdatest.class ---verbosity 10 --show-goto-functions +--verbosity 10 --show-goto-functions --function Lambdatest.main lambda function reference lambda\$new\$0 in class \"Lambdatest\" lambda function reference lambda\$new\$1 in class \"Lambdatest\" lambda function reference lambda\$f\$2 in class \"Lambdatest\" @@ -12,3 +12,8 @@ lambda function reference lambda\$m\$7 in class \"Lambdatest\" lambda function reference lambda\$static\$0 in class \"B\" ^EXIT=0$ ^SIGNAL=0$ +-- +-- +Incompatible with symex-driven lazy loading because this test wants to process +everything in the given class, not the functions reachable from a particular +entry point, which is required for symex-driven loading.