2015-03-13 Claire Dross <dross@adacore.com>

	* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Do not inline
	subprograms with unconstrained record parameters containing
	Itype declarations.
	* sinfo.ads Document GNATprove assumption that type should match
	in the AST.
	* sem_ch6.adb (Analyze_Subprogram_Body_Contract):
	Do not check for Refined_Depends and Refined_Globals contracts
	as they are optional.

2015-03-13  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch12.adb (Instantiate_Type): For a floating-point type,
	capture dimension info if any, because the generated subtype
	declaration does not come from source and will not process dimensions.
	* sem_dim,adb (Analyze_Dimension_Extension_Or_Record_Aggregate):
	Do not analyze expressions with an initialization procedure
	because aggregates will have been checked at the point of record
	declaration.

2015-03-13  Robert Dewar  <dewar@adacore.com>

	* aspects.ads, aspects.adb: Add entries for aspect Unimplemented.
	* einfo.ads, einfo.adb (Is_Unimplemented): New flag.
	* sem_ch13.adb: Add dummy entry for aspect Unimplemented.
	* snames.ads-tmpl: Add entry for Name_Unimplemented.



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

12 files changed, 176 insertions, 42 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 3b961475cc4..c3a79af55c0 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,31 @@
+2015-03-13  Claire Dross  <dross@adacore.com>
+
+	* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Do not inline
+	subprograms with unconstrained record parameters containing
+	Itype declarations.
+	* sinfo.ads Document GNATprove assumption that type should match
+	in the AST.
+	* sem_ch6.adb (Analyze_Subprogram_Body_Contract):
+	Do not check for Refined_Depends and Refined_Globals contracts
+	as they are optional.
+
+2015-03-13  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch12.adb (Instantiate_Type): For a floating-point type,
+	capture dimension info if any, because the generated subtype
+	declaration does not come from source and will not process dimensions.
+	* sem_dim,adb (Analyze_Dimension_Extension_Or_Record_Aggregate):
+	Do not analyze expressions with an initialization procedure
+	because aggregates will have been checked at the point of record
+	declaration.
+
+2015-03-13  Robert Dewar  <dewar@adacore.com>
+
+	* aspects.ads, aspects.adb: Add entries for aspect Unimplemented.
+	* einfo.ads, einfo.adb (Is_Unimplemented): New flag.
+	* sem_ch13.adb: Add dummy entry for aspect Unimplemented.
+	* snames.ads-tmpl: Add entry for Name_Unimplemented.
+
 2015-03-13  Gary Dismukes  <dismukes@adacore.com>
 
 	* style.adb (Missing_Overriding): Apply the
diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb
index 19e49b52220..bef432f67ff 100644
--- a/gcc/ada/aspects.adb
+++ b/gcc/ada/aspects.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2010-2014, Free Software Foundation, Inc.         --
+--          Copyright (C) 2010-2015, 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- --
@@ -595,6 +595,7 @@ package body Aspects is
     Aspect_Thread_Local_Storage         => Aspect_Thread_Local_Storage,
     Aspect_Type_Invariant               => Aspect_Invariant,
     Aspect_Unchecked_Union              => Aspect_Unchecked_Union,
+    Aspect_Unimplemented                => Aspect_Unimplemented,
     Aspect_Universal_Aliasing           => Aspect_Universal_Aliasing,
     Aspect_Universal_Data               => Aspect_Universal_Data,
     Aspect_Unmodified                   => Aspect_Unmodified,
diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index 0e01beba7a2..049efae87f1 100644
--- a/gcc/ada/aspects.ads
+++ b/gcc/ada/aspects.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2010-2014, Free Software Foundation, Inc.         --
+--          Copyright (C) 2010-2015, 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- --
@@ -140,6 +140,7 @@ package Aspects is
       Aspect_Synchronization,
       Aspect_Test_Case,                     -- GNAT
       Aspect_Type_Invariant,
+      Aspect_Unimplemented,                 -- GNAT
       Aspect_Unsuppress,
       Aspect_Value_Size,                    -- GNAT
       Aspect_Variable_Indexing,
@@ -369,6 +370,7 @@ package Aspects is
       Aspect_Synchronization           => Name,
       Aspect_Test_Case                 => Expression,
       Aspect_Type_Invariant            => Expression,
