[multiple changes]

2014-01-29  Thomas Quinot  <quinot@adacore.com>

	* sem_ch4.adb (Find_Component_In_Instance): Update comment.

2014-01-29  Ed Schonberg  <schonberg@adacore.com>

	* exp_util.adb (Build_Task_Image_Prefix): Indicate that the
	resulting string is an internal entity. and thus requires no
	initialization. This is relevant when Initialize_ Scalars is
	enabled, because the resultant spurious initialization may lead to
	secondary stack anomalies that produce a mangled name for a task.

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

	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): SPARK_Mode
	not inherited from spec anymore. Check consistency
	rules after processing of declarations.
	* sem_ch7.adb (Analyze_Package_Body_Helper): SPARK_Mode not inherited
	from spec anymore. Check consistency rules after processing of
	declarations.
	(Analyze_Package_Declaration): Set SPARK_Mode only for non-generic
	packages.
	* sem_prag.adb (Analyze_Pragma/Pragma_SPARK_Mode): Implement new
	consistency rules.

From-SVN: r207242

6 files changed, 205 insertions, 94 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 237c3e0..8987a17 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,28 @@
+2014-01-29  Thomas Quinot  <quinot@adacore.com>
+
+	* sem_ch4.adb (Find_Component_In_Instance): Update comment.
+
+2014-01-29  Ed Schonberg  <schonberg@adacore.com>
+
+	* exp_util.adb (Build_Task_Image_Prefix): Indicate that the
+	resulting string is an internal entity. and thus requires no
+	initialization. This is relevant when Initialize_ Scalars is
+	enabled, because the resultant spurious initialization may lead to
+	secondary stack anomalies that produce a mangled name for a task.
+
+2014-01-29  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): SPARK_Mode
+	not inherited from spec anymore. Check consistency
+	rules after processing of declarations.
+	* sem_ch7.adb (Analyze_Package_Body_Helper): SPARK_Mode not inherited
+	from spec anymore. Check consistency rules after processing of
+	declarations.
+	(Analyze_Package_Declaration): Set SPARK_Mode only for non-generic
+	packages.
+	* sem_prag.adb (Analyze_Pragma/Pragma_SPARK_Mode): Implement new
+	consistency rules.
+
 2014-01-27  Robert Dewar  <dewar@adacore.com>
 
 	* sem_res.adb (Resolve_Comparison_Op): Add type name/location
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 5262627..f6fff6c 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -1403,6 +1403,12 @@ package body Exp_Util is
                          Low_Bound => Make_Integer_Literal (Loc, 1),
                          High_Bound => New_Occurrence_Of (Len, Loc)))))));
 
+      --  Indicate that the result is an internal temporary, so it does not
+      --  receive a bogus initialization when declaration is expanded. This
+      --  is both efficient, and prevents anomalies in the handling of
+      --  dynamic objects on the secondary stack.
+
+      Set_Is_Internal (Res);
       Pos := Make_Temporary (Loc, 'P');
 
       Append_To (Decls,
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 51e7f09..7c0a0cc 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -3940,10 +3940,10 @@ package body Sem_Ch4 is
       --  In an instance, a component of a private extension may not be visible
       --  while it was visible in the generic. Search candidate scope for a
       --  component with the proper identifier. This is only done if all other
-      --  searches have failed. When the match is found (it always will be),
-      --  the Etype of both N and Sel are set from this component, and the
-      --  entity of Sel is set to reference this component.
-      --  ??? no longer true that a match is found ???
+      --  searches have failed. If a match is found, the Etype of both N and
+      --  Sel are set from this component, and the entity of Sel is set to
+      --  reference this component. If no match is found, Entity (Sel) remains
+      --  unset.
 
       function Has_Mode_Conformant_Spec (Comp : Entity_Id) return Boolean;
       --  It is known that the parent of N denotes a subprogram call. Comp
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 715ca24..77108b2 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -2999,34 +2999,10 @@ package body Sem_Ch6 is
 
             Push_Scope (Spec_Id);
 
-            --  Set SPARK_Mode
+            --  Set SPARK_Mode from context
 
-            --  For internally generated subprogram, always off. But generic
-            --  instances are not generated implicitly, so are never considered
-            --  as internal, even though Comes_From_Source is false.
-
-            if not Comes_From_Source (Spec_Id)
-              and then not Is_Generic_Instance (Spec_Id)
-            then
-               SPARK_Mode := Off;
-               SPARK_Mode_Pragma := Empty;
-
-            --  Inherited from spec
-
-            elsif Present (SPARK_Pragma (Spec_Id))
-              and then not SPARK_Pragma_Inherited (Spec_Id)
-            then
-               SPARK_Mode_Pragma := SPARK_Pragma (Spec_Id);
-               SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragma);
-               Set_SPARK_Pragma (Body_Id, SPARK_Pragma (Spec_Id));
-               Set_SPARK_Pragma_Inherited (Body_Id, True);
-
-            --  Otherwise set from context
-
-            else
-               Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
-               Set_SPARK_Pragma_Inherited (Body_Id, True);
-            end if;
+            Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+            Set_SPARK_Pragma_Inherited (Body_Id, True);
 
             --  Make sure that the subprogram is immediately visible. For
             --  child units that have no separate spec this is indispensable.
