2014-08-04 Hristian Kirtchev <kirtchev@adacore.com>

	* opt.ads Alphabetize various global flags. New flag
	Ignore_Pragma_SPARK_Mode along with a comment on usage.
	* sem_ch6.adb (Analyze_Generic_Subprogram_Body):
	Pragma SPARK_Mode is now allowed in generic units.
	(Analyze_Subprogram_Body_Helper): Do not verify the compatibility
	between the SPARK_Mode of a spec and that of a body when inside
	a generic.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Do not verify the
	compatibility between the SPARK_Mode of a spec and that of a
	body when inside a generic.
	* sem_ch12.adb (Analyze_Generic_Subprogram_Declaration):
	Pragma SPARK_Mode is now allowed in generic units.
	(Analyze_Package_Instantiation): Save and restore the value of
	flag Ignore_ Pragma_SPARK_Mode in a stack-like fasion. Set
	the governing SPARK_Mode before analyzing the instance.
	(Analyze_Subprogram_Instantiation): Save and restore the value
	of flag Ignore_ Pragma_SPARK_Mode in a stack-like fasion. Set
	the governing SPARK_Mode before analyzing the instance.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Emulate the
	placement of a source pragma when inserting the generated pragma
	for aspect SPARK_Mode.
	* sem_prag.adb (Analyze_Pragma): Reimplement the handling of
	pragma SPARK_Mode to allow for generics and their respective
	instantiations.
	* sem_util.ads, sem_util.adb (Check_SPARK_Mode_In_Generic): Removed.
	(Set_Ignore_Pragma_SPARK_Mode): New routine.

From-SVN: r213570

gcc/ada/ChangeLog

+2014-08-04  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* opt.ads Alphabetize various global flags. New flag
+	Ignore_Pragma_SPARK_Mode along with a comment on usage.
+	* sem_ch6.adb (Analyze_Generic_Subprogram_Body):
+	Pragma SPARK_Mode is now allowed in generic units.
+	(Analyze_Subprogram_Body_Helper): Do not verify the compatibility
+	between the SPARK_Mode of a spec and that of a body when inside
+	a generic.
+	* sem_ch7.adb (Analyze_Package_Body_Helper): Do not verify the
+	compatibility between the SPARK_Mode of a spec and that of a
+	body when inside a generic.
+	* sem_ch12.adb (Analyze_Generic_Subprogram_Declaration):
+	Pragma SPARK_Mode is now allowed in generic units.
+	(Analyze_Package_Instantiation): Save and restore the value of
+	flag Ignore_ Pragma_SPARK_Mode in a stack-like fasion. Set
+	the governing SPARK_Mode before analyzing the instance.
+	(Analyze_Subprogram_Instantiation): Save and restore the value
+	of flag Ignore_ Pragma_SPARK_Mode in a stack-like fasion. Set
+	the governing SPARK_Mode before analyzing the instance.
+	* sem_ch13.adb (Analyze_Aspect_Specifications): Emulate the
+	placement of a source pragma when inserting the generated pragma
+	for aspect SPARK_Mode.
+	* sem_prag.adb (Analyze_Pragma): Reimplement the handling of
+	pragma SPARK_Mode to allow for generics and their respective
+	instantiations.
+	* sem_util.ads, sem_util.adb (Check_SPARK_Mode_In_Generic): Removed.
+	(Set_Ignore_Pragma_SPARK_Mode): New routine.
+
 2014-08-04  Eric Botcazou  <ebotcazou@adacore.com>
 
         * gcc-interface/decl.c (gnat_to_gnu_entity) <E_Component>: Deal with

gcc/ada/opt.ads

@@ -648,6 +648,20 @@ package Opt is
    --  GNAT
    --  Disable generation of ALI file
 
+   Follow_Links_For_Files : Boolean := False;
+   --  PROJECT MANAGER
+   --  Set to True (-eL) to process the project files in trusted mode. If
+   --  Follow_Links is False, it is assumed that the project doesn't contain
+   --  any file duplicated through symbolic links (although the latter are
+   --  still valid if they point to a file which is outside of the project),
+   --  and that no directory has a name which is a valid source name.
+
+   Follow_Links_For_Dirs : Boolean := False;
+   --  PROJECT MANAGER
+   --  Set to True if directories can be links in this project, and therefore
+   --  additional system calls must be performed to ensure that we always see
+   --  the same full name for each directory.
+
    Force_Checking_Of_Elaboration_Flags : Boolean := False;
    --  GNATBIND
    --  True if binding with forced checking of the elaboration flags
