[multiple changes]

2016-04-18  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): In GNATprove
	mode, collect inherited class-wide conditions to generate the
	corresponding pragmas.
	* sem_prag.ads (Build_Pragma_Check_Equivalent): Moved from contracts
	* contracts.adb (Collect_Inherited_Class_Wide_Conditions): New
	procedure for overriding subprograms, used to generate the pragmas
	corresponding to an inherited class- wide pre- or postcondition.
	* sem_prag.adb (Build_Pragma_Check_Equivalent): moved here
	from contracts.adb (Replace_Condition_Entities): Subsidiary
	Build_Pragma_Check_Equivalent, to implement the proper semantics
	of inherited class-wide conditions, as given in AI12-0113.
	(Process_Class_Wide_Condition): Removed.
	(Collect_Inherited_Class_Wide_Conditions): Iterate over pragmas
	in contract of subprogram, to collect inherited class-wide
	conditions.
	(Build_Pragma_Check_Equivalent): Moved to sem_prag.adb

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

	* a-calend.adb (Ada.Calendar): Mark package body as SPARK_Mode Off.
	* a-calend.ads (Ada.Calendar): Mark package spec as
	SPARK_Mode and add synchronous external abstract state Clock_Time.

From-SVN: r235113

1 files changed, 0 insertions, 158 deletions

diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index ebaecc0..4eb6d26 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -1432,15 +1432,6 @@ package body Contracts is
       --  of statements to be checked on exit. Parameter Result is the entity
       --  of parameter _Result when Subp_Id denotes a function.
 
-      function Build_Pragma_Check_Equivalent
-        (Prag     : Node_Id;
-         Subp_Id  : Entity_Id := Empty;
-         Inher_Id : Entity_Id := Empty) return Node_Id;
-      --  Transform a [refined] pre- or postcondition denoted by Prag into an
-      --  equivalent pragma Check. When the pre- or postcondition is inherited,
-      --  the routine corrects the references of all formals of Inher_Id to
-      --  point to the formals of Subp_Id.
-
       procedure Process_Contract_Cases (Stmts : in out List_Id);
       --  Process pragma Contract_Cases. This routine prepends items to the
       --  body declarations and appends items to list Stmts.
@@ -1860,155 +1851,6 @@ package body Contracts is
          Analyze (Proc_Bod);
       end Build_Postconditions_Procedure;
 
