2014-01-29 Robert Dewar <dewar@adacore.com>

	* sem_ch7.adb, sem_prag.adb, sem_ch4.adb, sem_ch6.adb: Minor code
	reorganization.

2014-01-29  Yannick Moy  <moy@adacore.com>

	* gnat_rm.texi: Update description of SPARK_Mode pragma.

2014-01-29  Tristan Gingold  <gingold@adacore.com>

	* exp_ch9.adb (Expand_N_Protected_Body): Remove Num_Entries.



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

7 files changed, 92 insertions, 126 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 8987a17b60b..23fc4021aca 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,16 @@
+2014-01-29  Robert Dewar  <dewar@adacore.com>
+
+	* sem_ch7.adb, sem_prag.adb, sem_ch4.adb, sem_ch6.adb: Minor code
+	reorganization.
+
+2014-01-29  Yannick Moy  <moy@adacore.com>
+
+	* gnat_rm.texi: Update description of SPARK_Mode pragma.
+
+2014-01-29  Tristan Gingold  <gingold@adacore.com>
+
+	* exp_ch9.adb (Expand_N_Protected_Body): Remove Num_Entries.
+
 2014-01-29  Thomas Quinot  <quinot@adacore.com>
 
 	* sem_ch4.adb (Find_Component_In_Instance): Update comment.
diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb
index b85dd015f45..694569ddc24 100644
--- a/gcc/ada/exp_ch9.adb
+++ b/gcc/ada/exp_ch9.adb
@@ -8436,7 +8436,6 @@ package body Exp_Ch9 is
       Current_Node : Node_Id;
       Disp_Op_Body : Node_Id;
       New_Op_Body  : Node_Id;
-      Num_Entries  : Natural := 0;
       Op_Body      : Node_Id;
       Op_Id        : Entity_Id;
 
@@ -8625,8 +8624,6 @@ package body Exp_Ch9 is
 
             when N_Entry_Body =>
                Op_Id := Defining_Identifier (Op_Body);
-               Num_Entries := Num_Entries + 1;
-
                New_Op_Body := Build_Protected_Entry (Op_Body, Op_Id, Pid);
 
                Insert_After (Current_Node, New_Op_Body);
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index 6f04498d4f9..abb00383157 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -6309,124 +6309,75 @@ pragma SPARK_Mode [(On | Off)] ;
 @end smallexample
 
 @noindent
-This pragma is used to specify whether a construct must
-satisfy the syntactic and semantic rules of the SPARK 2014 programming
-language. The pragma is intended for use with formal verification tools
-and has no effect on the generated code.
+In general a program can have some parts that are in SPARK 2014 (and
+follow all the rules in the SPARK Reference Manual), and some parts
+that are full Ada 2012.
 
-The SPARK_Mode pragma is used to specify the value of the SPARK_Mode aspect
-(either Off or On) of an entity.
-More precisely, it is used to specify the aspect value of a ``section''
-of an entity (the term ``section'' is defined below).
-If a Spark_Mode pragma's (optional) argument is omitted,
-an implicit argument of On is assumed.
-
-A SPARK_Mode pragma may be used as a configuration pragma and then has the
-semantics described below.
-
-A SPARK_Mode pragma can be used as a local pragma only
-in the following contexts:
+The SPARK_Mode pragma is used to identify which parts are in SPARK
+2014 (by default programs are in full Ada). The SPARK_Mode pragma can
+be used in the following places:
 
 @itemize @bullet
 
 @item
-When the pragma is at the start of the visible declarations (preceded only
-by other pragmas) of a package declaration, it marks the visible part
-of the package as being in or out of SPARK 2014.
+As a configuration pragma, in which case it sets the default mode for
+all units compiled with this pragma.
 
 @item
-When the pragma appears at the start of the private declarations of a
-package (preceded only by other pragmas), it marks the private part
-of the package as being in or out of SPARK 2014.
+Immediately following a library-level subprogram spec
 
 @item
