[multiple changes]

2016-04-18  Yannick Moy  <moy@adacore.com>

	* sem_util.adb, sem_util.ads (Has_Full_Default_Initialization): used
	outside of GNATprove, hence it should not be removed.

2016-04-18  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Refinement_Clause):
	The refinement of an external abstract state can now mention
	non-external constituents.
	(Check_External_Property): Update all SPARK RM references.

2016-04-18  Bob Duff  <duff@adacore.com>

	* exp_intr.adb: Remove some duplicated code.

2016-04-18  Yannick Moy  <moy@adacore.com>

	* a-nudira.adb, a-nudira.ads, a-nuflra.adb, a-nuflra.ads: Mark
	package spec and body out of SPARK.

2016-04-18  Johannes Kanig  <kanig@adacore.com>

	* spark_xrefs.ads: Minor comment update.

2016-04-18  Johannes Kanig  <kanig@adacore.com>

	* gnat1drv.adb (Gnat1drv): Force loading of System
	unit for SPARK.

2016-04-18  Bob Duff  <duff@adacore.com>

	* a-cuprqu.adb: Correction to previous change. If a new node
	is inserted at the front of the queue (because it is higher
	priority than the previous front node), we need to update
	Header.Next_Unequal -- not just in the case where the queue was
	previously empty.

From-SVN: r235122

12 files changed, 223 insertions, 121 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index fbdfabc..1269d30 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,41 @@
+2016-04-18  Yannick Moy  <moy@adacore.com>
+
+	* sem_util.adb, sem_util.ads (Has_Full_Default_Initialization): used
+	outside of GNATprove, hence it should not be removed.
+
+2016-04-18  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_prag.adb (Analyze_Refinement_Clause):
+	The refinement of an external abstract state can now mention
+	non-external constituents.
+	(Check_External_Property): Update all SPARK RM references.
+
+2016-04-18  Bob Duff  <duff@adacore.com>
+
+	* exp_intr.adb: Remove some duplicated code.
+
+2016-04-18  Yannick Moy  <moy@adacore.com>
+
+	* a-nudira.adb, a-nudira.ads, a-nuflra.adb, a-nuflra.ads: Mark
+	package spec and body out of SPARK.
+
+2016-04-18  Johannes Kanig  <kanig@adacore.com>
+
+	* spark_xrefs.ads: Minor comment update.
+
+2016-04-18  Johannes Kanig  <kanig@adacore.com>
+
+	* gnat1drv.adb (Gnat1drv): Force loading of System
+	unit for SPARK.
+
+2016-04-18  Bob Duff  <duff@adacore.com>
+
+	* a-cuprqu.adb: Correction to previous change. If a new node
+	is inserted at the front of the queue (because it is higher
+	priority than the previous front node), we need to update
+	Header.Next_Unequal -- not just in the case where the queue was
+	previously empty.
+
 2016-04-18  Bob Duff  <duff@adacore.com>
 
 	* a-cuprqu.ads: Change the representation of List_Type from a
diff --git a/gcc/ada/a-cuprqu.adb b/gcc/ada/a-cuprqu.adb
index fb02f09..7502aa9 100644
--- a/gcc/ada/a-cuprqu.adb
+++ b/gcc/ada/a-cuprqu.adb
@@ -187,10 +187,17 @@ package body Ada.Containers.Unbounded_Priority_Queues is
          Prev.Next.Prev := Node;
          Prev.Next := Node;
 
-         if List.Length = 0 then
+         if Prev = H then
+
+            --  Make sure Next_Unequal of the Header always points to the first
+            --  "real" node. Here, we've inserted a new first "real" node, so
+            --  must update.
+
             List.Header.Next_Unequal := Node;
          end if;
 
+         pragma Assert (List.Header.Next_Unequal = List.Header.Next);
+
          List.Length := List.Length + 1;
 
          if List.Length > List.Max_Length then
