[multiple changes]

2014-07-30  Pat Rogers  <rogers@adacore.com>

	* gnat_rm.texi: Minor word error.

2014-07-30  Ed Schonberg  <schonberg@adacore.com>

	* exp_prag.adb (Expand_Old): Insert declarationss of temporaries
	created to capture the value of the prefix of 'Old at the
	beginning of the current declarative part, to prevent data flow
	anomalies in the postcondition procedure that will follow.

2014-07-30  Yannick Moy  <moy@adacore.com>

	* debug.adb: Retire debug flag -gnatdQ.
	* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Check SPARK_Mode
	on decl, not on body.  Ignore predicate functions.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Remove use of
	debug flag -gnatdQ.  Correctly analyze SPARK_Mode on decl and
	body when generating a decl for a body on which SPARK_Mode aspect
	is given.
	* sem_prag.adb (Analyze_Pragma|SPARK_Mode): Reorder tests for
	attaching pragma to entity, to account for declaration not coming
	from source.
	* sem_res.adb (Resolve_Call): Issue warning and flag subprogram
	as not always inlined in GNATprove mode, when called in an
	assertion context.

From-SVN: r213271

9 files changed, 132 insertions, 36 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 81d1faa..408f6d0 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,30 @@
+2014-07-30  Pat Rogers  <rogers@adacore.com>
+
+	* gnat_rm.texi: Minor word error.
+
+2014-07-30  Ed Schonberg  <schonberg@adacore.com>
+
+	* exp_prag.adb (Expand_Old): Insert declarationss of temporaries
+	created to capture the value of the prefix of 'Old at the
+	beginning of the current declarative part, to prevent data flow
+	anomalies in the postcondition procedure that will follow.
+
+2014-07-30  Yannick Moy  <moy@adacore.com>
+
+	* debug.adb: Retire debug flag -gnatdQ.
+	* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Check SPARK_Mode
+	on decl, not on body.  Ignore predicate functions.
+	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Remove use of
+	debug flag -gnatdQ.  Correctly analyze SPARK_Mode on decl and
+	body when generating a decl for a body on which SPARK_Mode aspect
+	is given.
+	* sem_prag.adb (Analyze_Pragma|SPARK_Mode): Reorder tests for
+	attaching pragma to entity, to account for declaration not coming
+	from source.
+	* sem_res.adb (Resolve_Call): Issue warning and flag subprogram
+	as not always inlined in GNATprove mode, when called in an
+	assertion context.
+
 2014-07-30  Vincent Celier  <celier@adacore.com>
 
 	* debug.adb: Minor comment update.
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index a93af0f..64162ef 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -80,7 +80,7 @@ package body Debug is
    --  dN   No file name information in exception messages
    --  dO   Output immediate error messages
    --  dP   Do not check for controlled objects in preelaborable packages
-   --  dQ   Enable inlining of bodies-without-decl in GNATprove mode
+   --  dQ
    --  dR   Bypass check for correct version of s-rpc
    --  dS   Never convert numbers to machine numbers in Sem_Eval
    --  dT   Convert to machine numbers only for constant declarations
@@ -438,11 +438,6 @@ package body Debug is
    --       in preelaborable packages, but this restriction is a huge pain,
    --       especially in the predefined library units.
 