@@ -657,6 +671,13 @@ package Opt is
    --  GNATMAKE, GPRMAKE, GPRBUILD
    --  Set to force recompilations even when the objects are up-to-date.
 
+   Front_End_Inlining : Boolean := False;
+   --  GNAT
+   --  Set True to activate inlining by front-end expansion (even on GCC
+   --  targets, where inlining is normally handled by the back end). Set by
+   --  the flag -gnatN (which is now considered obsolescent, since the GCC
+   --  back end can do a better job of inlining than the front end these days.
+
    Full_Path_Name_For_Brief_Errors : Boolean := False;
    --  PROJECT MANAGER
    --  When True, in Brief_Output mode, each error message line
@@ -684,6 +705,10 @@ package Opt is
    --  True when switch -gnateG is used. When True, create in a file
    --  <source>.prep, if the source is preprocessed.
 
+   Generate_SCIL : Boolean := False;
+   --  GNAT
+   --  Set True to activate SCIL code generation.
+
    Generate_SCO : Boolean := False;
    --  GNAT
    --  True when switch -fdump-scos (or -gnateS) is used. When True, Source
@@ -728,6 +753,12 @@ package Opt is
    --  default value appropriate to the system (in Osint.Initialize), and then
    --  reset if a command line switch is used to change the setting.
 
+   Ignore_Pragma_SPARK_Mode : Boolean := False;
+   --  GNAT
+   --  Set True to ignore the semantics and effects of pragma SPARK_Mode when
+   --  the pragma appears inside an instance whose enclosing context is subject
+   --  to SPARK_Mode "off".
+
    Ignore_Rep_Clauses : Boolean := False;
    --  GNAT
    --  Set True to ignore all representation clauses. Useful when compiling
@@ -798,35 +829,10 @@ package Opt is
    --  then elaboration flag checks are to be generated in the binder
    --  generated file.
 
-   Generate_SCIL : Boolean := False;
-   --  GNAT
-   --  Set True to activate SCIL code generation.
-
    Invalid_Value_Used : Boolean := False;
    --  GNAT
    --  Set True if a valid Invalid_Value attribute is encountered
 
-   Follow_Links_For_Files : Boolean := False;
-   --  PROJECT MANAGER
-   --  Set to True (-eL) to process the project files in trusted mode. If
-   --  Follow_Links is False, it is assumed that the project doesn't contain
-   --  any file duplicated through symbolic links (although the latter are
-   --  still valid if they point to a file which is outside of the project),
-   --  and that no directory has a name which is a valid source name.
-
-   Follow_Links_For_Dirs : Boolean := False;
-   --  PROJECT MANAGER
-   --  Set to True if directories can be links in this project, and therefore
-   --  additional system calls must be performed to ensure that we always see
-   --  the same full name for each directory.
-
-   Front_End_Inlining : Boolean := False;
-   --  GNAT
-   --  Set True to activate inlining by front-end expansion (even on GCC
-   --  targets, where inlining is normally handled by the back end). Set by
-   --  the flag -gnatN (which is now considered obsolescent, since the GCC
-   --  back end can do a better job of inlining than the front end these days.
-
    Inline_Processing_Required : Boolean := False;
    --  GNAT
    --  Set True if inline processing is required. Inline processing is required

gcc/ada/sem_ch12.adb

@@ -3342,8 +3342,6 @@ package body Sem_Ch12 is
       Set_Parent_Spec (New_N, Save_Parent);
       Rewrite (N, New_N);
 
-      Check_SPARK_Mode_In_Generic (N);
-
       --  The aspect specifications are not attached to the tree, and must
       --  be copied and attached to the generic copy explicitly.
 
@@ -3532,6 +3530,9 @@ package body Sem_Ch12 is
       Needs_Body       : Boolean;
       Inline_Now       : Boolean := False;
 
+      Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
+      --  Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+
       Save_Style_Check : constant Boolean := Style_Check;
       --  Save style check mode for restore on exit
 
@@ -3771,6 +3772,12 @@ package body Sem_Ch12 is
          goto Leave;
 
       else
+         --  If the instance or its context is subject to SPARK_Mode "off",
+         --  set the global flag which signals Analyze_Pragma to ignore all
+         --  SPARK_Mode pragmas within the instance.
+
+         Set_Ignore_Pragma_SPARK_Mode (N);
+
          Gen_Decl := Unit_Declaration_Node (Gen_Unit);
 
          --  Initialize renamings map, for error checking, and the list that
@@ -3835,9 +3842,7 @@ package body Sem_Ch12 is
             Set_Visible_Declarations (Act_Spec, Renaming_List);
          end if;
 
-         Act_Decl :=
-           Make_Package_Declaration (Loc,
-             Specification => Act_Spec);
+         Act_Decl := Make_Package_Declaration (Loc, Specification => Act_Spec);
 
          --  Propagate the aspect specifications from the package declaration
          --  template to the instantiated version of the package declaration.
@@ -4277,6 +4282,7 @@ package body Sem_Ch12 is
          Set_Defining_Identifier (N, Act_Decl_Id);
       end if;
 
+      Ignore_Pragma_SPARK_Mode := Save_IPSM;
       Style_Check := Save_Style_Check;
 
       --  Check that if N is an instantiation of System.Dim_Float_IO or
@@ -4311,6 +4317,7 @@ package body Sem_Ch12 is
             Restore_Env;
          end if;
 
+         Ignore_Pragma_SPARK_Mode := Save_IPSM;
          Style_Check := Save_Style_Check;
    end Analyze_Package_Instantiation;
 
@@ -4865,6 +4872,9 @@ package body Sem_Ch12 is
 
       --  Local variables
 
+      Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
+      --  Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+
       Vis_Prims_List : Elist_Id := No_Elist;
       --  List of primitives made temporarily visible in the instantiation
       --  to match the visibility of the formal type
@@ -4929,6 +4939,12 @@ package body Sem_Ch12 is
          Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit);
 
       else
+         --  If the instance or its context is subject to SPARK_Mode "off",
+         --  set the global flag which signals Analyze_Pragma to ignore all
+         --  SPARK_Mode pragmas within the instance.
+
+         Set_Ignore_Pragma_SPARK_Mode (N);
+
          Set_Entity (Gen_Id, Gen_Unit);
          Set_Is_Instantiated (Gen_Unit);
 
@@ -5139,6 +5155,8 @@ package body Sem_Ch12 is
          Env_Installed := False;
          Generic_Renamings.Set_Last (0);
          Generic_Renamings_HTable.Reset;
+
+         Ignore_Pragma_SPARK_Mode := Save_IPSM;
       end if;
 
    <<Leave>>
@@ -5155,6 +5173,8 @@ package body Sem_Ch12 is
          if Env_Installed then
             Restore_Env;
          end if;
+
+         Ignore_Pragma_SPARK_Mode := Save_IPSM;
    end Analyze_Subprogram_Instantiation;
 
    -------------------------

gcc/ada/sem_ch13.adb

@@ -2418,11 +2418,11 @@ package body Sem_Ch13 is
                          Expression => Relocate_Node (Expr))),
                      Pragma_Name                  => Name_SPARK_Mode);
 