diff --git a/gcc/ada/a-nudira.adb b/gcc/ada/a-nudira.adb
index 251f852..2e83600 100644
--- a/gcc/ada/a-nudira.adb
+++ b/gcc/ada/a-nudira.adb
@@ -29,7 +29,9 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-package body Ada.Numerics.Discrete_Random is
+package body Ada.Numerics.Discrete_Random with
+  SPARK_Mode => Off
+is
 
    package SRN renames System.Random_Numbers;
    use SRN;
diff --git a/gcc/ada/a-nudira.ads b/gcc/ada/a-nudira.ads
index 77501ec..c2a7382 100644
--- a/gcc/ada/a-nudira.ads
+++ b/gcc/ada/a-nudira.ads
@@ -41,7 +41,9 @@ with System.Random_Numbers;
 generic
    type Result_Subtype is (<>);
 
-package Ada.Numerics.Discrete_Random is
+package Ada.Numerics.Discrete_Random with
+  SPARK_Mode => Off
+is
 
    --  Basic facilities
 
diff --git a/gcc/ada/a-nuflra.adb b/gcc/ada/a-nuflra.adb
index 2c6fbc4..add19d4 100644
--- a/gcc/ada/a-nuflra.adb
+++ b/gcc/ada/a-nuflra.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-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- --
@@ -29,7 +29,9 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-package body Ada.Numerics.Float_Random is
+package body Ada.Numerics.Float_Random with
+  SPARK_Mode => Off
+is
 
    package SRN renames System.Random_Numbers;
    use SRN;
diff --git a/gcc/ada/a-nuflra.ads b/gcc/ada/a-nuflra.ads
index 5a448a7..ea4992c 100644
--- a/gcc/ada/a-nuflra.ads
+++ b/gcc/ada/a-nuflra.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
 -- GNAT. The copyright notice above, and the license provisions that follow --
@@ -38,7 +38,9 @@
 
 with System.Random_Numbers;
 
-package Ada.Numerics.Float_Random is
+package Ada.Numerics.Float_Random with
+  SPARK_Mode => Off
+is
 
    --  Basic facilities
 
diff --git a/gcc/ada/exp_intr.adb b/gcc/ada/exp_intr.adb
index b8f1fe4..f030782 100644
--- a/gcc/ada/exp_intr.adb
+++ b/gcc/ada/exp_intr.adb
@@ -852,11 +852,7 @@ package body Exp_Intr is
    ------------------------
 
    procedure Expand_Source_Info (N : Node_Id; Nam : Name_Id) is
-      --  ???There is duplicated code here (see Add_Source_Info)
-
       Loc : constant Source_Ptr := Sloc (N);
-      Ent : Entity_Id;
-
    begin
       --  Integer cases
 
@@ -870,67 +866,7 @@ package body Exp_Intr is
 
       else
          Name_Len := 0;