+      Aspect_Unimplemented             => Optional_Expression,
       Aspect_Unsuppress                => Name,
       Aspect_Value_Size                => Expression,
       Aspect_Variable_Indexing         => Name,
@@ -490,6 +492,7 @@ package Aspects is
       Aspect_Test_Case                    => Name_Test_Case,
       Aspect_Type_Invariant               => Name_Type_Invariant,
       Aspect_Unchecked_Union              => Name_Unchecked_Union,
+      Aspect_Unimplemented                => Name_Unimplemented,
       Aspect_Universal_Aliasing           => Name_Universal_Aliasing,
       Aspect_Universal_Data               => Name_Universal_Data,
       Aspect_Unmodified                   => Name_Unmodified,
@@ -717,6 +720,7 @@ package Aspects is
       Aspect_SPARK_Mode                   => Never_Delay,
       Aspect_Synchronization              => Never_Delay,
       Aspect_Test_Case                    => Never_Delay,
+      Aspect_Unimplemented                => Never_Delay,
       Aspect_Warnings                     => Never_Delay,
 
       Aspect_Alignment                    => Rep_Aspect,
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 70dc46fc17a..e215df9eb9d 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -584,8 +584,8 @@ package body Einfo is
    --    Is_Static_Type                  Flag281
    --    Has_Nested_Subprogram           Flag282
    --    Uplevel_Reference_Noted         Flag283
+   --    Is_Unimplemented                Flag284
 
-   --    (unused)                        Flag284
    --    (unused)                        Flag285
    --    (unused)                        Flag286
    --    (unused)                        Flag287
@@ -2456,6 +2456,11 @@ package body Einfo is
       return Flag246 (Id);
    end Is_Underlying_Record_View;
 
+   function Is_Unimplemented (Id : E) return B is
+   begin
+      return Flag284 (Id);
+   end Is_Unimplemented;
+
    function Is_Unsigned_Type (Id : E) return B is
    begin
       pragma Assert (Is_Type (Id));
@@ -5398,6 +5403,11 @@ package body Einfo is
       Set_Flag246 (Id, V);
    end Set_Is_Underlying_Record_View;
 
+   procedure Set_Is_Unimplemented (Id : E; V : B := True) is
+   begin
+      Set_Flag284 (Id, V);
+   end Set_Is_Unimplemented;
+
    procedure Set_Is_Unsigned_Type (Id : E; V : B := True) is
    begin
       pragma Assert (Is_Discrete_Or_Fixed_Point_Type (Id));
@@ -8767,6 +8777,7 @@ package body Einfo is
       W ("Is_True_Constant",                Flag163 (Id));
       W ("Is_Unchecked_Union",              Flag117 (Id));
       W ("Is_Underlying_Record_View",       Flag246 (Id));
+      W ("Is_Unimplemented",                Flag284 (Id));
       W ("Is_Unsigned_Type",                Flag144 (Id));
       W ("Is_Valued_Procedure",             Flag127 (Id));
       W ("Is_Visible_Formal",               Flag206 (Id));
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index cd92063e3f4..81a77f972b3 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -2745,8 +2745,8 @@ package Einfo is
 --       including generic formal parameters.
 
 --    Is_Obsolescent (Flag153)
---       Defined in all entities. Set for any entity for which a valid pragma
---       Obsolescent applies.
+--       Defined in all entities. Set for any entity to which a valid pragma
+--       or aspect Obsolescent applies.
 
 --    Is_Only_Out_Parameter (Flag226)
 --       Defined in formal parameter entities. Set if this parameter is the
@@ -3090,6 +3090,10 @@ package Einfo is
 --       as its corresponding record type, but whose parent is the full view
 --       of the parent in the original type extension.
 
+--    Is_Unimplemented (Flag284)
+--       Defined in all entities. Set for any entity to which a valid pragma
+--       or aspect Unimplemented applies.
+
 --    Is_Unsigned_Type (Flag144)
 --       Defined in all types, but can be set only for discrete and fixed-point
 --       type and subtype entities. This flag is only valid if the entity is
@@ -5299,6 +5303,7 @@ package Einfo is
    --    Is_Thunk                            (Flag225)
    --    Is_Trivial_Subprogram               (Flag235)
    --    Is_Unchecked_Union                  (Flag117)
