[gcc r13-201] [Ada] Raise Constraint_Error when converting negative values to Char_Code

[gcc r13-201] [Ada] Raise Constraint_Error when converting negative values to Char_Code

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:c32983082576e1452a19bc7df8901d6e6d9229c2

commit r13-201-gc32983082576e1452a19bc7df8901d6e6d9229c2
Author: Piotr Trojanek <trojanek@adacore.com>
Date:   Tue Jan 18 23:04:12 2022 +0100

    [Ada] Raise Constraint_Error when converting negative values to Char_Code
    
    GNATprove relies on the comment for Get_Enum_Lit_From_Pos, which
    promises to raise Constraint_Error when its Pos parameter is not among
    the representation values for enumeration literal. However, this promise
    was only respected in builds with range checks enabled.
    
    The root problem was that a similar comment for conversion from Uint to
    Char_Code was likewise only respected in builds with range checks
    enabled.
    
    Now both routines respect promises in their comments. The behaviour of
    GNAT itself is not affected. The fix is needed to filter garbage
    counterexamples generated by provers for characters objects in SPARK.
    
    gcc/ada/
    
            * uintp.adb (UI_To_CC): Guard against illegal inputs; reuse
            UI_To_Int.

Diff:
---
 gcc/ada/uintp.adb | 29 ++++++++---------------------
 1 file changed, 8 insertions(+), 21 deletions(-)

diff --git a/gcc/ada/uintp.adb b/gcc/ada/uintp.adb
index 854d2e167b0..921c1d27956 100644
--- a/gcc/ada/uintp.adb
+++ b/gcc/ada/uintp.adb
@@ -2233,30 +2233,17 @@ package body Uintp is
 
    function UI_To_CC (Input : Valid_Uint) return Char_Code is
    begin
-      if Direct (Input) then
-         return Char_Code (Direct_Val (Input));
+      --  Char_Code and Int have equal upper bounds, so simply guard against
+      --  negative Input and reuse conversion to Int. We trust that conversion
+      --  to Int will raise Constraint_Error when Input is too large.
 
-      --  Case of input is more than one digit
+      pragma Assert
+        (Char_Code'First = 0 and then Int (Char_Code'Last) = Int'Last);
 
+      if Input >= Uint_0 then
+         return Char_Code (UI_To_Int (Input));
       else
-         declare
-            In_Length : constant Int := N_Digits (Input);
-            In_Vec    : UI_Vector (1 .. In_Length);
-            Ret_CC    : Char_Code;
-
-         begin
-            Init_Operand (Input, In_Vec);
-
-            --  We assume value is positive
-
-            Ret_CC := 0;
-            for Idx in In_Vec'Range loop
-               Ret_CC := Ret_CC * Char_Code (Base) +
-                                  Char_Code (abs In_Vec (Idx));
-            end loop;
-
-            return Ret_CC;
-         end;
+         raise Constraint_Error;
       end if;
    end UI_To_CC;