-      -----------------------------------
-      -- Build_Pragma_Check_Equivalent --
-      -----------------------------------
-
-      function Build_Pragma_Check_Equivalent
-        (Prag     : Node_Id;
-         Subp_Id  : Entity_Id := Empty;
-         Inher_Id : Entity_Id := Empty) return Node_Id
-      is
-         function Suppress_Reference (N : Node_Id) return Traverse_Result;
-         --  Detect whether node N references a formal parameter subject to
-         --  pragma Unreferenced. If this is the case, set Comes_From_Source
-         --  to False to suppress the generation of a reference when analyzing
-         --  N later on.
-
-         ------------------------
-         -- Suppress_Reference --
-         ------------------------
-
-         function Suppress_Reference (N : Node_Id) return Traverse_Result is
-            Formal : Entity_Id;
-
-         begin
-            if Is_Entity_Name (N) and then Present (Entity (N)) then
-               Formal := Entity (N);
-
-               --  The formal parameter is subject to pragma Unreferenced.
-               --  Prevent the generation of a reference by resetting the
-               --  Comes_From_Source flag.
-
-               if Is_Formal (Formal)
-                 and then Has_Pragma_Unreferenced (Formal)
-               then
-                  Set_Comes_From_Source (N, False);
-               end if;
-            end if;
-
-            return OK;
-         end Suppress_Reference;
-
-         procedure Suppress_References is
-           new Traverse_Proc (Suppress_Reference);
-
-         --  Local variables
-
-         Loc          : constant Source_Ptr := Sloc (Prag);
-         Prag_Nam     : constant Name_Id    := Pragma_Name (Prag);
-         Check_Prag   : Node_Id;
-         Formals_Map  : Elist_Id;
-         Inher_Formal : Entity_Id;
-         Msg_Arg      : Node_Id;
-         Nam          : Name_Id;
-         Subp_Formal  : Entity_Id;
-
-      --  Start of processing for Build_Pragma_Check_Equivalent
-
-      begin
-         Formals_Map := No_Elist;
-
-         --  When the pre- or postcondition is inherited, map the formals of
-         --  the inherited subprogram to those of the current subprogram.
-
-         if Present (Inher_Id) then
-            pragma Assert (Present (Subp_Id));
-
-            Formals_Map := New_Elmt_List;
-
-            --  Create a relation <inherited formal> => <subprogram formal>
-
-            Inher_Formal := First_Formal (Inher_Id);
-            Subp_Formal  := First_Formal (Subp_Id);
-            while Present (Inher_Formal) and then Present (Subp_Formal) loop
-               Append_Elmt (Inher_Formal, Formals_Map);
-               Append_Elmt (Subp_Formal, Formals_Map);
-
-               Next_Formal (Inher_Formal);
-               Next_Formal (Subp_Formal);
-            end loop;
-         end if;
-
-         --  Copy the original pragma while performing substitutions (if
-         --  applicable).
-
-         Check_Prag :=
-           New_Copy_Tree
-             (Source    => Prag,
-              Map       => Formals_Map,
-              New_Scope => Current_Scope);
-
-         --  Mark the pragma as being internally generated and reset the
-         --  Analyzed flag.
-
-         Set_Analyzed          (Check_Prag, False);
-         Set_Comes_From_Source (Check_Prag, False);
-
-         --  The tree of the original pragma may contain references to the
-         --  formal parameters of the related subprogram. At the same time
-         --  the corresponding body may mark the formals as unreferenced:
-
-         --     procedure Proc (Formal : ...)
-         --       with Pre => Formal ...;
-
-         --     procedure Proc (Formal : ...) is
-         --        pragma Unreferenced (Formal);
-         --     ...
-
-         --  This creates problems because all pragma Check equivalents are
-         --  analyzed at the end of the body declarations. Since all source
-         --  references have already been accounted for, reset any references
-         --  to such formals in the generated pragma Check equivalent.
-
-         Suppress_References (Check_Prag);
-
-         if Present (Corresponding_Aspect (Prag)) then
-            Nam := Chars (Identifier (Corresponding_Aspect (Prag)));
-         else
-            Nam := Prag_Nam;
-         end if;
-
-         --  Convert the copy into pragma Check by correcting the name and
-         --  adding a check_kind argument.
-
-         Set_Pragma_Identifier
-           (Check_Prag, Make_Identifier (Loc, Name_Check));
-
-         Prepend_To (Pragma_Argument_Associations (Check_Prag),
-           Make_Pragma_Argument_Association (Loc,
-             Expression => Make_Identifier (Loc, Nam)));
-
-         --  Update the error message when the pragma is inherited
-
-         if Present (Inher_Id) then
-            Msg_Arg := Last (Pragma_Argument_Associations (Check_Prag));
-
-            if Chars (Msg_Arg) = Name_Message then
-               String_To_Name_Buffer (Strval (Expression (Msg_Arg)));
-
-               --  Insert "inherited" to improve the error message
-
-               if Name_Buffer (1 .. 8) = "failed p" then
-                  Insert_Str_In_Name_Buffer ("inherited ", 8);
-                  Set_Strval (Expression (Msg_Arg), String_From_Name_Buffer);
-               end if;
-            end if;
-         end if;
-
-         return Check_Prag;
-      end Build_Pragma_Check_Equivalent;
-
       ----------------------------
       -- Process_Contract_Cases --
       ----------------------------