2015-10-27 Hristian Kirtchev <kirtchev@adacore.com>

	* inline.adb (Is_Expression_Function): Removed.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): An internally
	generated subprogram body that completes an expression function
	inherits the SPARK_Mode from the spec.
	* sem_res.adb (Resolve_Call): Update all calls to
	Is_Expression_Function.
	* sem_util.ads, sem_util.adb (Is_Expression_Function): Reimplemented.
	(Is_Expression_Function_Or_Completion): New routine.



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

6 files changed, 85 insertions, 44 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index e18d49bb91f..de9d8b3c61e 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,16 @@
 2015-10-27  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* inline.adb (Is_Expression_Function): Removed.
+	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): An internally
+	generated subprogram body that completes an expression function
+	inherits the SPARK_Mode from the spec.
+	* sem_res.adb (Resolve_Call): Update all calls to
+	Is_Expression_Function.
+	* sem_util.ads, sem_util.adb (Is_Expression_Function): Reimplemented.
+	(Is_Expression_Function_Or_Completion): New routine.
+
+2015-10-27  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* lib-xref-spark_specific.adb, a-dirval-mingw.adb, exp_ch6.adb,
 	sem_ch8.adb, s-os_lib.adb: Minor reformatting.
 
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 99b536c72d3..1330df9b918 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -1357,10 +1357,6 @@ package body Inline is
       --  Returns True if subprogram Id is defined in the visible part of a
       --  package specification.
 
-      function Is_Expression_Function (Id : Entity_Id) return Boolean;
-      --  Returns True if subprogram Id was defined originally as an expression
-      --  function.
-
       ---------------------------------------------------
       -- Has_Formal_With_Discriminant_Dependent_Fields --
       ---------------------------------------------------
@@ -1472,20 +1468,6 @@ package body Inline is
            and then List_Containing (Decl) = Visible_Declarations (P);
       end In_Package_Visible_Spec;
 
-      ----------------------------
-      -- Is_Expression_Function --
-      ----------------------------
-
-      function Is_Expression_Function (Id : Entity_Id) return Boolean is
-         Decl : Node_Id := Parent (Parent (Id));
-      begin
-         if Nkind (Parent (Id)) = N_Defining_Program_Unit_Name then
-            Decl := Parent (Decl);
-         end if;
-
-         return Nkind (Original_Node (Decl)) = N_Expression_Function;
-      end Is_Expression_Function;
-
       ------------------------
       -- Is_Unit_Subprogram --
       ------------------------
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 85d864a2c0c..9fcaed9c333 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3493,15 +3493,40 @@ package body Sem_Ch6 is
          Generate_Reference_To_Formals (Body_Id);
       end if;
 
-      --  Set the SPARK_Mode from the current context (may be overwritten later
-      --  with explicit pragma). This is not done for entry barrier functions
-      --  because they are generated outside the protected type and should not
-      --  carry the mode of the enclosing context.
+      --  Entry barrier functions are generated outside the protected type and
+      --  should not carry the SPARK_Mode of the enclosing context.
 
       if Nkind (N) = N_Subprogram_Body
         and then Is_Entry_Barrier_Function (N)
       then
          null;
+
+      --  The body is generated as part of expression function expansion. When
+      --  the expression function appears in the visible declarations of a
+      --  package, the body is added to the private declarations. Since both
+      --  declarative lists may be subject to a different SPARK_Mode, inherit
+      --  the mode of the spec.
+
+      --    package P with SPARK_Mode is
+      --       function Expr_Func ... is (...);         --  original
+      --       [function Expr_Func ...;]                --  generated spec
+      --                                                --    mode is ON
+      --    private
+      --       pragma SPARK_Mode (Off);
+      --       [function Expr_Func ... is return ...;]  --  generated body
+      --    end P;                                      --    mode is ON
+
+      elsif not Comes_From_Source (N)
+        and then Present (Prev_Id)
+        and then Is_Expression_Function (Prev_Id)
+      then
+         Set_SPARK_Pragma (Body_Id, SPARK_Pragma (Prev_Id));
+         Set_SPARK_Pragma_Inherited
+           (Body_Id, SPARK_Pragma_Inherited (Prev_Id));
+
+      --  Set the SPARK_Mode from the current context (may be overwritten later
+      --  with explicit pragma).
+
       else
          Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
          Set_SPARK_Pragma_Inherited (Body_Id);
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 689e1cbca16..13034546ce8 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -5793,10 +5793,11 @@ package body Sem_Res is
       --  is frozen in the usual fashion, by the appearance of a real body,
       --  or at the end of a declarative part.
 
