[multiple changes]

2016-04-18  Yannick Moy  <moy@adacore.com>

	* sem_res.adb (Resolve_Call): Prevent inlining of
	calls inside expression functions.  Factor previous code issuing
	errors to call Cannot_Inline instead, which does appropriate
	processing of message for GNATprove.

2016-04-18  Arnaud Charlet  <charlet@adacore.com>

	* einfo.ads, sem_ch3.adb, sem_ch8.adb, osint-l.adb, rtsfind.adb,
	osint-b.adb: Cleanups.

2016-04-18  Yannick Moy  <moy@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Only create
	body to inline in GNATprove mode when SPARK_Mode On applies to
	subprogram body.
	* sem_prag.adb, sem_prag.ads (Get_SPARK_Mode_Type): Make function
	public.

2016-04-18  Eric Botcazou  <ebotcazou@adacore.com>

	* layout.adb: Fix minor typo in comment.
	* inline.adb: Fix minor pasto.
	* sem_ch12.ads: Fix minor typos in comments.

From-SVN: r235111

14 files changed, 123 insertions, 50 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index c4e73d1..c8e9141 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,29 @@
+2016-04-18  Yannick Moy  <moy@adacore.com>
+
+	* sem_res.adb (Resolve_Call): Prevent inlining of
+	calls inside expression functions.  Factor previous code issuing
+	errors to call Cannot_Inline instead, which does appropriate
+	processing of message for GNATprove.
+
+2016-04-18  Arnaud Charlet  <charlet@adacore.com>
+
+	* einfo.ads, sem_ch3.adb, sem_ch8.adb, osint-l.adb, rtsfind.adb,
+	osint-b.adb: Cleanups.
+
+2016-04-18  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Only create
+	body to inline in GNATprove mode when SPARK_Mode On applies to
+	subprogram body.
+	* sem_prag.adb, sem_prag.ads (Get_SPARK_Mode_Type): Make function
+	public.
+
+2016-04-18  Eric Botcazou  <ebotcazou@adacore.com>
+
+	* layout.adb: Fix minor typo in comment.
+	* inline.adb: Fix minor pasto.
+	* sem_ch12.ads: Fix minor typos in comments.
+
 2016-04-18  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_disp.adb (Check_Dispatching_Call): Major rewriting to
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index deae1b9..1fb29e4d 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -3449,7 +3449,7 @@ package Einfo is
 
 --    Next_Discriminant (synthesized)
 --       Applies to discriminants returned by First/Next_Discriminant. Returns
---       the next language-defined (ie: perhaps non-girder) discriminant by
+--       the next language-defined (i.e. perhaps non-girder) discriminant by
 --       following the chain of declared entities as long as the kind of the
 --       entity corresponds to a discriminant. Note that the discriminants
 --       might be the only components of the record. Returns Empty if there
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index bc7bc32..9a7b375 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -3866,7 +3866,6 @@ package body Inline is
          --  We can now complete the cleanup actions of scopes that contain
          --  pending instantiations (skipped for generic units, since we
          --  never need any cleanups in generic units).
-         --  pending instantiations.
 
          if Expander_Active
            and then not Is_Generic_Unit (Main_Unit_Entity)
diff --git a/gcc/ada/layout.adb b/gcc/ada/layout.adb
index c8d7ed7..cee5853 100644
--- a/gcc/ada/layout.adb
+++ b/gcc/ada/layout.adb
@@ -3318,7 +3318,7 @@ package body Layout is
             --  we have no way of doing that or easily figuring it out, so we
             --  don't bother.
 
-            --  Historical note. In versions of GNAT prior to Nov 6th, 2010, an
+            --  Historical note. In versions of GNAT prior to Nov 6th, 2011, an
             --  odd distinction was made between inherited alignments greater
             --  than the computed alignment (where the larger alignment was
             --  inherited) and inherited alignments smaller than the computed
diff --git a/gcc/ada/osint-b.adb b/gcc/ada/osint-b.adb
index 554d804..322bc6c 100644
--- a/gcc/ada/osint-b.adb
+++ b/gcc/ada/osint-b.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2001-2014, Free Software Foundation, Inc.         --
+--          Copyright (C) 2001-2015, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -153,7 +153,7 @@ package body Osint.B is
    -- More_Lib_Files --
    --------------------
 
