[multiple changes]

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.

From-SVN: r244776

gcc/ada/ChangeLog

+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

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;
 

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

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