+   --    Is_Unimplemented                    (Flag284)
    --    Is_Visible_Formal                   (Flag206)
    --    Kill_Elaboration_Checks             (Flag32)
    --    Kill_Range_Checks                   (Flag33)
@@ -5784,6 +5789,7 @@ package Einfo is
    --    SPARK_Pragma                        (Node32)
    --    Linker_Section_Pragma               (Node33)
    --    Contract                            (Node34)
+   --    Import_Pragma                       (Node35)   (non-generic case only)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Contains_Ignored_Ghost_Code         (Flag279)
    --    Default_Expressions_Processed       (Flag108)
@@ -5951,6 +5957,7 @@ package Einfo is
    --    Subprograms_For_Type                (Node29)
    --    Linker_Section_Pragma               (Node33)
    --    Contract                            (Node34)
+   --    Import_Pragma                       (Node35)
    --    Has_Invariants                      (Flag232)
    --    Is_Machine_Code_Subprogram          (Flag137)
    --    Is_Pure                             (Flag44)
@@ -6089,6 +6096,7 @@ package Einfo is
    --    SPARK_Pragma                        (Node32)
    --    Linker_Section_Pragma               (Node33)
    --    Contract                            (Node34)
+   --    Import_Pragma                       (Node35)   (non-generic case only)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Contains_Ignored_Ghost_Code         (Flag279)
    --    Delay_Cleanups                      (Flag114)
@@ -6894,6 +6902,7 @@ package Einfo is
    function Is_True_Constant                    (Id : E) return B;
    function Is_Unchecked_Union                  (Id : E) return B;
    function Is_Underlying_Record_View           (Id : E) return B;
+   function Is_Unimplemented                    (Id : E) return B;
    function Is_Unsigned_Type                    (Id : E) return B;
    function Is_Valued_Procedure                 (Id : E) return B;
    function Is_Visible_Formal                   (Id : E) return B;
@@ -7548,6 +7557,7 @@ package Einfo is
    procedure Set_Is_True_Constant                (Id : E; V : B := True);
    procedure Set_Is_Unchecked_Union              (Id : E; V : B := True);
    procedure Set_Is_Underlying_Record_View       (Id : E; V : B := True);
+   procedure Set_Is_Unimplemented                (Id : E; V : B := True);
    procedure Set_Is_Unsigned_Type                (Id : E; V : B := True);
    procedure Set_Is_Valued_Procedure             (Id : E; V : B := True);
    procedure Set_Is_Visible_Formal               (Id : E; V : B := True);
@@ -8352,6 +8362,7 @@ package Einfo is
    pragma Inline (Is_Type);
    pragma Inline (Is_Unchecked_Union);
    pragma Inline (Is_Underlying_Record_View);
+   pragma Inline (Is_Unimplemented);
    pragma Inline (Is_Unsigned_Type);
    pragma Inline (Is_Valued_Procedure);
    pragma Inline (Is_Visible_Formal);
@@ -8807,6 +8818,7 @@ package Einfo is
    pragma Inline (Set_Is_True_Constant);
    pragma Inline (Set_Is_Unchecked_Union);
    pragma Inline (Set_Is_Underlying_Record_View);
+   pragma Inline (Set_Is_Unimplemented);
    pragma Inline (Set_Is_Unsigned_Type);
    pragma Inline (Set_Is_Valued_Procedure);
    pragma Inline (Set_Is_Visible_Formal);
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 9a60befa0bf..7db46cf8178 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -1335,6 +1335,11 @@ package body Inline is
      (Spec_Id : Entity_Id;
       Body_Id : Entity_Id) return Boolean
    is
+      function Has_Parameter_With_Discriminant_Dependent_Fields
+        (Id : Entity_Id) return Boolean;
+      --  Returns true if the subprogram as parameters of an unconstrained
+      --  record types with fields whose types depend on a discriminant.
+
       function Has_Some_Contract (Id : Entity_Id) return Boolean;
       --  Returns True if subprogram Id has any contract (Pre, Post, Global,
       --  Depends, etc.)
@@ -1351,6 +1356,73 @@ package body Inline is
       --  Returns True if subprogram Id was defined originally as an expression
       --  function.
 