-When the pragma appears at the start of the declarations of a
-package body (preceded only by other pragmas),
-it marks the declaration list of the package body body as being
-in or out of SPARK 2014.
+Immediately within a library-level package body
 
 @item
-When the pragma appears at the start of the elaboration statements of
-a package body (preceded only by other pragmas),
-it marks the handled_sequence_of_statements of the package body
-as being in or out of SPARK 2014.
+Immediately following the @code{private} keyword of a library-level
+package spec
 
 @item
-When the pragma appears after a subprogram declaration (with only other
-pragmas intervening), it marks the subprogram's specification as
-being in or out of SPARK 2014.
+Immediately following the @code{begin} keyword of a library-level
+package body
 
 @item
-When the pragma appears at the start of the declarations of a subprogram
-body (preceded only by other pragmas), it marks the subprogram body
-as being in or out of SPARK 2014. For a subprogram body which is
-not a completion of another declaration, it also applies to the
-specification of the subprogram.
+Immediately within a library-level subprogram body
 
 @end itemize
 
-A package is defined to have 4 ``sections'': its visible part, its private
-part, its body's declaration list, and its body's
-handled_sequence_of_statements. Any other construct which requires a
-completion is defined to have 2 ``sections'': its declaration and its
-completion. Any other construct is defined to have 1 section.
+@noindent
+Normally a subprogram or package spec/body inherits the current mode
+that is active at the point it is declared. But this can be overridden
+by pragma within the spec or body as above.
 
-The SPARK_Mode aspect value of an arbitrary section of an arbitrary Ada entity
-or construct is then defined to be the following value:
+The basic consistency rule is that you can't turn SPARK_Mode back
+@code{On}, once you have explicitly (with a pragma) turned if
+@code{Off}. So the following rules apply:
 
-@itemize
+@noindent
+If a subprogram spec has SPARK_Mode @code{Off}, then the body must
+also have SPARK_Mode @code{Off}.
 
-@item
-If SPARK_Mode has been specified for the given section of the given entity or
-construct, then the specified value;
+@noindent
+For a package, we have four parts:
 
+@itemize
 @item
-else if SPARK_Mode has been specified for at least one preceding section of
-the same entity, then the SPARK_Mode of the immediately preceding section;
-
+the package public declarations
 @item
-else for any of the visible part or body declarations of a library unit package
-or either section of a library unit subprogram, if there is an applicable
-SPARK_Mode configuration pragma then the value specified by the
-pragma; if no such configuration pragma applies, then an implicit
-specification of Off is assumed;
-
+the package private part
 @item
-else for any subsequent (i.e., not the first) section of a library unit
-package, the SPARK_Mode of the preceding section;
-
+the body of the package
 @item
-else the SPARK_Mode of the enclosing section of the nearest enclosing package
-or subprogram;
-
+the elaboration code after @code{begin}
 @end itemize
 
-If the above computation does not specify a SPARK_Mode setting for any
-construct other than one of the four sections of a package, then a result of On
-or Off is determined instead based on the legality (with respect to the rules
-of SPARK 2014) of the construct. The construct's SPARK_Mode is On if and only
-if the construct is in SPARK 2014.
-
-If an earlier section of an entity has a Spark_Mode of Off, then the
-Spark_Mode aspect of any later section of that entity shall not be
-specified to be On. For example,
-if the specification of a subprogram has a Spark_Mode of Off, then the
-body of the subprogram shall not have a Spark_Mode of On.
-
-The following rules apply to SPARK code (i.e., constructs which
-have a SPARK_Mode aspect value of On):
-
-@itemize
-
-@item
-SPARK code shall only reference SPARK declarations, but a SPARK declaration
-which requires a completion may have a non-SPARK completion.
-
-@item
-SPARK code shall only enclose SPARK code, except that SPARK code may enclose
-a non-SPARK completion of an enclosed SPARK declaration.
-
-@end itemize
+@noindent
+For a package, the rule is that if you explicitly turn SPARK_Mode
+@code{Off} for any part, then all the following parts must have
+SPARK_Mode @code{Off}. Note that this may require repeating a pragma
+SPARK_Mode (@code{Off}) in the body. For example, if we have a
+configuration pragma SPARK_Mode (@code{On}) that turns the mode on by
+default everywhere, and one particular package spec has pragma
+SPARK_Mode (@code{Off}), then that pragma will need to be repeated in
+the package body.
 
 @node Pragma Static_Elaboration_Desired
 @unnumberedsec Pragma Static_Elaboration_Desired
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 7c0a0cc81c4..c7fc43269cc 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -3972,7 +3972,9 @@ package body Sem_Ch4 is
             Next_Component (Comp);
          end loop;
 