@@ -3076,17 +3052,10 @@ package body Sem_Ch6 is
 
             Push_Scope (Body_Id);
 
-            --  Set SPARK_Mode from context or OFF for internal routine
+            --  Set SPARK_Mode from context
 
-            if Comes_From_Source (Body_Id) then
-               Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
-               Set_SPARK_Pragma_Inherited (Body_Id, True);
-            else
-               Set_SPARK_Pragma (Body_Id, Empty);
-               Set_SPARK_Pragma_Inherited (Body_Id, False);
-               SPARK_Mode := Off;
-               SPARK_Mode_Pragma := Empty;
-            end if;
+            Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+            Set_SPARK_Pragma_Inherited (Body_Id, True);
          end if;
 
          --  For stubs and bodies with no previous spec, generate references to
@@ -3277,6 +3246,35 @@ package body Sem_Ch6 is
 
       Analyze_Declarations (Declarations (N));
 
+      --  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.
+
+      if Present (Spec_Id) and then Present (SPARK_Pragma (Body_Id)) then
+         if Present (SPARK_Pragma (Spec_Id)) then
+            if Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) = Off
+                 and then
+               Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On
+            then
+               Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
+               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);
+            end if;
+
+         elsif Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Body_Stub then
+            null;
+
+         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);
+         end if;
+      end if;
+
       --  Check completion, and analyze the statements
 
       Check_Completion;
@@ -3632,16 +3630,11 @@ package body Sem_Ch6 is
 
       Generate_Definition (Designator);
 
-      --  Set SPARK mode, always off for internal routines, otherwise set
-      --  from current context (may be overwritten later with explicit pragma)
+      --  Set SPARK mode from current context (may be overwritten later with
+      --  explicit pragma).
 
-      if Comes_From_Source (Designator) then
-         Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
-         Set_SPARK_Pragma_Inherited (Designator, True);
-      else
-         Set_SPARK_Pragma (Designator, Empty);
-         Set_SPARK_Pragma_Inherited (Designator, False);
-      end if;
+      Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
+      Set_SPARK_Pragma_Inherited (Designator, True);
 
       if Debug_Flag_C then
          Write_Str ("==> subprogram spec ");
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index 5ae4aa3..79cd31a 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.adb
@@ -346,28 +346,19 @@ package body Sem_Ch7 is
 
       Push_Scope (Spec_Id);
 
-      --  Set SPARK_Mode from private part of spec if it has a SPARK pragma.
-      --  Note that in the default case, SPARK_Aux_Pragma will be a copy of
-      --  SPARK_Pragma in the spec, so this properly handles the case where
-      --  there is no explicit SPARK_Pragma mode in the private part.
-
-      if Present (SPARK_Pragma (Spec_Id)) then
-         SPARK_Mode_Pragma := SPARK_Aux_Pragma (Spec_Id);
-         SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragma);
-         Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
-         Set_SPARK_Pragma_Inherited (Body_Id, True);
+      --  Set SPARK_Mode only for non-generic package
 
-      --  Otherwise set from context
+      if Ekind (Spec_Id) = E_Package then
+         --  Set SPARK_Mode from context
 
-      else
          Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
          Set_SPARK_Pragma_Inherited (Body_Id, True);
-      end if;
 
-      --  Set elaboration code SPARK mode the same for now
+         --  Set elaboration code SPARK mode the same for now
 
-      Set_SPARK_Aux_Pragma (Body_Id, SPARK_Pragma (Body_Id));
-      Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
+         Set_SPARK_Aux_Pragma (Body_Id, SPARK_Pragma (Body_Id));
+         Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
+      end if;
 
       Set_Categorization_From_Pragmas (N);
 
@@ -400,6 +391,32 @@ 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.
+
+      if Present (SPARK_Pragma (Body_Id)) then
+         if Present (SPARK_Aux_Pragma (Spec_Id)) then
+            if Get_SPARK_Mode_From_Pragma (SPARK_Aux_Pragma (Spec_Id)) = Off
+                 and then
+               Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On
+            then
+               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);
+            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);
+         end if;
+      end if;
+
       --  Analyze_Declarations has caused freezing of all types. Now generate
       --  bodies for RACW primitives and stream attributes, if any.
 
@@ -814,12 +831,14 @@ package body Sem_Ch7 is
       Set_Etype    (Id, Standard_Void_Type);
       Set_Contract (Id, Make_Contract (Sloc (Id)));
 