-                  --  When the aspect appears on a package body, insert the
-                  --  generated pragma at the top of the body declarations to
-                  --  emulate the behavior of a source pragma.
+                  --  When the aspect appears on a package or a subprogram
+                  --  body, insert the generated pragma at the top of the body
+                  --  declarations to emulate the behavior of a source pragma.
 
-                  if Nkind (N) = N_Package_Body then
+                  if Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
                      Decorate (Aspect, Aitem);
 
                      Decls := Declarations (N);
@@ -2435,11 +2435,14 @@ package body Sem_Ch13 is
                      Prepend_To (Decls, Aitem);
                      goto Continue;
 
-                  --  When the aspect is associated with package declaration,
-                  --  insert the generated pragma at the top of the visible
-                  --  declarations to emulate the behavior of a source pragma.
+                  --  When the aspect is associated with a [generic] package
+                  --  declaration, insert the generated pragma at the top of
+                  --  the visible declarations to emulate the behavior of a
+                  --  source pragma.
 
-                  elsif Nkind (N) = N_Package_Declaration then
+                  elsif Nkind_In (N, N_Generic_Package_Declaration,
+                                     N_Package_Declaration)
+                  then
                      Decorate (Aspect, Aitem);
 
                      Decls := Visible_Declarations (Specification (N));

