[multiple changes]

2014-08-01  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_res.adb (Resolve_Call): Do not perform
	GNATprove-specific inlining while within a generic.

2014-08-01  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch4.adb (Analyze_Case_Expression): Handle properly a
	case expression with incompatible alternatives, when the first
	alternative is overloaded.

From-SVN: r213460

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index c2bd64a47b2790923042f53c4086351fa31a2c21..f829f8405968b6ca51cb40f2c8eee3523d075029 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,14 @@
+2014-08-01  Hristian Kirtchev  <kirtchev@adacore.com>
+
+       * sem_res.adb (Resolve_Call): Do not perform
+       GNATprove-specific inlining while within a generic.
+
+2014-08-01  Ed Schonberg  <schonberg@adacore.com>
+
+       * sem_ch4.adb (Analyze_Case_Expression): Handle properly a
+       case expression with incompatible alternatives, when the first
+       alternative is overloaded.
+
 2014-08-01  Ed Schonberg  <schonberg@adacore.com>
 
        * sem_res.adb (Check_Parameterless_Call): Use Relocate_Node

diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 64f0a7451f66478538e60c233fe0588750cf72ca..26496dfbba997f28d667a37e0d8d56ce1437bfe0 100644 (file)
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -1363,6 +1363,9 @@ package body Sem_Ch4 is
       Others_Present : Boolean;
       --  Indicates if Others was present
 
+      Wrong_Alt : Node_Id;
+      --  For error reporting
+
    --  Start of processing for Analyze_Case_Expression
 
    begin
@@ -1415,6 +1418,9 @@ package body Sem_Ch4 is
 
                if No (Alt) then
                   Add_One_Interp (N, It.Typ, It.Typ);
+
+               else
+                  Wrong_Alt := Alt;
                end if;
 
                Get_Next_Interp (I, It);
@@ -1441,6 +1447,12 @@ package body Sem_Ch4 is
          return;
       end if;
 
+      if Etype (N) = Any_Type and then Present (Wrong_Alt) then
+         Error_Msg_N ("type incompatible with that of previous alternatives",
+           Expression (Wrong_Alt));
+         return;
+      end if;
+
       --  If the case expression is a formal object of mode in out, then
       --  treat it as having a nonstatic subtype by forcing use of the base
       --  type (which has to get passed to Check_Case_Choices below).  Also

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index ac3acd428845649b54bd08ff880531c533be0d43..034ca5865f4f7359ddf82bf0f234745a4492ab96 100644 (file)
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6208,14 +6208,15 @@ package body Sem_Res is
       Eval_Call (N);
       Check_Elab_Call (N);
 
-      --  In GNATprove mode, expansion is disabled, but we want to inline
-      --  some subprograms to facilitate formal verification. Indirect calls,
-      --  through a subprogram type, cannot be inlined. Inlining is only
-      --  performed for calls for which SPARK_Mode is On.
+      --  In GNATprove mode, expansion is disabled, but we want to inline some
+      --  subprograms to facilitate formal verification. Indirect calls through
+      --  a subprogram type or within a generic cannot be inlined. Inlining is
+      --  performed only for calls subject to SPARK_Mode on.
 
       if GNATprove_Mode
-        and then Is_Overloadable (Nam)
         and then SPARK_Mode = On
+        and then Is_Overloadable (Nam)
+        and then not Inside_A_Generic
       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