diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2021-11-22 21:12:41 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-12-02 16:26:23 +0000 |
| commit | a83c4eea27122fe2f90ff35d813ca34e8f542387 (patch) | |
| tree | 80507ed9e3ff54d38edad511842fa7f673cc47ad /gcc/ada/libgnat | |
| parent | d43fbe0151b8efcb452970a92c31f52d64d0003e (diff) | |
| download | gcc-a83c4eea27122fe2f90ff35d813ca34e8f542387.zip gcc-a83c4eea27122fe2f90ff35d813ca34e8f542387.tar.gz gcc-a83c4eea27122fe2f90ff35d813ca34e8f542387.tar.bz2 | |
[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.
Diffstat (limited to 'gcc/ada/libgnat')
| -rw-r--r-- | gcc/ada/libgnat/s-valuti.ads | 42 |
1 files changed, 27 insertions, 15 deletions
diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads index 388a884..7483f2c 100644 --- 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; |