[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.
This commit is contained in:
Piotr Trojanek 2022-01-18 23:04:12 +01:00 committed by Pierre-Marie de Rodat
parent 5c8053df7b
commit c329830825

View file

@ -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;