-   function More_Lib_Files return Boolean renames  More_Files;
+   function More_Lib_Files return Boolean renames More_Files;
 
    ------------------------
    -- Next_Main_Lib_File --
diff --git a/gcc/ada/osint-l.adb b/gcc/ada/osint-l.adb
index 9cc8f4c..eb7e3c3 100644
--- a/gcc/ada/osint-l.adb
+++ b/gcc/ada/osint-l.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2001-2007, Free Software Foundation, Inc.         --
+--          Copyright (C) 2001-2015, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -29,7 +29,7 @@ package body Osint.L is
    -- More_Lib_Files --
    --------------------
 
-   function More_Lib_Files return Boolean renames  More_Files;
+   function More_Lib_Files return Boolean renames More_Files;
 
    ------------------------
    -- Next_Main_Lib_File --
diff --git a/gcc/ada/rtsfind.adb b/gcc/ada/rtsfind.adb
index 3c84bbe..e2d9cb5 100644
--- a/gcc/ada/rtsfind.adb
+++ b/gcc/ada/rtsfind.adb
@@ -730,7 +730,7 @@ package body Rtsfind is
 
          declare
             U : RT_Unit_Table_Record
-                  renames  RT_Unit_Table (RE_Unit_Table (E));
+                  renames RT_Unit_Table (RE_Unit_Table (E));
          begin
             if No (U.Entity) then
                U.Entity := S;
diff --git a/gcc/ada/sem_ch12.ads b/gcc/ada/sem_ch12.ads
index c54d735..faf8917 100644
--- a/gcc/ada/sem_ch12.ads
+++ b/gcc/ada/sem_ch12.ads
@@ -100,7 +100,7 @@ package Sem_Ch12 is
       Body_Optional : Boolean := False);
    --  Called after semantic analysis, to complete the instantiation of
    --  package instances. The flag Inlined_Body is set if the body is
-   --  being instantiated on the fly for inlined purposes.
+   --  being instantiated on the fly for inlining purposes.
    --
    --  The flag Body_Optional indicates that the call is for an instance
    --  that precedes the current instance in the same declarative part.
@@ -112,10 +112,10 @@ package Sem_Ch12 is
    --  appears in the context of some other unit P that contains an instance
    --  of G, we compile the body of I2, but not that of I1. However, when we
    --  compile U as the main unit, we compile both bodies. This will lead to
-   --  lead to link-time errors if the compilation of I1 generates public
-   --  symbols, because those in I2 will receive different names in both
-   --  cases. This forces us to analyze the body of I1 even when U is not the
-   --  main unit. We don't want this additional mechanism to generate an error
+   --  link-time errors if the compilation of I1 generates public symbols,
+   --  because those in I2 will receive different names in both cases.
+   --  This forces us to analyze the body of I1 even when U is not the main
+   --  unit. We don't want this additional mechanism to generate an error
    --  when the body of the generic for I1 is not present, and this is the
    --  reason for the presence of the flag Body_Optional, which is exchanged
    --  between the current procedure and Load_Parent_Of_Generic.
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 5f28a14..a010b54c 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -19828,7 +19828,7 @@ package body Sem_Ch3 is
                         end if;
 
                      elsif Is_Dispatching_Operation (Prim)
-                       and then Disp_Typ  /= Full_T
+                       and then Disp_Typ /= Full_T
                      then
 
                         --  Verify that it is not otherwise controlled by a
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 7f42479..a0a75b2 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -2178,6 +2178,11 @@ package body Sem_Ch6 is
       --  Check whether unanalyzed body has an aspect or pragma that may
       --  generate a SPARK contract.
 
+      function Body_Has_SPARK_Mode_On return Boolean;
+      --  Check whether SPARK_Mode On applies to the subprogram body, either
+      --  because it is specified directly on the body, or because it is
+      --  inherited from the enclosing subprogram or package.
+
       procedure Build_Subprogram_Declaration;
       --  Create a matching subprogram declaration for subprogram body N
 
@@ -2272,6 +2277,53 @@ package body Sem_Ch6 is
          return False;
       end Body_Has_Contract;
 
