[Ada] Split spec and body of expression function with Subprogram_Variant

gcc/ada/

	* libgnat/s-valuti.ads (Scan_Natural_Ghost): Split body from
	spec and put it into private part, so that GNATprove can pick it
	both when analysing the unit and its clients.

diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads
index 388a884c8e8a4bce425c4677a68f930c3793fb53..7483f2c0c0344034fd064fc52d9c6fe6da8c4d15 100644 (file)
--- a/gcc/ada/libgnat/s-valuti.ads
+++ b/gcc/ada/libgnat/s-valuti.ads
@@ -218,21 +218,6 @@ is
       P   : Natural;
       Acc : Natural)
       return Natural
-   is
-     (if Str (P) = '_' then
-        Scan_Natural_Ghost (Str, P + 1, Acc)
-      else
-        (declare
-           Shift_Acc : constant Natural :=
-             Acc * 10 + (Character'Pos (Str (P)) - Character'Pos ('0'));
-         begin
-           (if P = Str'Last
-              or else Str (P + 1) not in '0' .. '9' | '_'
-              or else Shift_Acc >= Integer'Last / 10
-            then
-              Shift_Acc
-            else
-              Scan_Natural_Ghost (Str, P + 1, Shift_Acc))))
    with
      Ghost,
      Subprogram_Variant => (Increases => P),
@@ -352,4 +337,31 @@ is
    --  no check for this case, the caller must ensure this condition is met.
    pragma Warnings (GNATprove, On, """Ptr"" is not modified");
 
+private
+
+   ------------------------
+   -- Scan_Natural_Ghost --
+   ------------------------
+
+   function Scan_Natural_Ghost
+     (Str : String;
+      P   : Natural;
+      Acc : Natural)
+      return Natural
+   is
+     (if Str (P) = '_' then
+        Scan_Natural_Ghost (Str, P + 1, Acc)
+      else
+        (declare
+           Shift_Acc : constant Natural :=
+             Acc * 10 + (Character'Pos (Str (P)) - Character'Pos ('0'));
+         begin
+           (if P = Str'Last
+              or else Str (P + 1) not in '0' .. '9' | '_'
+              or else Shift_Acc >= Integer'Last / 10
+            then
+              Shift_Acc
+            else
+              Scan_Natural_Ghost (Str, P + 1, Shift_Acc))));
+
 end System.Val_Util;