[Ada] Add range check for GNATprove on 'Pos to Long_Integer conversion

Message ID 20200727080551.GA36275@adacore.com
State New
Headers show
Series
  • [Ada] Add range check for GNATprove on 'Pos to Long_Integer conversion
Related show

Commit Message

Pierre-Marie de Rodat July 27, 2020, 8:05 a.m.
In GNAT mode attribute Pos is typically expanded into either a type
conversion (unless applied to enumeration types with custom
representation values) and analysis of this type conversion adds check
flags as required.

In GNATprove mode we expand the attribute with
Apply_Universal_Integer_Attribute_Checks, which adds a type conversion,
but its analysis only adds check flags if the size of the target type is
smaller than the size of universal integer. This should be fixed in the
compiler itself, but we already had a workaround for 'Length and
'Range_Length.

This patch extends the existing workaround to 'Pos, which is enough to
solve the problem in GNATprove; the compiler is not affected by this
patch.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference) Extend
	existing workaround to 'Pos.

Patch

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