+      ----------------------------
+      -- Body_Has_SPARK_Mode_On --
+      ----------------------------
+
+      function Body_Has_SPARK_Mode_On return Boolean is
+         Decls : constant List_Id := Declarations (N);
+         Item  : Node_Id;
+
+      begin
+         --  Check for SPARK_Mode aspect
+
+         if Present (Aspect_Specifications (N)) then
+            Item := First (Aspect_Specifications (N));
+            while Present (Item) loop
+               if Get_Aspect_Id (Item) = Aspect_SPARK_Mode then
+                  return No (Expression (Item))
+                           or else
+                        (Nkind (Expression (Item)) = N_Identifier
+                           and then
+                         Get_SPARK_Mode_Type (Chars (Expression (Item))) = On);
+               end if;
+
+               Next (Item);
+            end loop;
+         end if;
+
+         --  Check for SPARK_Mode pragma
+
+         if Present (Decls) then
+            Item := First (Decls);
+            while Present (Item) loop
+               if Nkind (Item) = N_Pragma
+                 and then Get_Pragma_Id (Item) = Pragma_SPARK_Mode
+               then
+                  return Get_SPARK_Mode_From_Pragma (Item) = On;
+               end if;
+
+               Next (Item);
+            end loop;
+         end if;
+
+         --  Applicable SPARK_Mode is inherited from the enclosing subprogram
+         --  or package.
+
+         return SPARK_Mode = On;
+      end Body_Has_SPARK_Mode_On;
+
       ----------------------------------
       -- Build_Subprogram_Declaration --
       ----------------------------------
@@ -3695,6 +3747,7 @@ package body Sem_Ch6 is
         and then Present (Spec_Id)
         and then
           Nkind (Unit_Declaration_Node (Spec_Id)) = N_Subprogram_Declaration
+        and then Body_Has_SPARK_Mode_On
         and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id)
         and then not Body_Has_Contract
       then
@@ -3814,18 +3867,6 @@ package body Sem_Ch6 is
 
       Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id);
 
-      --  If SPARK_Mode for body is not On, disable frontend inlining for this
-      --  subprogram in GNATprove mode, as its body should not be analyzed.
-
-      if SPARK_Mode /= On
-        and then GNATprove_Mode
-        and then Present (Spec_Id)
-        and then Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Declaration
-      then
-         Set_Body_To_Inline (Parent (Parent (Spec_Id)), Empty);
-         Set_Is_Inlined_Always (Spec_Id, False);
-      end if;
-
       --  Check completion, and analyze the statements
 
       Check_Completion;
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index e8f7b1f..73303f4 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -7526,7 +7526,7 @@ package body Sem_Ch8 is
          --  array of Boolean type.
 
          when Name_Op_And | Name_Op_Not | Name_Op_Or  | Name_Op_Xor =>
-            while Id  /= Priv_Id loop
+            while Id /= Priv_Id loop
                if Valid_Boolean_Arg (Id) and then Is_Base_Type (Id) then
                   Add_Implicit_Operator (Id);
                   return True;
@@ -7538,7 +7538,7 @@ package body Sem_Ch8 is
          --  Equality: look for any non-limited type (result is Boolean)
 
          when Name_Op_Eq | Name_Op_Ne =>
-            while Id  /= Priv_Id loop
+            while Id /= Priv_Id loop
                if Is_Type (Id)
                  and then not Is_Limited_Type (Id)
                  and then Is_Base_Type (Id)
@@ -7553,7 +7553,7 @@ package body Sem_Ch8 is
          --  Comparison operators: scalar type, or array of scalar
 
          when Name_Op_Lt | Name_Op_Le | Name_Op_Gt | Name_Op_Ge =>
-            while Id  /= Priv_Id loop
+            while Id /= Priv_Id loop
                if (Is_Scalar_Type (Id)
                     or else (Is_Array_Type (Id)
                               and then Is_Scalar_Type (Component_Type (Id))))
@@ -7576,7 +7576,7 @@ package body Sem_Ch8 is
               Name_Op_Multiply |
               Name_Op_Divide   |
               Name_Op_Expon    =>