-      --  Inherit spark mode from context for now
+      --  Set SPARK_Mode from context only for non-generic package
 
-      Set_SPARK_Pragma               (Id, SPARK_Mode_Pragma);
-      Set_SPARK_Aux_Pragma           (Id, SPARK_Mode_Pragma);
-      Set_SPARK_Pragma_Inherited     (Id, True);
-      Set_SPARK_Aux_Pragma_Inherited (Id, True);
+      if Ekind (Id) = E_Package then
+         Set_SPARK_Pragma               (Id, SPARK_Mode_Pragma);
+         Set_SPARK_Aux_Pragma           (Id, SPARK_Mode_Pragma);
+         Set_SPARK_Pragma_Inherited     (Id, True);
+         Set_SPARK_Aux_Pragma_Inherited (Id, True);
+      end if;
 
       --  Analyze aspect specifications immediately, since we need to recognize
       --  things like Pure early enough to diagnose violations during analysis.
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 3ddaed2..1cc7fd2 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -18597,14 +18597,26 @@ package body Sem_Prag is
             Spec_Id : Entity_Id;
             Stmt    : Node_Id;
 
-            procedure Check_Pragma_Conformance (Old_Pragma : Node_Id);
-            --  Verify the monotonicity of SPARK modes between the new pragma
-            --  N, and the old pragma, Old_Pragma, that was inherited. If
-            --  Old_Pragma is Empty, the call has no effect, otherwise we
-            --  verify that the new mode is less restrictive than the old mode.
-            --  For example, if the old mode is ON, then the new mode can be
-            --  anything. But if the old mode is OFF, then the only allowed
-            --  new mode is also OFF.
+            procedure Check_Pragma_Conformance
+              (Context_Pragma : Node_Id;
+               Entity_Pragma  : Node_Id;
+               Entity         : Entity_Id);
+            --  If Context_Pragma is not Empty, verify that the new pragma N
+            --  is compatible with the pragma Context_Pragma that was inherited
+            --  from the context:
+            --  . if Context_Pragma is ON, then the new mode can be anything
+            --  . if Context_Pragma is OFF, then the only allowed new mode is
+            --    also OFF.
+            --
+            --  If Entity is not Empty, verify that the new pragma N is
+            --  compatible with Entity_Pragma, the SPARK_Mode previously set
+            --  for Entity (which may be Empty):
+            --  . if Entity_Pragma is ON, then the new mode can be anything
+            --  . if Entity_Pragma is OFF, then the only allowed new mode is
+            --    also OFF.
+            --  . if Entity_Pragma is Empty, we always issue an error, as this
+            --    corresponds to a case where a previous section of Entity
+            --    had no SPARK_Mode set.
 
             procedure Check_Library_Level_Entity (E : Entity_Id);
             --  Verify that pragma is applied to library-level entity E
@@ -18613,20 +18625,44 @@ package body Sem_Prag is
             -- Check_Pragma_Conformance --
             ------------------------------
 
-            procedure Check_Pragma_Conformance (Old_Pragma : Node_Id) is
+            procedure Check_Pragma_Conformance
+              (Context_Pragma : Node_Id;
+               Entity_Pragma  : Node_Id;
+               Entity         : Entity_Id) is
             begin
-               if Present (Old_Pragma) then
-                  pragma Assert (Nkind (Old_Pragma) = N_Pragma);
+               if Present (Context_Pragma) then
+                  pragma Assert (Nkind (Context_Pragma) = N_Pragma);
 
                   --  New mode less restrictive than the established mode
 
-                  if Get_SPARK_Mode_From_Pragma (Old_Pragma) = Off
+                  if Get_SPARK_Mode_From_Pragma (Context_Pragma) = Off
                     and then Mode_Id = On
                   then
                      Error_Msg_N
-                       ("cannot change 'S'P'A'R'K_Mode from Off to On", Arg1);
+                       ("cannot change SPARK_Mode from Off to On", Arg1);
                      Error_Msg_Sloc := Sloc (SPARK_Mode_Pragma);
-                     Error_Msg_N ("\'S'P'A'R'K_Mode was set to Off#", Arg1);
+                     Error_Msg_N ("\SPARK_Mode was set to Off#", Arg1);
+                     raise Pragma_Exit;
+                  end if;
+               end if;
+
+               if Present (Entity) then
+                  if Present (Entity_Pragma) then
+                     if Get_SPARK_Mode_From_Pragma (Entity_Pragma) = Off
+                       and then Mode_Id = On
+                     then
+                        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 & #",
+                           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);
                      raise Pragma_Exit;
                   end if;
                end if;
