Merge pull request #1905 from smowton/smowton/cleanup/broken-regression-tests

Fix broken test descriptions

Author: smowton

regression/ansi-c/Forward_Declaration2/test.desc

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

regression/ansi-c/Incomplete_Type1/test.desc

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

regression/ansi-c/function_return1/test.desc

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

regression/ansi-c/static2/test.desc

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

regression/ansi-c/static3/test.desc

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

regression/cbmc-java/NondetArray/test.desc

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

regression/cbmc-java/NondetArray2/test.desc

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

regression/cbmc-java/NondetArray3/test.desc

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

regression/cbmc-java/NondetArray4/test.desc

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

regression/cbmc-java/NondetAssume1/test.desc

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

regression/cbmc-java/NondetAssume2/test.desc

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

regression/cbmc-java/NondetBoolean/test.desc

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

regression/cbmc-java/NondetByte/test.desc

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

regression/cbmc-java/NondetCastToObject/test.desc

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

regression/cbmc-java/NondetChar/test.desc

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

regression/cbmc-java/NondetDirectFromMethod/test.desc

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

regression/cbmc-java/NondetDouble/test.desc

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

regression/cbmc-java/NondetFloat/test.desc

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

regression/cbmc-java/NondetGenericArray/test.desc

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

regression/cbmc-java/NondetGenericRecursive/test.desc

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

regression/cbmc-java/NondetGenericRecursive2/test.desc

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

regression/cbmc-java/NondetGenericWithNull/test.desc

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

regression/cbmc-java/NondetGenericWithoutNull/test.desc

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

regression/cbmc-java/NondetInit/test.desc

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

regression/cbmc-java/NondetInit/test_lazy.desc

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

regression/cbmc-java/NondetInit2/test.desc

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

regression/cbmc-java/NondetInit3/test.desc

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

regression/cbmc-java/NondetInt/test.desc

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

regression/cbmc-java/NondetLong/test.desc

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

regression/cbmc-java/NondetShort/test.desc

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

regression/cbmc-java/address_space_size_limit1/test.desc

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

regression/cbmc-java/array2/test.desc

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

regression/cbmc-java/exceptions26/test.desc

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

regression/cbmc-java/exceptions27/test.desc

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

regression/cbmc-java/inherited_static_field1/test.desc

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

regression/cbmc-java/inherited_static_field10/test.desc

@@ -4,6 +4,8 @@ Test.class
 Stub static field x found for non-stub type java::Test\. In future this will be a fatal error\.
 assertion at file Test\.java line 6 .* FAILURE
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 Stub static field x found for non-stub type java::Parent\. In future this will be a fatal error\.
 --

regression/cbmc-java/inherited_static_field2/test.desc

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

regression/cbmc-java/inherited_static_field3/test.desc

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

regression/cbmc-java/inherited_static_field4/test.desc

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

regression/cbmc-java/inherited_static_field5/test.desc

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

regression/cbmc-java/inherited_static_field6/test.desc

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

regression/cbmc-java/inherited_static_field7/test.desc

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

regression/cbmc-java/inherited_static_field8/test.desc

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

regression/cbmc-java/inherited_static_field9/test.desc

@@ -5,6 +5,8 @@ Stub static field x found for non-stub type java::Test\. In future this will be
 Stub static field x found for non-stub type java::Parent\. In future this will be a fatal error\.
 assertion at file Test\.java line 6 .* FAILURE
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 --
 This tests the corner case where static fields are found on non-stub types, here caused

regression/cbmc-java/lambda1/B.class

@@ -36,11 +36,11 @@ public int j(int x) {
 
     public int k(int x) {
         a.x = 10;
-        
+
         Function<Integer, Integer> foo = (y) -> y * a.x;
         return foo.apply(x);
     }
-    
+
     public int l(int x) {
         b.y = 10;
         Function<Integer, Integer> 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<Integer> {