[multiple changes]

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

	* exp_ch9.adb (Is_Exception_Safe): Return true if no exceptions.

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

	* inline.ads (Pending_Body_Info): Add SPARK_Mode and
	SPARK_Mode_Pragma components to be able to analyze generic
	instance.
	* sem_ch12.adb (Analyze_Package_Instantiation,
	Inline_Instance_Body, Need_Subprogram_Instance_Body,
	Load_Parent_Of_Generic): Pass in SPARK_Mode from instantiation
	for future analysis of the instance.
	(Instantiate_Package_Body,
	Instantiate_Subprogram_Body, Set_Instance_Inv): Set SPARK_Mode
	from instantiation to analyze the instance.

From-SVN: r207244

4 files changed, 61 insertions, 7 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 23fc402..cdef61e 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,20 @@
+2014-01-29  Tristan Gingold  <gingold@adacore.com>
+
+	* exp_ch9.adb (Is_Exception_Safe): Return true if no exceptions.
+
+2014-01-29  Yannick Moy  <moy@adacore.com>
+
+	* inline.ads (Pending_Body_Info): Add SPARK_Mode and
+	SPARK_Mode_Pragma components to be able to analyze generic
+	instance.
+	* sem_ch12.adb (Analyze_Package_Instantiation,
+	Inline_Instance_Body, Need_Subprogram_Instance_Body,
+	Load_Parent_Of_Generic): Pass in SPARK_Mode from instantiation
+	for future analysis of the instance.
+	(Instantiate_Package_Body,
+	Instantiate_Subprogram_Body, Set_Instance_Inv): Set SPARK_Mode
+	from instantiation to analyze the instance.
+
 2014-01-29  Robert Dewar  <dewar@adacore.com>
 
 	* sem_ch7.adb, sem_prag.adb, sem_ch4.adb, sem_ch6.adb: Minor code
diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb
index 694569d..8f78f06 100644
--- a/gcc/ada/exp_ch9.adb
+++ b/gcc/ada/exp_ch9.adb
@@ -13425,6 +13425,14 @@ package body Exp_Ch9 is
    --  Start of processing for Is_Exception_Safe
 
    begin
+
+      --  When exceptions can not be propagated, the subprogram will always
+      --  return normaly.
+
+      if No_Exception_Handlers_Set then
+         return True;
+      end if;
+
       --  If the checks handled by the back end are not disabled, we cannot
       --  ensure that no exception will be raised.
 
diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads
index 825b958..fd0e965 100644
--- a/gcc/ada/inline.ads
+++ b/gcc/ada/inline.ads
@@ -96,6 +96,11 @@ package Inline is
 
       Warnings : Warning_Record;
       --  Capture values of warning flags
+
+      SPARK_Mode        : SPARK_Mode_Type;
+      SPARK_Mode_Pragma : Node_Id;
+      --  SPARK_Mode for an instance is the one applicable at the point of
+      --  instantiation.
    end record;
 
    package Pending_Instantiations is new Table.Table (
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 565df4e..c9adaac 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -3899,7 +3899,9 @@ package body Sem_Ch12 is
                    Local_Suppress_Stack_Top => Local_Suppress_Stack_Top,
                    Version                  => Ada_Version,
                    Version_Pragma           => Ada_Version_Pragma,
-                   Warnings                 => Save_Warnings));
+                   Warnings                 => Save_Warnings,
+                   SPARK_Mode               => SPARK_Mode,
+                   SPARK_Mode_Pragma        => SPARK_Mode_Pragma));
             end if;
          end if;
 
@@ -4245,7 +4247,9 @@ package body Sem_Ch12 is
                Local_Suppress_Stack_Top => Local_Suppress_Stack_Top,
                Version                  => Ada_Version,
                Version_Pragma           => Ada_Version_Pragma,
-               Warnings                 => Save_Warnings)),
+               Warnings                 => Save_Warnings,
+               SPARK_Mode               => SPARK_Mode,
+               SPARK_Mode_Pragma        => SPARK_Mode_Pragma)),
             Inlined_Body => True);
 
          Pop_Scope;