gcc/ada/sem_ch6.adb

@@ -1251,8 +1251,6 @@ package body Sem_Ch6 is
             end loop;
          end;
 
-         Check_SPARK_Mode_In_Generic (N);
-
          Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
          Set_SPARK_Pragma_Inherited (Body_Id, True);
 
@@ -3743,11 +3741,12 @@ 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.
+      --  Verify that the SPARK_Mode of the body agrees with that of its spec
 
-      if Present (Spec_Id) and then Present (SPARK_Pragma (Body_Id)) then
+      if not Inside_A_Generic
+        and then 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
@@ -3757,7 +3756,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
@@ -3767,7 +3766,8 @@ 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;
 

gcc/ada/sem_ch7.adb

@@ -437,11 +437,9 @@ package body Sem_Ch7 is
          Inspect_Deferred_Constant_Completion (Declarations (N));
       end if;
 
-      --  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.
+      --  Verify that the SPARK_Mode of the body agrees with that of its spec
 
-      if Present (SPARK_Pragma (Body_Id)) then
+      if not Inside_A_Generic and then 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

gcc/ada/sem_util.adb

@@ -3078,31 +3078,6 @@ package body Sem_Util is
       end if;
    end Check_Result_And_Post_State;
 
-   ---------------------------------
-   -- Check_SPARK_Mode_In_Generic --
-   ---------------------------------
-
-   procedure Check_SPARK_Mode_In_Generic (N : Node_Id) is
-      Aspect : Node_Id;
-
-   begin
-      --  Try to find aspect SPARK_Mode and flag it as illegal
-
-      if Has_Aspects (N) then
-         Aspect := First (Aspect_Specifications (N));
-         while Present (Aspect) loop
-            if Get_Aspect_Id (Aspect) = Aspect_SPARK_Mode then
-               Error_Msg_Name_1 := Name_SPARK_Mode;
-               Error_Msg_N
-                 ("incorrect placement of aspect % on a generic", Aspect);
-               exit;
-            end if;
-
-            Next (Aspect);
-         end loop;
-      end if;
-   end Check_SPARK_Mode_In_Generic;
-
    ------------------------------
    -- Check_Unprotected_Access --
    ------------------------------
@@ -16481,6 +16456,128 @@ package body Sem_Util is
       Set_Entity (N, Val);
    end Set_Entity_With_Checks;
 
