From df81923f6d805ebf390e116b1902d0c8ec93c477 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Fri, 12 Jun 2020 19:06:51 +0200 Subject: [PATCH] [Ada] Add range check for GNATprove on 'Pos to Long_Integer conversion gcc/ada/ * exp_spark.adb (Expand_SPARK_N_Attribute_Reference) Extend existing workaround to 'Pos. --- gcc/ada/exp_spark.adb | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index 6454902..b400268 100644 --- a/gcc/ada/exp_spark.adb +++ b/gcc/ada/exp_spark.adb @@ -400,13 +400,16 @@ package body Exp_SPARK is -- flag as the compiler assumes attributes always fit in this type. -- Since in SPARK_Mode we do not take Storage_Error into account, we -- cannot make this assumption and need to produce a check. - -- ??? It should be enough to add this check for attributes 'Length - -- and 'Range_Length when the type is as big as Long_Long_Integer. + -- ??? It should be enough to add this check for attributes + -- 'Length, 'Range_Length and 'Pos when the type is as big + -- as Long_Long_Integer. declare Typ : Entity_Id; begin - if Attr_Id = Attribute_Range_Length then + if Attr_Id = Attribute_Range_Length + or else Attr_Id = Attribute_Pos + then Typ := Etype (Prefix (N)); elsif Attr_Id = Attribute_Length then @@ -421,6 +424,9 @@ package body Exp_SPARK is if Present (Typ) and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer) then + -- ??? This should rather be a range check, but this would + -- crash GNATprove which somehow recovers the proper kind + -- of check anyway. Set_Do_Overflow_Check (N); end if; end; -- 2.7.4