| ------------------------------------------------------------------------------ |
| -- -- |
| -- GNAT RUN-TIME COMPONENTS -- |
| -- -- |
| -- S Y S T E M . W I D T H _ U -- |
| -- -- |
| -- B o d y -- |
| -- -- |
| -- Copyright (C) 1992-2023, Free Software Foundation, Inc. -- |
| -- -- |
| -- GNAT is free software; you can redistribute it and/or modify it under -- |
| -- terms of the GNU General Public License as published by the Free Soft- -- |
| -- ware Foundation; either version 3, or (at your option) any later ver- -- |
| -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- |
| -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- |
| -- or FITNESS FOR A PARTICULAR PURPOSE. -- |
| -- -- |
| -- As a special exception under Section 7 of GPL version 3, you are granted -- |
| -- additional permissions described in the GCC Runtime Library Exception, -- |
| -- version 3.1, as published by the Free Software Foundation. -- |
| -- -- |
| -- You should have received a copy of the GNU General Public License and -- |
| -- a copy of the GCC Runtime Library Exception along with this program; -- |
| -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- |
| -- <http://www.gnu.org/licenses/>. -- |
| -- -- |
| -- GNAT was originally developed by the GNAT team at New York University. -- |
| -- Extensive contributions were provided by Ada Core Technologies Inc. -- |
| -- -- |
| ------------------------------------------------------------------------------ |
| |
| package body System.Width_U is |
| |
| -- Ghost code, loop invariants and assertions in this unit are meant for |
| -- analysis only, not for run-time checking, as it would be too costly |
| -- otherwise. This is enforced by setting the assertion policy to Ignore. |
| |
| pragma Assertion_Policy (Ghost => Ignore, |
| Loop_Invariant => Ignore, |
| Assert => Ignore, |
| Assert_And_Cut => Ignore, |
| Subprogram_Variant => Ignore); |
| |
| function Width (Lo, Hi : Uns) return Natural is |
| |
| -- Ghost code, loop invariants and assertions in this unit are meant for |
| -- analysis only, not for run-time checking, as it would be too costly |
| -- otherwise. This is enforced by setting the assertion policy to |
| -- Ignore. |
| |
| pragma Assertion_Policy (Ghost => Ignore, |
| Loop_Invariant => Ignore, |
| Assert => Ignore); |
| |
| ------------------ |
| -- Local Lemmas -- |
| ------------------ |
| |
| procedure Lemma_Lower_Mult (A, B, C : Big_Natural) |
| with |
| Ghost, |
| Pre => A <= B, |
| Post => A * C <= B * C; |
| |
| procedure Lemma_Div_Commutation (X, Y : Uns) |
| with |
| Ghost, |
| Pre => Y /= 0, |
| Post => Big (X) / Big (Y) = Big (X / Y); |
| |
| procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) |
| with |
| Ghost, |
| Post => X / Y / Z = X / (Y * Z); |
| |
| procedure Lemma_Euclidian (V, Q, F, R : Big_Integer) |
| with |
| Ghost, |
| Pre => F > 0 and then Q = V / F and then R = V rem F, |
| Post => V = Q * F + R; |
| -- Ghost lemma to prove the relation between the quotient/remainder of |
| -- division by F and the value V. |
| |
| ---------------------- |
| -- Lemma_Lower_Mult -- |
| ---------------------- |
| |
| procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is null; |
| |
| --------------------------- |
| -- Lemma_Div_Commutation -- |
| --------------------------- |
| |
| procedure Lemma_Div_Commutation (X, Y : Uns) is null; |
| |
| --------------------- |
| -- Lemma_Div_Twice -- |
| --------------------- |
| |
| procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) is |
| XY : constant Big_Natural := X / Y; |
| YZ : constant Big_Natural := Y * Z; |
| XYZ : constant Big_Natural := X / Y / Z; |
| R : constant Big_Natural := (XY rem Z) * Y + (X rem Y); |
| begin |
| pragma Assert (X = XY * Y + (X rem Y)); |
| pragma Assert (XY = XY / Z * Z + (XY rem Z)); |
| pragma Assert (X = XYZ * YZ + R); |
| pragma Assert ((XY rem Z) * Y <= (Z - 1) * Y); |
| pragma Assert (R <= YZ - 1); |
| pragma Assert (X / YZ = (XYZ * YZ + R) / YZ); |
| pragma Assert (X / YZ = XYZ + R / YZ); |
| end Lemma_Div_Twice; |
| |
| --------------------- |
| -- Lemma_Euclidian -- |
| --------------------- |
| |
| procedure Lemma_Euclidian (V, Q, F, R : Big_Integer) is null; |
| |
| -- Local variables |
| |
| W : Natural; |
| T : Uns; |
| |
| -- Local ghost variables |
| |
| Max_W : constant Natural := Max_Log10 with Ghost; |
| Pow : Big_Integer := 1 with Ghost; |
| T_Init : constant Uns := Uns'Max (Lo, Hi) with Ghost; |
| |
| -- Start of processing for System.Width_U |
| |
| begin |
| if Lo > Hi then |
| return 0; |
| |
| else |
| -- Minimum value is 2, one for space, one for digit |
| |
| W := 2; |
| |
| -- Get max of absolute values |
| |
| T := Uns'Max (Lo, Hi); |
| |
| -- Increase value if more digits required |
| |
| while T >= 10 loop |
| Lemma_Div_Commutation (T, 10); |
| Lemma_Div_Twice (Big (T_Init), Big_10 ** (W - 2), Big_10); |
| |
| T := T / 10; |
| W := W + 1; |
| Pow := Pow * 10; |
| |
| pragma Loop_Invariant (W in 3 .. Max_W + 2); |
| pragma Loop_Invariant (Pow = Big_10 ** (W - 2)); |
| pragma Loop_Invariant (Big (T) = Big (T_Init) / Pow); |
| pragma Loop_Variant (Decreases => T); |
| end loop; |
| |
| declare |
| F : constant Big_Integer := Big_10 ** (W - 2) with Ghost; |
| Q : constant Big_Integer := Big (T_Init) / F with Ghost; |
| R : constant Big_Integer := Big (T_Init) rem F with Ghost; |
| begin |
| pragma Assert (Q < Big_10); |
| Lemma_Euclidian (Big (T_Init), Q, F, R); |
| Lemma_Lower_Mult (Q, Big (9), F); |
| pragma Assert (Big (T_Init) <= Big (9) * F + F - 1); |
| pragma Assert (Big (T_Init) < Big_10 * F); |
| pragma Assert (Big_10 * F = Big_10 ** (W - 1)); |
| end; |
| |
| return W; |
| end if; |
| end Width; |
| |
| end System.Width_U; |