-   --  dQ   Enable inlining of bodies-without-decl in GNATprove mode. A decl is
-   --       created by the frontend so that the usual frontend inlining
-   --       mechanism can be used for formal verification. Under a debug flag
-   --       until fully reliable.
-
    --  dR   Bypass the check for a proper version of s-rpc being present
    --       to use the -gnatz? switch. This allows debugging of the use
    --       of stubs generation without needing to have GLADE (or some
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index 696d063..c48f3d2 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -440,6 +440,9 @@ package body Exp_Prag is
 
                --  Generate a temporary to capture the value of the prefix:
                --    Temp : <Pref type>;
+               --  Place that temporary at the beginning of declarations, to
+               --  prevent anomolies in the GNATprove flow analysis pass in
+               --  the precondition procedure that follows.
 
                Decl :=
                  Make_Object_Declaration (Loc,
@@ -448,7 +451,7 @@ package body Exp_Prag is
                      New_Occurrence_Of (Etype (Pref), Loc));
                Set_No_Initialization (Decl);
 
-               Append_To (Decls, Decl);
+               Prepend_To (Decls, Decl);
 
                --  Evaluate the prefix, generate:
                --    Temp := <Pref>;
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index 1867302..b0a018b 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -7215,7 +7215,7 @@ The meaning of a test case is that there is at least one context where
 that context, then @code{Ensures} holds when the subprogram returns.
 Mode @code{Nominal} indicates that the input context should also satisfy the
 precondition of the subprogram, and the output context should also satisfy its
-postcondition. More @code{Robustness} indicates that the precondition and
+postcondition. Mode @code{Robustness} indicates that the precondition and
 postcondition of the subprogram should be ignored for this test case.
 
 @node Pragma Thread_Local_Storage
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 4f09958..be556fb 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -1692,13 +1692,14 @@ package body Inline is
       elsif Is_Generic_Instance (Spec_Id) then
          return False;
 
-      --  Only inline subprograms whose body is marked SPARK_Mode On. Other
-      --  subprogram bodies should not be analyzed.
-
-      elsif Present (Body_Id)
-        and then (No (SPARK_Pragma (Body_Id))
-                   or else
-                     Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) /= On)
+      --  Only inline subprograms whose spec is marked SPARK_Mode On. For
+      --  the subprogram body, a similar check is performed after the body
+      --  is analyzed, as this is where a pragma SPARK_Mode might be inserted.
+
+      elsif Present (Spec_Id)
+        and then (No (SPARK_Pragma (Spec_Id))
+                    or else
+                  Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) /= On)
       then
          return False;
 
@@ -1708,6 +1709,12 @@ package body Inline is
       elsif Instantiation_Location (Sloc (Id)) /= No_Location then
          return False;
 
+      --  Predicate functions are treated specially by GNATprove. Do not inline
+      --  them.
+
+      elsif Is_Predicate_Function (Id) then
+         return False;
+
       --  Otherwise, this is a subprogram declared inside the private part of a
       --  package, or inside a package body, or locally in a subprogram, and it
       --  does not have any contract. Inline it.
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index a9fa109..f359b48 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -1497,7 +1497,7 @@ package body Sem_Ch13 is
          --  Start of processing for Analyze_One_Aspect
 
          begin
-            --  Skip aspect if already analyzed (not clear if this is needed)
+            --  Skip aspect if already analyzed, to avoid looping in some cases
 
             if Analyzed (Aspect) then
                goto Continue;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 393d557..72ee382 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3034,10 +3034,6 @@ package body Sem_Ch6 is
                if No (Spec_Id)
                  and then GNATprove_Mode
 
-                 --  Under a debug flag until remaining issues are fixed
-
-                 and then Debug_Flag_QQ
-
                  --  Inlining does not apply during pre-analysis of code
 
                  and then Full_Analysis
@@ -3077,13 +3073,51 @@ package body Sem_Ch6 is
                      New_Decl : constant Node_Id :=
                                   Make_Subprogram_Declaration (Loc,
                                     Copy_Separate_Tree (Specification (N)));
+                     SPARK_Mode_Aspect : Node_Id;
+                     Aspects : List_Id;
+                     Prag, Aspect : Node_Id;
 
                   begin
                      Insert_Before (N, New_Decl);
                      Move_Aspects (From => N, To => New_Decl);
+
+                     --  Mark the newly moved aspects as not analyzed, so that
+                     --  their effect on New_Decl is properly analyzed.
+
+                     Aspect := First (Aspect_Specifications (New_Decl));
+                     while Present (Aspect) loop
+                        Set_Analyzed (Aspect, False);
+                        Next (Aspect);
+                     end loop;
+
                      Analyze (New_Decl);
+
+                     --  The analysis of the generated subprogram declaration
+                     --  may have introduced pragmas, which need to be
+                     --  analyzed.
+
+                     Prag := Next (New_Decl);
+                     while Prag /= N loop
+                        Analyze (Prag);
+                        Next (Prag);
+                     end loop;
+
                      Spec_Id := Defining_Entity (New_Decl);
 