+      ------------------------------------------------------
+      -- Has_Parameter_With_Discriminant_Dependent_Fields --
+      ------------------------------------------------------
+
+      function Has_Parameter_With_Discriminant_Dependent_Fields
+        (Id : Entity_Id) return Boolean
+      is
+         E    : Entity_Id := Id;
+         Spec : Node_Id   := Parent (E);
+
+      begin
+         --  Get the specification of the subprogram. Go through alias if
+         --  needed.
+
+         if Nkind (Spec) = N_Defining_Program_Unit_Name then
+            Spec := Parent (Spec);
+         end if;
+
+         while Nkind (Spec) not in N_Subprogram_Specification loop
+            pragma Assert (Present (Alias (E)));
+            E := Alias (E);
+            Spec := Parent (E);
+
+            if Nkind (Spec) = N_Defining_Program_Unit_Name then
+               Spec := Parent (Spec);
+            end if;
+         end loop;
+
+         declare
+            Params   : constant List_Id := Parameter_Specifications (Spec);
+            Param    : Node_Id;
+            Param_Ty : Entity_Id;
+
+         begin
+            if Is_Non_Empty_List (Params) then
+               Param := First (Params);
+               while Present (Param) loop
+                  Param_Ty := Etype (Defining_Identifier (Param));
+
+                  --  If the parameter is an unconstrained record, check if
+                  --  it has components whose types depend on a discriminant.
+
+                  if Is_Record_Type (Param_Ty)
+                    and then not Is_Constrained (Param_Ty)
+                  then
+                     declare
+                        Comp : Node_Id := First_Component (Param_Ty);
+
+                     begin
+                        while Present (Comp) loop
+                           if Has_Discriminant_Dependent_Constraint (Comp) then
+                              return True;
+                           end if;
+
+                           Comp := Next_Component (Comp);
+                        end loop;
+                     end;
+                  end if;
+
+                  Param := Next (Param);
+               end loop;
+            end if;
+         end;
+
+         return False;
+      end Has_Parameter_With_Discriminant_Dependent_Fields;
+
       -----------------------
       -- Has_Some_Contract --
       -----------------------
@@ -1497,11 +1569,20 @@ package body Inline is
       elsif Instantiation_Location (Sloc (Id)) /= No_Location then
          return False;
 
-      --  Don't inline predicate functions (treated specially by GNATprove)
+      --  Do not inline predicate functions (treated specially by GNATprove)
 
       elsif Is_Predicate_Function (Id) then
          return False;
 
+      --  Do not inline subprograms with a parameter of an unconstrained
+      --  record type if it has discrimiant dependent fields. Indeed, with
+      --  such parameters, the frontend cannot always ensure type compliance
+      --  in record component accesses (in particular with records containing
+      --  packed arrays).
+
+      elsif Has_Parameter_With_Discriminant_Dependent_Fields (Id) then
+         return False;
+
       --  Otherwise, this is a subprogram declared inside the private part of a
       --  package, or inside a package body, or locally in a subprogram, and it
       --  does not have any contract. Inline it.
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 424c118bbb9..0fa78179c84 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -12456,6 +12456,14 @@ package body Sem_Ch12 is
          end;
       end if;
 
+      --  For a floating-point type, capture dimension info if any, because
+      --  the generated subtype declaration does not come from source and
+      --  will not process dimensions.
+
+      if Is_Floating_Point_Type (Act_T) then
+         Copy_Dimensions (Act_T, Subt);
+      end if;
+
       return Decl_Nodes;
    end Instantiate_Type;
 
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 5883e4c5e92..fc230109044 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -1642,6 +1642,8 @@ package body Sem_Ch13 is
             --  Processing based on specific aspect
 
             case A_Id is
+               when Aspect_Unimplemented =>
+                  null; -- ??? temp for now
 
                --  No_Aspect should be impossible
 
@@ -9024,7 +9026,8 @@ package body Sem_Ch13 is
               Aspect_Refined_Post              |
               Aspect_Refined_State             |
               Aspect_SPARK_Mode                |