-
-         case Nam is
-            when Name_File =>
-               Get_Decoded_Name_String
-                 (Reference_Name (Get_Source_File_Index (Loc)));
-
-            when Name_Source_Location =>
-               Build_Location_String (Loc);
-
-            when Name_Enclosing_Entity =>
-
-               --  Skip enclosing blocks to reach enclosing unit
-
-               Ent := Current_Scope;
-               while Present (Ent) loop
-                  exit when Ekind (Ent) /= E_Block
-                    and then Ekind (Ent) /= E_Loop;
-                  Ent := Scope (Ent);
-               end loop;
-
-               --  Ent now points to the relevant defining entity
-
-               Write_Entity_Name (Ent);
-
-            when Name_Compilation_ISO_Date =>
-               Name_Buffer (1 .. 10) := Opt.Compilation_Time (1 .. 10);
-               Name_Len := 10;
-
-            when Name_Compilation_Date =>
-               declare
-                  subtype S13 is String (1 .. 3);
-                  Months : constant array (1 .. 12) of S13 :=
-                    ("Jan", "Feb", "Mar", "Apr", "May", "Jun",
-                     "Jul", "Aug", "Sep", "Oct", "Nov", "Dec");
-
-                  M1 : constant Character := Opt.Compilation_Time (6);
-                  M2 : constant Character := Opt.Compilation_Time (7);
-
-                  MM : constant Natural range 1 .. 12 :=
-                    (Character'Pos (M1) - Character'Pos ('0')) * 10 +
-                    (Character'Pos (M2) - Character'Pos ('0'));
-
-               begin
-                  --  Reformat ISO date into MMM DD YYYY (__DATE__) format
-
-                  Name_Buffer (1 .. 3)  := Months (MM);
-                  Name_Buffer (4)       := ' ';
-                  Name_Buffer (5 .. 6)  := Opt.Compilation_Time (9 .. 10);
-                  Name_Buffer (7)       := ' ';
-                  Name_Buffer (8 .. 11) := Opt.Compilation_Time (1 .. 4);
-                  Name_Len := 11;
-               end;
-
-            when Name_Compilation_Time =>
-               Name_Buffer (1 .. 8) := Opt.Compilation_Time (12 .. 19);
-               Name_Len := 8;
-
-            when others =>
-               raise Program_Error;
-         end case;
-
+         Add_Source_Info (Loc, Nam);
          Rewrite (N,
            Make_String_Literal (Loc,
              Strval => String_From_Name_Buffer));
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index b8ea585..29f2f94 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -1045,6 +1045,20 @@ begin
       Original_Operating_Mode := Operating_Mode;
       Frontend;
 
+      --  In GNATprove mode, force loading of System unit when tasking is
+      --  used, so that in particular System.Interrupt_Priority is available
+      --  to GNATprove for the generation of VCs for checking the respect of
+      --  Ceiling Protocol.
+
+      if GNATprove_Mode and Opt.Tasking_Used then
+         declare
+            Unused_E : constant Entity_Id :=
+              Rtsfind.RTE (Rtsfind.RE_Interrupt_Priority);
+         begin
+            null;
+         end;
+      end if;
+
       --  Exit with errors if the main source could not be parsed
 
       if Sinput.Main_Source_File = No_Source_File then
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 0197159..118d43d 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -25514,7 +25514,7 @@ package body Sem_Prag is
             Error_Msg_Name_1 := Prop_Nam;
 
             --  The property is enabled in the related Abstract_State pragma
-            --  that defines the state (SPARK RM 7.2.8(3)).
+            --  that defines the state (SPARK RM 7.2.8(2)).
 
             if Enabled then
                if No (Constit) then
@@ -25525,7 +25525,7 @@ package body Sem_Prag is
 
             --  The property is missing in the declaration of the state, but
             --  a constituent is introducing it in the state refinement
-            --  (SPARK RM 7.2.8(3)).
+            --  (SPARK RM 7.2.8(2)).
 
             elsif Present (Constit) then
                Error_Msg_Name_2 := Chars (Constit);
@@ -25746,49 +25746,31 @@ package body Sem_Prag is
             Analyze_Constituent (Constit);
          end if;
 
-         --  A refined external state is subject to special rules with respect
-         --  to its properties and constituents.
+         --  The set of properties that all external constituents yield must
+         --  match that of the refined state. There are two cases to detect:
+         --  the refined state lacks a property or has an extra property
+         --  (SPARK RM 7.2.8(2)).
 
          if Is_External_State (State_Id) then