+                     --  If aspect SPARK_Mode was specified on the body, it
+                     --  needs to be repeated on the generated decl and the
+                     --  body. Since the original aspect was moved to the
+                     --  generated decl, copy it for the body.
+
+                     if Has_Aspect (Spec_Id, Aspect_SPARK_Mode) then
+                        SPARK_Mode_Aspect :=
+                          New_Copy (Find_Aspect (Spec_Id, Aspect_SPARK_Mode));
+                        Set_Analyzed (SPARK_Mode_Aspect, False);
+                        Aspects := New_List;
+                        Append (SPARK_Mode_Aspect, Aspects);
+                        Set_Aspect_Specifications (N, Aspects);
+                     end if;
+
                      Set_Specification (N, Body_Spec);
                      Body_Id := Analyze_Subprogram_Specification (Body_Spec);
                      Set_Corresponding_Spec (N, Spec_Id);
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 122d47c..983cb32 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -19830,11 +19830,6 @@ package body Sem_Prag is
                         raise Pragma_Exit;
                      end if;
 
-                  --  Skip internally generated code
-
-                  elsif not Comes_From_Source (Stmt) then
-                     null;
-
                   elsif Nkind (Stmt) in N_Generic_Declaration then
                      Error_Pragma
                        ("incorrect placement of pragma% on a generic");
@@ -19869,6 +19864,11 @@ package body Sem_Prag is
                      Set_SPARK_Pragma_Inherited     (Spec_Id, False);
                      return;
 
+                  --  Skip internally generated code
+
+                  elsif not Comes_From_Source (Stmt) then
+                     null;
+
                   --  The pragma does not apply to a legal construct, issue an
                   --  error and stop the analysis.
 
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 88356fd..92317ed 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6210,7 +6210,6 @@ package body Sem_Res is
       if GNATprove_Mode
         and then Is_Overloadable (Nam)
         and then SPARK_Mode = On
-        and then Full_Analysis
       then
          --  Retrieve the body to inline from the ultimate alias of Nam, if
          --  there is one, otherwise calls that should be inlined end up not
@@ -6220,23 +6219,54 @@ package body Sem_Res is
             Nam_Alias : constant Entity_Id := Ultimate_Alias (Nam);
             Decl : constant Node_Id := Unit_Declaration_Node (Nam_Alias);
          begin
-            if Nkind (Decl) = N_Subprogram_Declaration
-              and then Can_Be_Inlined_In_GNATprove_Mode (Nam_Alias, Empty)
-              and then No (Corresponding_Body (Decl))
+            --  If the subprogram is not eligible for inlining in GNATprove
+            --  mode, do nothing.
+
+            if not Can_Be_Inlined_In_GNATprove_Mode (Nam_Alias, Empty)
+              or else Nkind (Decl) /= N_Subprogram_Declaration
+              or else not Is_Inlined_Always (Nam_Alias)
             then
-               Error_Msg_NE
-                 ("?cannot inline call to & (body not seen yet)", N, Nam);
+               null;
+
+            --  Calls cannot be inlined inside assertions, as GNATprove treats
+            --  assertions as logic expressions.
+
+            elsif In_Assertion_Expr /= 0 then
+               Error_Msg_NE ("?cannot inline call to &", N, Nam);
+               Error_Msg_N ("\call appears in assertion expression", N);
                Set_Is_Inlined_Always (Nam_Alias, False);
 
-            elsif Nkind (Decl) = N_Subprogram_Declaration
-              and then Present (Body_To_Inline (Decl))
-              and then Is_Inlined (Nam_Alias)
-            then
-               if Is_Potentially_Unevaluated (N) then
+            --  Inlining should not be performed during pre-analysis
+
+            elsif Full_Analysis then
+
+               --  With the one-pass inlining technique, a call cannot be
+               --  inlined if the corresponding body has not been seen yet.
+
+               if No (Corresponding_Body (Decl)) then
+                  Error_Msg_NE
+                    ("?cannot inline call to & (body not seen yet)", N, Nam);
+                  Set_Is_Inlined_Always (Nam_Alias, False);
+
+               --  Nothing to do if there is no body to inline, indicating that
+               --  the subprogram is not suitable for inlining in GNATprove
+               --  mode.
+
+               elsif No (Body_To_Inline (Decl)) then
+                  null;
+
+               --  Calls cannot be inlined inside potentially unevaluated
+               --  expressions, as this would create complex actions inside
+               --  expressions, that are not handled by GNATprove.
+
+               elsif Is_Potentially_Unevaluated (N) then
                   Error_Msg_NE ("?cannot inline call to &", N, Nam);
                   Error_Msg_N
                     ("\call appears in potentially unevaluated context", N);
                   Set_Is_Inlined_Always (Nam_Alias, False);
+
+               --  Otherwise, inline the call
+
                else
                   Expand_Inlined_Call (N, Nam_Alias, Nam);
                end if;