[multiple changes]

2014-07-30  Robert Dewar  <dewar@adacore.com>

	* sem_ch4.adb (Analyze_If_Expression): Resolve condition before
	analyzing branches.
	* sem_eval.adb (Out_Of_Range): Check for statically unevaluated
	expression case.

2014-07-30  Robert Dewar  <dewar@adacore.com>

	* sem_ch13.adb (Analyze_Aspect, predicate cases): Diagnose use
	of predicate aspect on entity other than a type.

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

	* sem_ch6.adb (Body_Has_Contract): New predicate to determine
	when a subprogram body without a previous spec cannot be inlined
	in GNATprove mode, because it includes aspects or pragmas that
	generate a SPARK contract clause.
	* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): A subprogram
	instance cannot be inlined.

From-SVN: r213247

6 files changed, 128 insertions, 7 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 768c313..dea492c 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,26 @@
 2014-07-30  Robert Dewar  <dewar@adacore.com>
 
+	* sem_ch4.adb (Analyze_If_Expression): Resolve condition before
+	analyzing branches.
+	* sem_eval.adb (Out_Of_Range): Check for statically unevaluated
+	expression case.
+
+2014-07-30  Robert Dewar  <dewar@adacore.com>
+
+	* sem_ch13.adb (Analyze_Aspect, predicate cases): Diagnose use
+	of predicate aspect on entity other than a type.
+
+2014-07-30  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch6.adb (Body_Has_Contract): New predicate to determine
+	when a subprogram body without a previous spec cannot be inlined
+	in GNATprove mode, because it includes aspects or pragmas that
+	generate a SPARK contract clause.
+	* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): A subprogram
+	instance cannot be inlined.
+
+2014-07-30  Robert Dewar  <dewar@adacore.com>
+
 	* debug.adb: Document that d7 suppresses compilation time output.
 	* errout.adb (Write_Header): Include compilation time in
 	header output.
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 69388ac..c2ee807 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -1490,13 +1490,12 @@ package body Inline is
 
       function Has_Some_Contract (Id : Entity_Id) return Boolean is
          Items : constant Node_Id := Contract (Id);
+
       begin
          return Present (Items)
            and then (Present (Pre_Post_Conditions (Items))
-                       or else
-                     Present (Contract_Test_Cases (Items))
-                       or else
-                     Present (Classifications (Items)));
+                      or else Present (Contract_Test_Cases (Items))
+                      or else Present (Classifications (Items)));
       end Has_Some_Contract;
 
       --------------------------
@@ -1589,6 +1588,9 @@ package body Inline is
       then
          return False;
 
+      elsif Is_Generic_Instance (Spec_Id) then
+         return False;
+
       --  Only inline subprograms whose body is marked SPARK_Mode On
 
       elsif No (SPARK_Pragma (Body_Id))
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index c7d039d..f6a8707 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -1778,6 +1778,15 @@ package body Sem_Ch13 is
                     Aspect_Predicate         |
                     Aspect_Static_Predicate  =>
 
+                  --  These aspects apply only to subtypes
+
+                  if not Is_Type (E) then
+                     Error_Msg_N
+                       ("predicate can only be specified for a subtype",
+                        Aspect);
+                     goto Continue;
+                  end if;
+
                   --  Construct the pragma (always a pragma Predicate, with
                   --  flags recording whether it is static/dynamic). We also
                   --  set flags recording this in the type itself.
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 9686197..f7d6aa8 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -2046,7 +2046,18 @@ package body Sem_Ch4 is
          Check_Compiler_Unit ("if expression", N);
       end if;
 
+      --  Analyze and resolve the condition. We need to resolve this now so
+      --  that it gets folded to True/False if possible, before we analyze
+      --  the THEN/ELSE branches, because when analyzing these branches, we
+      --  may call Is_Statically_Unevaluated, which expects the condition of
+      --  an enclosing IF to have been analyze/resolved/evaluated.
+
       Analyze_Expression (Condition);
+      Resolve (Condition, Any_Boolean);
+
+      --  Analyze THEN expression and (if present) ELSE expression. For those
+      --  we delay resolution in the normal manner, because of overloading etc.
+
       Analyze_Expression (Then_Expr);
 
       if Present (Else_Expr) then
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 815ab54..e2b267b 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -2167,6 +2167,10 @@ package body Sem_Ch6 is
       --  Analyze the aspect specifications of a subprogram body [stub]. It is
       --  assumed that N has aspects.
 
+      function Body_Has_Contract return Boolean;
+      --  Check whether unanalyzed body has an aspect or pragma that may
+      --  generate a SPARK contrac.
+
       procedure Check_Anonymous_Return;
       --  Ada 2005: if a function returns an access type that denotes a task,
       --  or a type that contains tasks, we must create a master entity for
