[gcc(refs/users/aoliva/heads/testme)] [Ada] Add range check for GNATprove on 'Pos to Long_Integer conversion

[Alexandre Oliva]

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

commit df81923f6d805ebf390e116b1902d0c8ec93c477
Author: Piotr Trojanek <trojanek@adacore.com>
Date:   Fri Jun 12 19:06:51 2020 +0200

    [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:
---
 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 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;