-
-            --  The set of properties that all external constituents yield must
-            --  match that of the refined state. There are two cases to detect:
-            --  the refined state lacks a property or has an extra property.
-
-            if External_Constit_Seen then
-               Check_External_Property
-                 (Prop_Nam => Name_Async_Readers,
-                  Enabled  => Async_Readers_Enabled (State_Id),
-                  Constit  => AR_Constit);
-
-               Check_External_Property
-                 (Prop_Nam => Name_Async_Writers,
-                  Enabled  => Async_Writers_Enabled (State_Id),
-                  Constit  => AW_Constit);
-
-               Check_External_Property
-                 (Prop_Nam => Name_Effective_Reads,
-                  Enabled  => Effective_Reads_Enabled (State_Id),
-                  Constit  => ER_Constit);
-
-               Check_External_Property
-                 (Prop_Nam => Name_Effective_Writes,
-                  Enabled  => Effective_Writes_Enabled (State_Id),
-                  Constit  => EW_Constit);
-
-            --  An external state may be refined to null (SPARK RM 7.2.8(2))
-
-            elsif Null_Seen then
-               null;
-
-            --  The external state has constituents, but none of them are
-            --  external (SPARK RM 7.2.8(2)).
-
-            else
-               SPARK_Msg_NE
-                 ("external state & requires at least one external "
-                  & "constituent or null refinement", State, State_Id);
-            end if;
+            Check_External_Property
+              (Prop_Nam => Name_Async_Readers,
+               Enabled  => Async_Readers_Enabled (State_Id),
+               Constit  => AR_Constit);
+
+            Check_External_Property
+              (Prop_Nam => Name_Async_Writers,
+               Enabled  => Async_Writers_Enabled (State_Id),
+               Constit  => AW_Constit);
+
+            Check_External_Property
+              (Prop_Nam => Name_Effective_Reads,
+               Enabled  => Effective_Reads_Enabled (State_Id),
+               Constit  => ER_Constit);
+
+            Check_External_Property
+              (Prop_Nam => Name_Effective_Writes,
+               Enabled  => Effective_Writes_Enabled (State_Id),
+               Constit  => EW_Constit);
 
          --  When a refined state is not external, it should not have external
          --  constituents (SPARK RM 7.2.8(1)).
@@ -26760,17 +26742,17 @@ package body Sem_Prag is
    ---------------------------------------------
 
    procedure Collect_Inherited_Class_Wide_Conditions (Subp : Entity_Id) is
-      Parent_Subp : constant Entity_Id := Overridden_Operation (Subp);
-      Prags       : constant Node_Id   := Contract (Parent_Subp);
+      Parent_Subp  : constant Entity_Id := Overridden_Operation (Subp);
+      Prags        : constant Node_Id   := Contract (Parent_Subp);
+      In_Spec_Expr : Boolean;
+      Installed    : Boolean;
       Prag         : Node_Id;
       New_Prag     : Node_Id;
-      Installed    : Boolean;
-      In_Spec_Expr : Boolean;
 
    begin
       Installed := False;
 
-      --  Iterate over the contract of the overridden subprogram  to find
+      --  Iterate over the contract of the overridden subprogram to find all
       --  inherited class-wide pre- and postconditions.
 
       if Present (Prags) then
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 35b0888..1146b9d 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -9046,6 +9046,110 @@ package body Sem_Util is
       end if;
    end Has_Enabled_Property;
 
