Update tests and add failure test

Author: tjj2017

testsuite/gnat2goto/tests/separate_subprog_assert_check/p.adb

@@ -0,0 +1,17 @@
+--  Use *.asu file extension for a subunit so that it is not included as a
+--  a top level unit to be analysed using by the regression test system.
+--  The gnat front-end will automatically analyse the subunit when it
+--  encounters the sybprogram_body_stub.
+pragma Source_File_Name (
+			 Subunit_File_Name  => "*.asu",
+			Dot_Replacement => "-");
+
+procedure P (X : in out integer) is
+   procedure Inc (N : in out Integer) is separate;
+   Old_X : constant Integer := X;
+begin
+   Inc (X);
+   --  The following assert should succeed if the possibility
+   --  overflow is ignored.
+   pragma Assert (X = Old_X + 1);
+end P;

testsuite/gnat2goto/tests/separate_subprog_assert_check/test.opt

@@ -0,0 +1 @@
+ALL XFAIL Assert statement in p.adb should succeed.

testsuite/gnat2goto/tests/separate_subprog_assert_check/test.out

@@ -0,0 +1,3 @@
+[2] file p-inc.asu line 6 assertion: SUCCESS
+[1] file p.adb line 16 assertion: SUCCESS
+VERIFICATION SUCCEEDED

testsuite/gnat2goto/tests/separate_subprog_assert_check/test.py

@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()