-         --  Need comment on what is going on when we fall through ???
+         --  If we fall through, no match, so no changes made
+
+         return;
       end Find_Component_In_Instance;
 
       ------------------------------
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 77108b25bde..68775fbde7b 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3260,7 +3260,7 @@ package body Sem_Ch6 is
                Error_Msg_N ("incorrect application of SPARK_Mode#", N);
                Error_Msg_Sloc := Sloc (SPARK_Pragma (Spec_Id));
                Error_Msg_NE
-                 ("\value Off was set for SPARK_Mode on & #", N, Spec_Id);
+                 ("\value Off was set for SPARK_Mode on&#", N, Spec_Id);
             end if;
 
          elsif Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Body_Stub then
@@ -3270,8 +3270,7 @@ package body Sem_Ch6 is
             Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
             Error_Msg_N ("incorrect application of SPARK_Mode#", N);
             Error_Msg_Sloc := Sloc (Spec_Id);
-            Error_Msg_NE
-              ("\no value was set for SPARK_Mode on & #", N, Spec_Id);
+            Error_Msg_NE ("\no value was set for SPARK_Mode on&#", N, Spec_Id);
          end if;
       end if;
 
@@ -3348,12 +3347,11 @@ package body Sem_Ch6 is
       --  the body of the procedure. But first we deal with a special case
       --  where we want to modify this check. If the body of the subprogram
       --  starts with a raise statement or its equivalent, or if the body
-      --  consists entirely of a null statement, then it is pretty obvious
-      --  that it is OK to not reference the parameters. For example, this
-      --  might be the following common idiom for a stubbed function:
-      --  statement of the procedure raises an exception. In particular this
-      --  deals with the common idiom of a stubbed function, which might
-      --  appear as something like:
+      --  consists entirely of a null statement, then it is pretty obvious that
+      --  it is OK to not reference the parameters. For example, this might be
+      --  the following common idiom for a stubbed function: statement of the
+      --  procedure raises an exception. In particular this deals with the
+      --  common idiom of a stubbed function, which appears something like:
 
       --     function F (A : Integer) return Some_Type;
       --        X : Some_Type;
@@ -3649,12 +3647,12 @@ package body Sem_Ch6 is
       New_Overloaded_Entity (Designator);
       Check_Delayed_Subprogram (Designator);
 
-      --  If the type of the first formal of the current subprogram is a
-      --  non-generic tagged private type, mark the subprogram as being a
-      --  private primitive. Ditto if this is a function with controlling
-      --  result, and the return type is currently private. In both cases,
-      --  the type of the controlling argument or result must be in the
-      --  current scope for the operation to be primitive.
+      --  If the type of the first formal of the current subprogram is a non-
+      --  generic tagged private type, mark the subprogram as being a private
+      --  primitive. Ditto if this is a function with controlling result, and
+      --  the return type is currently private. In both cases, the type of the
+      --  controlling argument or result must be in the current scope for the
+      --  operation to be primitive.
 
       if Has_Controlling_Result (Designator)
         and then Is_Private_Type (Etype (Designator))
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index 79cd31a3d4b..4b6a6e42482 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.adb
@@ -349,6 +349,7 @@ package body Sem_Ch7 is
       --  Set SPARK_Mode only for non-generic package
 
       if Ekind (Spec_Id) = E_Package then
+
          --  Set SPARK_Mode from context
 
          Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