+   ----------------------------------
+   -- Set_Ignore_Pragma_SPARK_Mode --
+   ----------------------------------
+
+   procedure Set_Ignore_Pragma_SPARK_Mode (N : Node_Id) is
+      procedure Set_SPARK_Mode (Expr : Node_Id);
+      --  Set flag Ignore_Pragma_SPARK_Mode based on the argument of aspect or
+      --  pragma SPARK_Mode denoted by Expr.
+
+      --------------------
+      -- Set_SPARK_Mode --
+      --------------------
+
+      procedure Set_SPARK_Mode (Expr : Node_Id) is
+      begin
+         --  When pragma SPARK_Mode with argument "off" applies to an instance,
+         --  all SPARK_Mode pragmas within the instance are ignored.
+
+         if Present (Expr)
+           and then Nkind (Expr) = N_Identifier
+           and then Chars (Expr) = Name_Off
+         then
+            Ignore_Pragma_SPARK_Mode := True;
+         end if;
+      end Set_SPARK_Mode;
+
+      --  Local variables
+
+      Aspects : constant List_Id := Aspect_Specifications (N);
+      Context : constant Node_Id := Parent (N);
+      Args    : List_Id;
+      Aspect  : Node_Id;
+      Decl    : Node_Id;
+
+   --  Start of processing for Set_Ignore_Pragma_SPARK_Mode
+
+   begin
+      --  When the enclosing context of the instance has SPARK_Mode "off", all
+      --  SPARK_Mode pragmas within the instance are ignored. Note that there
+      --  is no point in checking whether the instantiation itself carries
+      --  aspect/pragma SPARK_Mode because it is either illegal ("on") or has
+      --  no effect ("off").
+
+      if SPARK_Mode = Off then
+         Ignore_Pragma_SPARK_Mode := True;
+         return;
+      end if;
+
+      --  Inspect the aspects of the instantiation and locate SPARK_Mode. Note
+      --  that the aspect form of SPARK_Mode precedes a potentially duplicate
+      --  pragma.
+
+      if Present (Aspects) then
+         Aspect := First (Aspects);
+         while Present (Aspect) loop
+            if Get_Aspect_Id (Aspect) = Aspect_SPARK_Mode then
+               Set_SPARK_Mode (Expression (Aspect));
+               return;
+            end if;
+
+            Next (Aspect);
+         end loop;
+      end if;
+
+      --  Peek ahead of the instance and locate pragma SPARK_Mode. Even though
+      --  the pragma is analyzed after the instance, its mode must be known now
+      --  as it governs the legality of SPARK_Mode pragmas within the instance.
+
+      Decl := Empty;
+
+      --  The instance is a compilation unit, the pragma appears on the
+      --  Pragmas_After list.
+
+      if Present (Context)
+        and then Nkind (Context) = N_Compilation_Unit
+        and then Present (Aux_Decls_Node (Context))
+        and then Present (Pragmas_After (Aux_Decls_Node (Context)))
+      then
+         Decl := First (Pragmas_After (Aux_Decls_Node (Context)));
+
+      --  The instance is part of a declarative list, the pragma appears after
+      --  the instance.
+
+      elsif Is_List_Member (N) then
+         Decl := Next (N);
+      end if;
+
+      --  Inspect all declarations following the instance
+
+      while Present (Decl) loop
+         if Nkind (Decl) = N_Pragma then
+            if Get_Pragma_Id (Decl) = Pragma_SPARK_Mode then
+               Args := Pragma_Argument_Associations (Decl);
+
+               --  The pragma argument dictates the mode
+
+               if Present (Args) then
+                  Set_SPARK_Mode (Get_Pragma_Arg (First (Args)));
+               end if;
+
+               --  Only the first SPARK_Mode following the instance is
+               --  considered, any extra (illegal) pragmas are ignored.
+
+               exit;
+            end if;
+
+         --  Skip internally generated code
+
+         elsif not Comes_From_Source (Decl) then
+            null;
+
+         --  Otherwise a source construct exhaust the range where the pragma
+         --  may appear.
+
+         else
+            exit;
+         end if;
+
+         Next (Decl);
+      end loop;
+   end Set_Ignore_Pragma_SPARK_Mode;
+
    ------------------------
    -- Set_Name_Entity_Id --
    ------------------------

gcc/ada/sem_util.ads

@@ -327,10 +327,6 @@ package Sem_Util is
    --  and post-state. Prag is a [refined] postcondition or a contract-cases
    --  pragma. Result_Seen is set when the pragma mentions attribute 'Result.
 
-   procedure Check_SPARK_Mode_In_Generic (N : Node_Id);
-   --  Given a generic package [body] or a generic subprogram [body], inspect
-   --  the aspect specifications (if any) and flag SPARK_Mode as illegal.
-
    procedure Check_Unprotected_Access
      (Context : Node_Id;
       Expr    : Node_Id);
@@ -1841,6 +1837,11 @@ package Sem_Util is
    --    If restriction No_Implementation_Identifiers is set, then it checks
    --    that the entity is not implementation defined.
 
+   procedure Set_Ignore_Pragma_SPARK_Mode (N : Node_Id);
+   --  Determine whether [the enclosing context of] package or subprogram N is
+   --  subject to pragma SPARK_Mode with mode "off". If this is the case, set
+   --  global flag Ignore_Pragma_SPARK_Mode to True.
+
    procedure Set_Name_Entity_Id (Id : Name_Id; Val : Entity_Id);
    pragma Inline (Set_Name_Entity_Id);
    --  Sets the Entity_Id value associated with the given name, which is the