]> gcc.gnu.org Git - gcc.git/commit
[Ada] Raise Constraint_Error when converting negative values to Char_Code
authorPiotr Trojanek <trojanek@adacore.com>
Tue, 18 Jan 2022 22:04:12 +0000 (23:04 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Mon, 9 May 2022 09:27:38 +0000 (09:27 +0000)
commitc32983082576e1452a19bc7df8901d6e6d9229c2
treebc408321616b89794a134c0380daf7efd921e6bd
parent5c8053df7b7cbb9709aec0f295c4d0b8c7251f7f
[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.
gcc/ada/uintp.adb
This page took 0.057899 seconds and 6 git commands to generate.