-      if Is_Entity_Name (Subp) and then not In_Spec_Expression
-        and then not Is_Expression_Function (Current_Scope)
+      if Is_Entity_Name (Subp)
+        and then not In_Spec_Expression
+        and then not Is_Expression_Function_Or_Completion (Current_Scope)
         and then
-          (not Is_Expression_Function (Entity (Subp))
+          (not Is_Expression_Function_Or_Completion (Entity (Subp))
             or else Scope (Entity (Subp)) = Current_Scope)
       then
          Freeze_Expression (Subp);
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index d8567c59e7f..a576862dcec 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -5081,7 +5081,6 @@ package body Sem_Util is
               (Is_Concurrent_Type (Scope (Discriminal_Link (E)))
                 or else
                   Is_Concurrent_Record_Type (Scope (Discriminal_Link (E)))));
-
    end Denotes_Discriminant;
 
    -------------------------
@@ -11677,26 +11676,46 @@ package body Sem_Util is
    ----------------------------
 
    function Is_Expression_Function (Subp : Entity_Id) return Boolean is
-      Decl : Node_Id;
-
    begin
-      if Ekind (Subp) /= E_Function then
+      if Ekind_In (Subp, E_Function, E_Subprogram_Body) then
+         return
+           Nkind (Original_Node (Unit_Declaration_Node (Subp))) =
+             N_Expression_Function;
+      else
          return False;
+      end if;
+   end Is_Expression_Function;
+
+   ------------------------------------------
+   -- Is_Expression_Function_Or_Completion --
+   ------------------------------------------
+
+   function Is_Expression_Function_Or_Completion
+     (Subp : Entity_Id) return Boolean
+   is
+      Subp_Decl : Node_Id;
+
+   begin
+      if Ekind (Subp) = E_Function then
+         Subp_Decl := Unit_Declaration_Node (Subp);
+
+         --  The function declaration is either an expression function or is
+         --  completed by an expression function body.
+
+         return
+           Is_Expression_Function (Subp)
+             or else (Nkind (Subp_Decl) = N_Subprogram_Declaration
+                       and then Present (Corresponding_Body (Subp_Decl))
+                       and then Is_Expression_Function
+                                  (Corresponding_Body (Subp_Decl)));
+
+      elsif Ekind (Subp) = E_Subprogram_Body then
+         return Is_Expression_Function (Subp);
 
       else
-         Decl := Unit_Declaration_Node (Subp);
-         return Nkind (Decl) = N_Subprogram_Declaration
-           and then
-             (Nkind (Original_Node (Decl)) = N_Expression_Function
-               or else
-                 (Present (Corresponding_Body (Decl))
-                   and then
-                     Nkind (Original_Node
-                             (Unit_Declaration_Node
-                               (Corresponding_Body (Decl)))) =
-                                  N_Expression_Function));
+         return False;
       end if;
-   end Is_Expression_Function;
+   end Is_Expression_Function_Or_Completion;
 
    -----------------------
    -- Is_EVF_Expression --
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 67bc7f19403..03a1c21ba66 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1334,9 +1334,12 @@ package Sem_Util is
    --  Determine whether entity Id is the spec entity of an entry [family]
 
    function Is_Expression_Function (Subp : Entity_Id) return Boolean;
-   --  Predicate to determine whether a scope entity comes from a rewritten
-   --  expression function call, and should be inlined unconditionally. Also
-   --  used to determine that such a call does not constitute a freeze point.
+   --  Determine whether subprogram [body] Subp denotes an expression function
+
+   function Is_Expression_Function_Or_Completion
+     (Subp : Entity_Id) return Boolean;
+   --  Determine whether subprogram [body] Subp denotes an expression function
+   --  or is completed by an expression function body.
 
    function Is_EVF_Expression (N : Node_Id) return Boolean;
    --  Determine whether node N denotes a reference to a formal parameter of