@@ -391,9 +392,9 @@ package body Sem_Ch7 is
          Inspect_Deferred_Constant_Completion (Declarations (N));
       end if;
 
-      --  After declarations have been analyzed, the body has been set
-      --  its final value of SPARK_Mode. Check that SPARK_Mode for body
-      --  is consistent with SPARK_Mode for spec.
+      --  After declarations have been analyzed, the body has been set to have
+      --  the final value of SPARK_Mode. Check that the SPARK_Mode for the body
+      --  is consistent with the SPARK_Mode for the spec.
 
       if Present (SPARK_Pragma (Body_Id)) then
          if Present (SPARK_Aux_Pragma (Spec_Id)) then
@@ -404,16 +405,16 @@ package body Sem_Ch7 is
                Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
                Error_Msg_N ("incorrect application of SPARK_Mode#", N);
                Error_Msg_Sloc := Sloc (SPARK_Aux_Pragma (Spec_Id));
-               Error_Msg_NE ("\value Off was set for SPARK_Mode on & #",
-                             N, Spec_Id);
+               Error_Msg_NE
+                 ("\value Off was set for SPARK_Mode on & #", N, Spec_Id);
             end if;
 
          else
             Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
             Error_Msg_N ("incorrect application of SPARK_Mode#", N);
             Error_Msg_Sloc := Sloc (Spec_Id);
-            Error_Msg_NE ("\no value was set for SPARK_Mode on & #",
-                          N, Spec_Id);
+            Error_Msg_NE
+              ("\no value was set for SPARK_Mode on & #", N, Spec_Id);
          end if;
       end if;
 
@@ -539,12 +540,13 @@ package body Sem_Ch7 is
             function Has_Referencer
               (L     : List_Id;
                Outer : Boolean) return  Boolean;
-            --  Traverse the given list of declarations in reverse order.
-            --  Return True if a referencer is present. Return False if none is
-            --  found. The Outer parameter is True for the outer level call and
-            --  False for inner level calls for nested packages. If Outer is
-            --  True, then any entities up to the point of hitting a referencer
-            --  get their Is_Public flag cleared, so that the entities will be
+            --  Traverse given list of declarations in reverse order. Return
+            --  True if a referencer is present. Return False if none is found.
+            --
+            --  The Outer parameter is True for the outer level call and False
+            --  for inner level calls for nested packages. If Outer is True,
+            --  then any entities up to the point of hitting a referencer get
+            --  their Is_Public flag cleared, so that the entities will be
             --  treated as static entities in the C sense, and need not have
             --  fully qualified names. Furthermore, if the referencer is an
             --  inlined subprogram that doesn't reference other subprograms,
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 1cc7fd2460c..b6846d45299 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -18628,7 +18628,8 @@ package body Sem_Prag is
             procedure Check_Pragma_Conformance
               (Context_Pragma : Node_Id;
                Entity_Pragma  : Node_Id;
-               Entity         : Entity_Id) is
+               Entity         : Entity_Id)
+            is
             begin
                if Present (Context_Pragma) then
                   pragma Assert (Nkind (Context_Pragma) = N_Pragma);
@@ -18654,15 +18655,17 @@ package body Sem_Prag is
                         Error_Msg_N ("incorrect use of SPARK_Mode", Arg1);
                         Error_Msg_Sloc := Sloc (Entity_Pragma);
                         Error_Msg_NE
-                          ("\value Off was set for SPARK_Mode on & #",
+                          ("\value Off was set for SPARK_Mode on&#",
                            Arg1, Entity);
                         raise Pragma_Exit;
                      end if;
+
                   else
                      Error_Msg_N ("incorrect use of SPARK_Mode", Arg1);
                      Error_Msg_Sloc := Sloc (Entity);
-                     Error_Msg_NE ("\no value was set for SPARK_Mode on & #",
-                                   Arg1, Entity);
+                     Error_Msg_NE
+                       ("\no value was set for SPARK_Mode on&#",
+                        Arg1, Entity);
                      raise Pragma_Exit;
                   end if;
                end if;