From: Piotr Trojanek <trojanek@adacore.com>
Date: Fri, 12 Jun 2020 17:06:51 +0000 (+0200)
Subject: [Ada] Add range check for GNATprove on 'Pos to Long_Integer conversion
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=df81923f6d805ebf390e116b1902d0c8ec93c477;p=gcc.git

[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.
---

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 6454902f06b..b400268ac5b 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;