@@ -18733,7 +18769,10 @@ package body Sem_Prag is
                   then
                      Spec_Id := Defining_Entity (Stmt);
                      Check_Library_Level_Entity (Spec_Id);
-                     Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+                     Check_Pragma_Conformance
+                       (Context_Pragma => SPARK_Pragma (Spec_Id),
+                        Entity_Pragma  => Empty,
+                        Entity         => Empty);
 
                      Set_SPARK_Pragma               (Spec_Id, N);
                      Set_SPARK_Pragma_Inherited     (Spec_Id, False);
@@ -18748,7 +18787,10 @@ package body Sem_Prag is
                   then
                      Spec_Id := Defining_Entity (Stmt);
                      Check_Library_Level_Entity (Spec_Id);
-                     Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+                     Check_Pragma_Conformance
+                       (Context_Pragma => SPARK_Pragma (Spec_Id),
+                        Entity_Pragma  => Empty,
+                        Entity         => Empty);
 
                      Set_SPARK_Pragma               (Spec_Id, N);
                      Set_SPARK_Pragma_Inherited     (Spec_Id, False);
@@ -18804,7 +18846,10 @@ package body Sem_Prag is
 
                   if List_Containing (N) = Private_Declarations (Context) then
                      Check_Library_Level_Entity (Spec_Id);
-                     Check_Pragma_Conformance (SPARK_Aux_Pragma (Spec_Id));
+                     Check_Pragma_Conformance
+                       (Context_Pragma => Empty,
+                        Entity_Pragma  => SPARK_Pragma (Spec_Id),
+                        Entity         => Spec_Id);
                      SPARK_Mode_Pragma := N;
                      SPARK_Mode := Mode_Id;
 
@@ -18815,7 +18860,10 @@ package body Sem_Prag is
 
                   else
                      Check_Library_Level_Entity (Spec_Id);
-                     Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+                     Check_Pragma_Conformance
+                       (Context_Pragma => SPARK_Pragma (Spec_Id),
+                        Entity_Pragma  => Empty,
+                        Entity         => Empty);
                      SPARK_Mode_Pragma := N;
                      SPARK_Mode := Mode_Id;
 
@@ -18834,8 +18882,10 @@ package body Sem_Prag is
                then
                   Spec_Id := Defining_Entity (Context);
                   Check_Library_Level_Entity (Spec_Id);
-                  Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
-
+                  Check_Pragma_Conformance
+                    (Context_Pragma => SPARK_Pragma (Spec_Id),
+                     Entity_Pragma  => Empty,
+                     Entity         => Empty);
                   Set_SPARK_Pragma           (Spec_Id, N);
                   Set_SPARK_Pragma_Inherited (Spec_Id, False);
 
@@ -18848,7 +18898,10 @@ package body Sem_Prag is
                   Spec_Id := Corresponding_Spec (Context);
                   Body_Id := Defining_Entity (Context);
                   Check_Library_Level_Entity (Body_Id);
-                  Check_Pragma_Conformance (SPARK_Pragma (Body_Id));
+                  Check_Pragma_Conformance
+                    (Context_Pragma => SPARK_Pragma (Body_Id),
+                     Entity_Pragma  => SPARK_Aux_Pragma (Spec_Id),
+                     Entity         => Spec_Id);
                   SPARK_Mode_Pragma := N;
                   SPARK_Mode := Mode_Id;
 
@@ -18867,7 +18920,19 @@ package body Sem_Prag is
                   Context := Specification (Context);
                   Body_Id := Defining_Entity (Context);
                   Check_Library_Level_Entity (Body_Id);
-                  Check_Pragma_Conformance (SPARK_Pragma (Body_Id));
+
+                  if Present (Spec_Id) then
+                     Check_Pragma_Conformance
+                       (Context_Pragma => SPARK_Pragma (Body_Id),
+                        Entity_Pragma  => SPARK_Pragma (Spec_Id),
+                        Entity         => Spec_Id);
+                  else
+                     Check_Pragma_Conformance
+                       (Context_Pragma => SPARK_Pragma (Body_Id),
+                        Entity_Pragma  => Empty,
+                        Entity         => Empty);
+                  end if;
+
                   SPARK_Mode_Pragma := N;
                   SPARK_Mode := Mode_Id;
 
@@ -18887,7 +18952,10 @@ package body Sem_Prag is
                   Spec_Id := Corresponding_Spec (Context);
                   Body_Id := Defining_Entity (Context);
                   Check_Library_Level_Entity (Body_Id);
-                  Check_Pragma_Conformance (SPARK_Aux_Pragma (Body_Id));
+                  Check_Pragma_Conformance
+                    (Context_Pragma => Empty,
+                     Entity_Pragma  => SPARK_Pragma (Body_Id),
+                     Entity         => Body_Id);
                   SPARK_Mode_Pragma := N;
                   SPARK_Mode := Mode_Id;