Add test case for handling subprogram_body_stub

Author: tjj2017

testsuite/gnat2goto/tests/separate_subprog/p-inc.asu

@@ -0,0 +1,7 @@
+separate (P)
+procedure Inc (N : in out Integer) is
+   Old_N : constant Integer := N;
+begin
+   N := N + 1;
+   pragma Assert (N = Old_N + 1);
+end Inc;

testsuite/gnat2goto/tests/separate_subprog/p.adb

@@ -0,0 +1,15 @@
+--  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);
+   pragma Assert (X = Old_X + 1);
+end P;

testsuite/gnat2goto/tests/separate_subprog/test.out

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

testsuite/gnat2goto/tests/separate_subprog/test.py

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