-              Aspect_Test_Case                 =>
+              Aspect_Test_Case                 |
+              Aspect_Unimplemented             =>
             raise Program_Error;
 
       end case;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 929b1c94155..2f9e1f5532b 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -2203,22 +2203,6 @@ package body Sem_Ch6 is
 
          if Present (Ref_Global) then
             Analyze_Refined_Global_In_Decl_Part (Ref_Global);
-
-         --  When the corresponding Global pragma references a state with
-         --  visible refinement, the body requires Refined_Global. Such a
-         --  refinement is not required when SPARK checks are suppressed.
-
-         else
-            Prag := Get_Pragma (Spec_Id, Pragma_Global);
-
-            if SPARK_Mode /= Off
-              and then Present (Prag)
-              and then Contains_Refined_State (Prag)
-            then
-               Error_Msg_NE
-                 ("body of subprogram& requires global refinement",
-                  Body_Decl, Spec_Id);
-            end if;
          end if;
 
          --  Refined_Depends must be analyzed after Refined_Global in order to
@@ -2226,22 +2210,6 @@ package body Sem_Ch6 is
 
          if Present (Ref_Depends) then
             Analyze_Refined_Depends_In_Decl_Part (Ref_Depends);
-
-         --  When the corresponding Depends pragma references a state with
-         --  visible refinement, the body requires Refined_Depends. Such a
-         --  refinement is not required when SPARK checks are suppressed.
-
-         else
-            Prag := Get_Pragma (Spec_Id, Pragma_Depends);
-
-            if SPARK_Mode /= Off
-              and then Present (Prag)
-              and then Contains_Refined_State (Prag)
-            then
-               Error_Msg_NE
-                 ("body of subprogram& requires dependance refinement",
-                  Body_Decl, Spec_Id);
-            end if;
          end if;
       end Analyze_Completion_Contract;
 
diff --git a/gcc/ada/sem_dim.adb b/gcc/ada/sem_dim.adb
index 37d2f7a9123..1f98027a379 100644
--- a/gcc/ada/sem_dim.adb
+++ b/gcc/ada/sem_dim.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2011-2014, Free Software Foundation, Inc.         --
+--          Copyright (C) 2011-2015, 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- --
@@ -27,6 +27,7 @@ with Aspects;  use Aspects;
 with Atree;    use Atree;
 with Einfo;    use Einfo;
 with Errout;   use Errout;
+with Exp_Util; use Exp_Util;
 with Lib;      use Lib;
 with Namet;    use Namet;
 with Nlists;   use Nlists;
@@ -1792,9 +1793,14 @@ package body Sem_Dim is
 
    begin
       --  Aspect is an Ada 2012 feature. Note that there is no need to check
-      --  dimensions for aggregates that don't come from source.
+      --  dimensions for aggregates that don't come from source, or if we are
+      --  within an initialization procedure, whose expressions have been
+      --  checked at the point of record declaration.
 
-      if Ada_Version < Ada_2012 or else not Comes_From_Source (N) then
+      if Ada_Version < Ada_2012
+        or else not Comes_From_Source (N)
+        or else Inside_Init_Proc
+      then
          return;
       end if;
 
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index 3dc93111fb1..5f057f236a8 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -617,6 +617,17 @@ package Sinfo is
    --       checks on empty ranges, which typically appear in deactivated
    --       code in a particular configuration).
 
+   --    6. Subtypes should match in the AST, even after a generic is
+   --       instantiated. In particular, GNATprove relies on the fact that,
+   --       on a selected component, the type of the selected component is
+   --       the type of the corresponding component in the prefix of the
+   --       selected component.
+   --
+   --       Note that, in some cases, we know that this rule is broken by the
+   --       frontend. In particular, if the selected component is a packed
+   --       array depending on a discriminant of a unconstrained formal object
+   --       parameter of a generic.
+
    -----------------------
    -- Check Flag Fields --
    -----------------------
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index 6e1aec85a6b..3781cfccc04 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -144,6 +144,7 @@ package Snames is
    Name_Dynamic_Predicate              : constant Name_Id := N + $;
    Name_Static_Predicate               : constant Name_Id := N + $;
    Name_Synchronization                : constant Name_Id := N + $;
+   Name_Unimplemented                  : constant Name_Id := N + $;
 
    --  Some special names used by the expander. Note that the lower case u's
    --  at the start of these names get translated to extra underscores. These