2017-01-23 Claire Dross <dross@adacore.com>

	* exp_spark.adb (Expand_SPARK_Attribute_Reference):  For
	attributes which return Universal_Integer, introduce a conversion
	to the expected type with the appropriate check flags set.
	* sem_res.adb (Resolve_Range): The higher bound can be in Typ's
	base type if the range is null. It may still be invalid if it
	is higher than the lower bound. This is checked later in the
	context in which the range appears.

2017-01-23  Pierre-Marie de Rodat  <derodat@adacore.com>

	* scos.ads: Introduce a constant to represent ignored
	dependencies in SCO_Unit_Table_Entry.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@244776 138bc75d-0d04-0410-961f-82ee72b054a4

4 files changed, 55 insertions, 3 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 76ee520f0b4..c2780aeeeb7 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,18 @@
+2017-01-23  Claire Dross  <dross@adacore.com>
+
+	* exp_spark.adb (Expand_SPARK_Attribute_Reference):  For
+	attributes which return Universal_Integer, introduce a conversion
+	to the expected type with the appropriate check flags set.
+	* sem_res.adb (Resolve_Range): The higher bound can be in Typ's
+	base type if the range is null. It may still be invalid if it
+	is higher than the lower bound. This is checked later in the
+	context in which the range appears.
+
+2017-01-23  Pierre-Marie de Rodat  <derodat@adacore.com>
+
+	* scos.ads: Introduce a constant to represent ignored
+	dependencies in SCO_Unit_Table_Entry.
+
 2017-01-23  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* exp_ch9.adb (Expand_N_Protected_Type_Declaration): Remove extra
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 5b002ca86ee..9861c625f4b 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -24,6 +24,7 @@
 ------------------------------------------------------------------------------
 
 with Atree;    use Atree;
+with Checks;   use Checks;
 with Einfo;    use Einfo;
 with Exp_Ch5;  use Exp_Ch5;
 with Exp_Dbug; use Exp_Dbug;
@@ -148,6 +149,29 @@ package body Exp_SPARK is
                New_Occurrence_Of (RTE (RE_To_Address), Loc),
              Parameter_Associations => New_List (Expr)));
          Analyze_And_Resolve (N, Typ);
+
+      --  For attributes which return Universal_Integer, introduce a conversion
+      --  to the expected type with the appropriate check flags set.
+
+      elsif Attr_Id = Attribute_Alignment
+        or else Attr_Id = Attribute_Bit
+        or else Attr_Id = Attribute_Bit_Position
+        or else Attr_Id = Attribute_Descriptor_Size
+        or else Attr_Id = Attribute_First_Bit
+        or else Attr_Id = Attribute_Last_Bit
+        or else Attr_Id = Attribute_Length
+        or else Attr_Id = Attribute_Max_Size_In_Storage_Elements
+        or else Attr_Id = Attribute_Pos
+        or else Attr_Id = Attribute_Position
+        or else Attr_Id = Attribute_Range_Length
+        or else Attr_Id = Attribute_Object_Size
+        or else Attr_Id = Attribute_Size
+        or else Attr_Id = Attribute_Value_Size
+        or else Attr_Id = Attribute_VADS_Size
+        or else Attr_Id = Attribute_Aft
+        or else Attr_Id = Attribute_Max_Alignment_For_Allocation
+      then
+         Apply_Universal_Integer_Attribute_Checks (N);
       end if;
    end Expand_SPARK_Attribute_Reference;
 
diff --git a/gcc/ada/scos.ads b/gcc/ada/scos.ads
index da5cc47c5ad..61f6efe2397 100644
--- a/gcc/ada/scos.ads
+++ b/gcc/ada/scos.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2009-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 2009-2016, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -497,6 +497,11 @@ package SCOs is
    --  Used to index values in this table. Values start at 1 and are assigned
    --  sequentially as entries are constructed.
 
+   Missing_Dep_Num : constant Nat := 0;
+   --  Represents a dependency number for a dependency that is ignored. SCO
+   --  information consumers use this to strip units that must be kept out of
+   --  the coverage analysis.
+
    type SCO_Unit_Table_Entry is record
       File_Name : String_Ptr;
       --  Pointer to file name in ALI file
@@ -505,7 +510,9 @@ package SCOs is
       --  Index for the source file
 
       Dep_Num : Nat;
-      --  Dependency number in ALI file
+      --  Dependency number in ALI file. This is a positive number when the
+      --  dependency is actually available in the context, it is
+      --  Missing_Dep_Num otherwise.
 
       From : Nat;
       --  Starting index in SCO_Table of SCO information for this unit
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 58ee4036948..e2c65f15e0a 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -9617,8 +9617,14 @@ package body Sem_Res is
 
    begin
       Set_Etype (N, Typ);
+
+      --  The lower bound should be in Typ. The higher bound can be in Typ's
+      --  base type if the range is null. It may still be invalid if it is
+      --  higher than the lower bound. This is checked later in the context in
+      --  which the range appears.
+
       Resolve (L, Typ);
-      Resolve (H, Typ);
+      Resolve (H, Base_Type (Typ));
 
       --  Check for inappropriate range on unordered enumeration type