@@ -4363,7 +4367,9 @@ package body Sem_Ch12 is
                Local_Suppress_Stack_Top => Local_Suppress_Stack_Top,
                Version                  => Ada_Version,
                Version_Pragma           => Ada_Version_Pragma,
-               Warnings                 => Save_Warnings)),
+               Warnings                 => Save_Warnings,
+               SPARK_Mode               => SPARK_Mode,
+               SPARK_Mode_Pragma        => SPARK_Mode_Pragma)),
             Inlined_Body => True);
       end if;
    end Inline_Instance_Body;
@@ -4421,7 +4427,9 @@ package body Sem_Ch12 is
              Local_Suppress_Stack_Top => Local_Suppress_Stack_Top,
              Version                  => Ada_Version,
              Version_Pragma           => Ada_Version_Pragma,
-             Warnings                 => Save_Warnings));
+             Warnings                 => Save_Warnings,
+             SPARK_Mode               => SPARK_Mode,
+             SPARK_Mode_Pragma        => SPARK_Mode_Pragma));
          return True;
 
       --  Here if not inlined, or we ignore the inlining
@@ -9913,6 +9921,8 @@ package body Sem_Ch12 is
       Opt.Ada_Version          := Body_Info.Version;
       Opt.Ada_Version_Pragma   := Body_Info.Version_Pragma;
       Restore_Warnings (Body_Info.Warnings);
+      Opt.SPARK_Mode           := Body_Info.SPARK_Mode;
+      Opt.SPARK_Mode_Pragma    := Body_Info.SPARK_Mode_Pragma;
 
       if No (Gen_Body_Id) then
          Load_Parent_Of_Generic
@@ -10203,6 +10213,8 @@ package body Sem_Ch12 is
       Opt.Ada_Version          := Body_Info.Version;
       Opt.Ada_Version_Pragma   := Body_Info.Version_Pragma;
       Restore_Warnings (Body_Info.Warnings);
+      Opt.SPARK_Mode           := Body_Info.SPARK_Mode;
+      Opt.SPARK_Mode_Pragma    := Body_Info.SPARK_Mode_Pragma;
 
       if No (Gen_Body_Id) then
 
@@ -12091,7 +12103,9 @@ package body Sem_Ch12 is
                                 Local_Suppress_Stack_Top,
                               Version                  => Ada_Version,
                               Version_Pragma           => Ada_Version_Pragma,
-                              Warnings                 => Save_Warnings);
+                              Warnings                 => Save_Warnings,
+                              SPARK_Mode               => SPARK_Mode,
+                              SPARK_Mode_Pragma        => SPARK_Mode_Pragma);
 
                            --  Package instance
 
@@ -12133,7 +12147,9 @@ package body Sem_Ch12 is
                          Local_Suppress_Stack_Top => Local_Suppress_Stack_Top,
                          Version                  => Ada_Version,
                          Version_Pragma           => Ada_Version_Pragma,
-                         Warnings                 => Save_Warnings)),
+                         Warnings                 => Save_Warnings,
+                         SPARK_Mode               => SPARK_Mode,
+                         SPARK_Mode_Pragma        => SPARK_Mode_Pragma)),
                      Body_Optional => Body_Optional);
                end;
             end if;
@@ -13799,7 +13815,9 @@ package body Sem_Ch12 is
      (Gen_Unit : Entity_Id;
       Act_Unit : Entity_Id)
    is
-      Assertion_Status : constant Boolean := Assertions_Enabled;
+      Assertion_Status       : constant Boolean := Assertions_Enabled;
+      Save_SPARK_Mode        : constant SPARK_Mode_Type := SPARK_Mode;
+      Save_SPARK_Mode_Pragma : constant Node_Id := SPARK_Mode_Pragma;
 
    begin
       --  Regardless of the current mode, predefined units are analyzed in the
@@ -13822,6 +13840,12 @@ package body Sem_Ch12 is
          if Ada_Version >= Ada_2012 then
             Assertions_Enabled := Assertion_Status;
          end if;
+
+         --  SPARK_Mode for an instance is the one applicable at the point of
+         --  instantiation.
+
+         SPARK_Mode := Save_SPARK_Mode;
+         SPARK_Mode_Pragma := Save_SPARK_Mode_Pragma;
       end if;
 
       Current_Instantiated_Parent :=