@@ -2339,6 +2343,68 @@ package body Sem_Ch6 is
          end if;
       end Analyze_Aspects_On_Body_Or_Stub;
 
+      -----------------------
+      -- Body_Has_Contract --
+      -----------------------
+
+      function Body_Has_Contract return Boolean is
+         Decls  : constant List_Id := Declarations (N);
+         A_Spec : Node_Id;
+         A      : Aspect_Id;
+         Decl   : Node_Id;
+         P_Id   : Pragma_Id;
+
+      begin
+         --  Check for unanalyzed aspects in the body that will
+         --  generate a contract.
+
+         if Present (Aspect_Specifications (N)) then
+            A_Spec := First (Aspect_Specifications (N));
+            while Present (A_Spec) loop
+               A := Get_Aspect_Id (Chars (Identifier (A_Spec)));
+
+               if A = Aspect_Contract_Cases
+                 or else A = Aspect_Depends
+                 or else A = Aspect_Global
+                 or else A = Aspect_Pre
+                 or else A = Aspect_Precondition
+                 or else A = Aspect_Post
+                 or else A = Aspect_Postcondition
+               then
+                  return True;
+               end if;
+
+               Next (A_Spec);
+            end loop;
+         end if;
+
+         --  Check for pragmas that may generate a contract.
+
+         if Present (Decls) then
+            Decl := First (Decls);
+            while Present (Decl) loop
+               if Nkind (Decl) = N_Pragma then
+                  P_Id := Get_Pragma_Id (Pragma_Name (Decl));
+
+                  if P_Id = Pragma_Contract_Cases
+                    or else P_Id = Pragma_Depends
+                    or else P_Id = Pragma_Global
+                    or else P_Id = Pragma_Pre
+                    or else P_Id = Pragma_Precondition
+                    or else P_Id = Pragma_Post
+                    or else P_Id = Pragma_Postcondition
+                  then
+                     return True;
+                  end if;
+               end if;
+
+               Next (Decl);
+            end loop;
+         end if;
+
+         return False;
+      end Body_Has_Contract;
+
       ----------------------------
       -- Check_Anonymous_Return --
       ----------------------------
@@ -2969,6 +3035,7 @@ package body Sem_Ch6 is
                  and then Full_Analysis
                  and then Comes_From_Source (Body_Id)
                  and then Is_List_Member (N)
+                 and then not Body_Has_Contract
                then
                   declare
                      Body_Spec : constant Node_Id :=
@@ -3410,6 +3477,7 @@ package body Sem_Ch6 is
            and then
              Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Declaration
            and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id)
+           and then not Body_Has_Contract
          then
             Build_Body_To_Inline (N, Spec_Id);
          end if;
@@ -3437,6 +3505,7 @@ package body Sem_Ch6 is
         and then Present (Spec_Id)
         and then Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Declaration
         and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id)
+        and then not Body_Has_Contract
       then
          Check_And_Build_Body_To_Inline (N, Spec_Id, Body_Id);
       end if;
diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb
index addd331..6c41a4e 100644
--- a/gcc/ada/sem_eval.adb
+++ b/gcc/ada/sem_eval.adb
@@ -5280,15 +5280,22 @@ package body Sem_Eval is
       --  If we have the static expression case, then this is an illegality
       --  in Ada 95 mode, except that in an instance, we never generate an
       --  error (if the error is legitimate, it was already diagnosed in the
-      --  template). The expression to compute the length of a packed array is
-      --  attached to the array type itself, and deserves a separate message.
+      --  template).
 
       if Is_Static_Expression (N)
         and then not In_Instance
         and then not In_Inlined_Body
         and then Ada_Version >= Ada_95
       then
-         if Nkind (Parent (N)) = N_Defining_Identifier
+         --  No message if we are staticallly unevaluated
+
+         if Is_Statically_Unevaluated (N) then
+            null;
+
+         --  The expression to compute the length of a packed array is attached
+         --  to the array type itself, and deserves a separate message.
+
+         elsif Nkind (Parent (N)) = N_Defining_Identifier
            and then Is_Array_Type (Parent (N))
            and then Present (Packed_Array_Impl_Type (Parent (N)))
            and then Present (First_Rep_Item (Parent (N)))
@@ -5298,6 +5305,8 @@ package body Sem_Eval is
               First_Rep_Item (Parent (N)));
             Rewrite (N, Make_Integer_Literal (Sloc (N), Uint_1));
 
+         --  All cases except the special array case
+
          else
             Apply_Compile_Time_Constraint_Error
               (N, "value not in range of}", CE_Range_Check_Failed);