+   -------------------------------------
+   -- Has_Full_Default_Initialization --
+   -------------------------------------
+
+   function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean is
+      Arg  : Node_Id;
+      Comp : Entity_Id;
+      Prag : Node_Id;
+
+   begin
+      --  A private type and its full view is fully default initialized when it
+      --  is subject to pragma Default_Initial_Condition without an argument or
+      --  with a non-null argument. Since any type may act as the full view of
+      --  a private type, this check must be performed prior to the specialized
+      --  tests below.
+
+      if Has_Default_Init_Cond (Typ)
+        or else Has_Inherited_Default_Init_Cond (Typ)
+      then
+         Prag := Get_Pragma (Typ, Pragma_Default_Initial_Condition);
+
+         --  Pragma Default_Initial_Condition must be present if one of the
+         --  related entity flags is set.
+
+         pragma Assert (Present (Prag));
+         Arg := First (Pragma_Argument_Associations (Prag));
+
+         --  A non-null argument guarantees full default initialization
+
+         if Present (Arg) then
+            return Nkind (Arg) /= N_Null;
+
+         --  Otherwise the missing argument defaults the pragma to "True" which
+         --  is considered a non-null argument (see above).
+
+         else
+            return True;
+         end if;
+      end if;
+
+      --  A scalar type is fully default initialized if it is subject to aspect
+      --  Default_Value.
+
+      if Is_Scalar_Type (Typ) then
+         return Has_Default_Aspect (Typ);
+
+      --  An array type is fully default initialized if its element type is
+      --  scalar and the array type carries aspect Default_Component_Value or
+      --  the element type is fully default initialized.
+
+      elsif Is_Array_Type (Typ) then
+         return
+           Has_Default_Aspect (Typ)
+             or else Has_Full_Default_Initialization (Component_Type (Typ));
+
+      --  A protected type, record type or type extension is fully default
+      --  initialized if all its components either carry an initialization
+      --  expression or have a type that is fully default initialized. The
+      --  parent type of a type extension must be fully default initialized.
+
+      elsif Is_Record_Type (Typ) or else Is_Protected_Type (Typ) then
+
+         --  Inspect all entities defined in the scope of the type, looking for
+         --  uninitialized components.
+
+         Comp := First_Entity (Typ);
+         while Present (Comp) loop
+            if Ekind (Comp) = E_Component
+              and then Comes_From_Source (Comp)
+              and then No (Expression (Parent (Comp)))
+              and then not Has_Full_Default_Initialization (Etype (Comp))
+            then
+               return False;
+            end if;
+
+            Next_Entity (Comp);
+         end loop;
+
+         --  Ensure that the parent type of a type extension is fully default
+         --  initialized.
+
+         if Etype (Typ) /= Typ
+           and then not Has_Full_Default_Initialization (Etype (Typ))
+         then
+            return False;
+         end if;
+
+         --  If we get here, then all components and parent portion are fully
+         --  default initialized.
+
+         return True;
+
+      --  A task type is fully default initialized by default
+
+      elsif Is_Task_Type (Typ) then
+         return True;
+
+      --  Otherwise the type is not fully default initialized
+
+      else
+         return False;
+      end if;
+   end Has_Full_Default_Initialization;
+
    --------------------
    -- Has_Infinities --
    --------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index e868c83..d8a9b52 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1034,6 +1034,19 @@ package Sem_Util is
    --  Determine whether subprogram Subp_Id has an effectively volatile formal
    --  parameter or returns an effectively volatile value.
 
+   function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean;
+   --  Determine whether type Typ defines "full default initialization" as
+   --  specified by SPARK RM 3.1. To qualify as such, the type must be
+   --    * A scalar type with specified Default_Value
+   --    * An array-of-scalar type with specified Default_Component_Value
+   --    * An array type whose element type defines full default initialization
+   --    * A protected type, record type or type extension whose components
+   --      either include a default expression or have a type which defines
+   --      full default initialization. In the case of type extensions, the
+   --      parent type defines full default initialization.
+   --   * A task type
+   --   * A private type whose Default_Initial_Condition is non-null
+
    function Has_Infinities (E : Entity_Id) return Boolean;
    --  Determines if the range of the floating-point type E includes
    --  infinities. Returns False if E is not a floating-point type.
diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads
index eb95f73..f02234f 100644
--- a/gcc/ada/spark_xrefs.ads
+++ b/gcc/ada/spark_xrefs.ads
@@ -200,7 +200,7 @@ package SPARK_Xrefs is
    --  not relate to Generated Globals.
 
    --  The processing (reading and writing) of this section happens in
-   --  package Flow_Computed_Globals (from the SPARK 2014 sources), for
+   --  package Flow_Generated_Globals (from the SPARK 2014 sources), for
    --  further information please refer there.
 
    ----------------