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

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

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 526 bytes --]

Due to a latent bug with freezing, the expression function with
Subprogram_Variant which was recently added to the System.Val_Util unit
triggers a crash in CodePeer.

Ordinary compilation was not affected by this bug, because of the
Assertion_Policy (Ghost => Ignore) applied to this unit.

Tested on x86_64-pc-linux-gnu, committed on trunk

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.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 1735 bytes --]

diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads
--- 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;