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/B.class b/regression/cbmc-java/lambda1/B.class index ee0d07a678c..8d177c6dc03 100644 Binary files a/regression/cbmc-java/lambda1/B.class and b/regression/cbmc-java/lambda1/B.class differ diff --git a/regression/cbmc-java/lambda1/C.class b/regression/cbmc-java/lambda1/C.class index 710b045719f..44f19f094e6 100644 Binary files a/regression/cbmc-java/lambda1/C.class and b/regression/cbmc-java/lambda1/C.class differ diff --git a/regression/cbmc-java/lambda1/Lambdatest$A.class b/regression/cbmc-java/lambda1/Lambdatest$A.class index 71fae8c53b3..0556baf0fb4 100644 Binary files a/regression/cbmc-java/lambda1/Lambdatest$A.class and b/regression/cbmc-java/lambda1/Lambdatest$A.class differ diff --git a/regression/cbmc-java/lambda1/Lambdatest.class b/regression/cbmc-java/lambda1/Lambdatest.class index 4dbc3b78291..506d117020a 100644 Binary files a/regression/cbmc-java/lambda1/Lambdatest.class and b/regression/cbmc-java/lambda1/Lambdatest.class differ diff --git a/regression/cbmc-java/lambda1/Lambdatest.java b/regression/cbmc-java/lambda1/Lambdatest.java index 0e021165b59..3dce340b8fd 100644 --- a/regression/cbmc-java/lambda1/Lambdatest.java +++ b/regression/cbmc-java/lambda1/Lambdatest.java @@ -36,11 +36,11 @@ public int j(int x) { public int k(int x) { a.x = 10; - + Function 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 9ec5bd91cbd..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\" @@ -10,3 +10,10 @@ 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$ +-- +-- +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. 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$ --