diff mbox series

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

Message ID 20211202162849.GA2158494@adacore.com
State New
Headers show
Series [Ada] Split spec and body of expression function with Subprogram_Variant | expand

Commit Message

Pierre-Marie de Rodat Dec. 2, 2021, 4:28 p.m. UTC 
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.
diff mbox series

Patch

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;