2013-07-12 Basile Starynkevitch <basile@starynkevitch.net>

	MELT branch merged with trunk rev 200918 using svnmerge.py



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/branches/melt-branch@200920 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 11 insertions, 0 deletions

diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index 3b8a3bcbc89..fcbe9889861 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -113,6 +113,9 @@ package Sem_Prag is
    --  True have their analysis delayed until after the main program is parsed
    --  and analyzed.
 
+   function Get_SPARK_Mode_Id (N : Node_Id) return SPARK_Mode_Id;
+   --  Given a pragma SPARK_Mode node, return the corresponding mode id
+
    procedure Initialize;
    --  Initializes data structures used for pragma processing. Must be called
    --  before analyzing each new main source program.
@@ -127,6 +130,10 @@ package Sem_Prag is
    --  length, and then returns True. If it is not of the correct form, then an
    --  appropriate error message is posted, and False is returned.
 
+   function Is_Elaboration_SPARK_Mode (N : Node_Id) return Boolean;
+   --  Determine whether pragma SPARK_Mode appears in the statement part of a
+   --  package body.
+
    function Is_Non_Significant_Pragma_Reference (N : Node_Id) return Boolean;
    --  The node N is a node for an entity and the issue is whether the
    --  occurrence is a reference for the purposes of giving warnings about
@@ -143,6 +150,10 @@ package Sem_Prag is
    --  False is returned, then the argument is treated as an entity reference
    --  to the operator.
 
+   function Is_Private_SPARK_Mode (N : Node_Id) return Boolean;
+   --  Determine whether pragma SPARK_Mode appears in the private part of a
+   --  package.
+
    function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean;
    --  Returns True if Nam is one of the names recognized as a valid assertion
    --  kind by the Assertion_Policy pragma. Note that the 'Class cases are