-            while Id  /= Priv_Id loop
+            while Id /= Priv_Id loop
                if Is_Numeric_Type (Id) and then Is_Base_Type (Id) then
                   Add_Implicit_Operator (Id);
                   return True;
@@ -7588,7 +7588,7 @@ package body Sem_Ch8 is
          --  Concatenation: any one-dimensional array type
 
          when Name_Op_Concat =>
-            while Id  /= Priv_Id loop
+            while Id /= Priv_Id loop
                if Is_Array_Type (Id)
                  and then Number_Dimensions (Id) = 1
                  and then Is_Base_Type (Id)
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 534681a..1d64de5 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -235,11 +235,6 @@ package body Sem_Prag is
    --  original one, following the renaming chain) is returned. Otherwise the
    --  entity is returned unchanged. Should be in Einfo???
 
-   function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type;
-   --  Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram
-   --  Get_SPARK_Mode_Type. Convert a name into a corresponding value of type
-   --  SPARK_Mode_Type.
-
    function Has_Extra_Parentheses (Clause : Node_Id) return Boolean;
    --  Subsidiary to the analysis of pragmas Depends and Refined_Depends.
    --  Determine whether dependency clause Clause is surrounded by extra
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index ce05bfd..3bc2f65 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -383,6 +383,11 @@ package Sem_Prag is
    function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type;
    --  Given a pragma SPARK_Mode node, return corresponding mode id
 
+   function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type;
+   --  Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram
+   --  Get_SPARK_Mode_From_Pragma. Convert a name into a corresponding value
+   --  of type SPARK_Mode_Type.
+
    procedure Initialize;
    --  Initializes data structures used for pragma processing. Must be called
    --  before analyzing each new main source program.
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 8eb8ac0..bd4b562 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6428,16 +6428,14 @@ package body Sem_Res is
             --  assertions as logic expressions.
 
             elsif In_Assertion_Expr /= 0 then
-               Error_Msg_NE ("info: no contextual analysis of &?", N, Nam);
-               Error_Msg_N ("\call appears in assertion expression", N);
-               Set_Is_Inlined_Always (Nam_UA, False);
+               Cannot_Inline
+                 ("cannot inline & (in assertion expression)?", N, Nam_UA);
 
             --  Calls cannot be inlined inside default expressions
 
             elsif In_Default_Expr then
-               Error_Msg_NE ("info: no contextual analysis of &?", N, Nam);
-               Error_Msg_N ("\call appears in default expression", N);
-               Set_Is_Inlined_Always (Nam_UA, False);
+               Cannot_Inline
+                 ("cannot inline & (in default expression)?", N, Nam_UA);
 
             --  Inlining should not be performed during pre-analysis
 
@@ -6447,10 +6445,8 @@ package body Sem_Res is
                --  inlined if the corresponding body has not been seen yet.
 
                if No (Body_Id) then
-                  Error_Msg_NE
-                    ("info: no contextual analysis of & (body not seen yet)?",
-                     N, Nam);
-                  Set_Is_Inlined_Always (Nam_UA, False);
+                  Cannot_Inline
+                    ("cannot inline & (body not seen yet)?", N, Nam_UA);
 
                --  Nothing to do if there is no body to inline, indicating that
                --  the subprogram is not suitable for inlining in GNATprove
@@ -6459,15 +6455,26 @@ package body Sem_Res is
                elsif No (Body_To_Inline (Nam_Decl)) then
                   null;
 
+               --  Do not inline calls inside expression functions, as this
+               --  would prevent interpreting them as logical formulas in
+               --  GNATprove.
+
+               elsif Present (Current_Subprogram)
+                       and then
+                     Is_Expression_Function_Or_Completion (Current_Subprogram)
+               then
+                  Cannot_Inline
+                    ("cannot inline & (inside expression function)?",
+                     N, Nam_UA);
+
                --  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 ("info: no contextual analysis of &?", N, Nam);
-                  Error_Msg_N
-                    ("\call appears in potentially unevaluated context", N);
-                  Set_Is_Inlined_Always (Nam_UA, False);
+                  Cannot_Inline
+                    ("cannot inline & (in potentially unevaluated context)?",
+                     N, Nam_UA);
 
                --  Otherwise, inline the call