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

	* sem_res.adb (Resolve_Entry_Call): reset
	Is_Overloaded flag after resolving calls to overloaded protected
	operations.
	* exp_spark.adb (Expand_SPARK): call
	Qualify_Entity_Names for tasking nodes, i.e. protected types,
	task types and entries.
	* exp_ch4.adb (Expand_N_If_Expression): Refine previous change
	in case of an unconstrained type.

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

	* sem_eval.adb, sem_eval.ads (Check_Non_Static_Context): Add
	comment to document usage of subprogram in GNATprove.



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

6 files changed, 52 insertions, 6 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index b72d52477fc..47029de63f0 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,19 @@
+2016-04-18  Arnaud Charlet  <charlet@adacore.com>
+
+	* sem_res.adb (Resolve_Entry_Call): reset
+	Is_Overloaded flag after resolving calls to overloaded protected
+	operations.
+	* exp_spark.adb (Expand_SPARK): call
+	Qualify_Entity_Names for tasking nodes, i.e. protected types,
+	task types and entries.
+	* exp_ch4.adb (Expand_N_If_Expression): Refine previous change
+	in case of an unconstrained type.
+
+2016-04-18  Yannick Moy  <moy@adacore.com>
+
+	* sem_eval.adb, sem_eval.ads (Check_Non_Static_Context): Add
+	comment to document usage of subprogram in GNATprove.
+
 2016-04-18  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_prag.adb (Analyze_Pragma, case Test_Case): Improve error
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index 2e7b36b54e8..2832d615c76 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -5450,8 +5450,10 @@ package body Exp_Ch4 is
 
          --  We now wrap the actions into the appropriate expression
 
-         if Minimize_Expression_With_Actions then
-
+         if Minimize_Expression_With_Actions
+           and then (Is_Elementary_Type (Underlying_Type (Typ))
+                      or else Is_Constrained (Underlying_Type (Typ)))
+         then
             --  If we can't use N_Expression_With_Actions nodes, then we insert
             --  the following sequence of actions (using Insert_Actions):
 
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index d1e97fc13bc..bd86d18c7ff 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -62,10 +62,13 @@ package body Exp_SPARK is
          --  user interaction. The verification back-end already takes care
          --  of qualifying names when needed.
 
-         when N_Block_Statement     |
-              N_Package_Body        |
-              N_Package_Declaration |
-              N_Subprogram_Body     =>
+         when N_Block_Statement            |
+              N_Entry_Declaration          |
+              N_Package_Body               |
+              N_Package_Declaration        |
+              N_Protected_Type_Declaration |
+              N_Subprogram_Body            |
+              N_Task_Type_Declaration      =>
             Qualify_Entity_Names (N);
 
          when N_Expanded_Name |
diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb
index 9703943bdd1..620c1663e03 100644
--- a/gcc/ada/sem_eval.adb
+++ b/gcc/ada/sem_eval.adb
@@ -467,6 +467,14 @@ package body Sem_Eval is
       --  non-static contexts, then ACVC test C490001 fails on Sparc/Solaris
       --  and SGI/Irix.
 
+      --  This conversion is always done by GNATprove on real literals in
+      --  non-static expressions, by calling Check_Non_Static_Context from
+      --  gnat2why, as GNATprove cannot do the conversion later contrary
+      --  to gigi. The frontend computes the information about which
+      --  expressions are static, which is used by gnat2why to call
+      --  Check_Non_Static_Context on exactly those real literals that are
+      --  not sub-expressions of static expressions.
+
       if Nkind (N) = N_Real_Literal
         and then not Is_Machine_Number (N)
         and then not Is_Generic_Type (Etype (N))
diff --git a/gcc/ada/sem_eval.ads b/gcc/ada/sem_eval.ads
index b59fb6c1137..b689b80011d 100644
--- a/gcc/ada/sem_eval.ads
+++ b/gcc/ada/sem_eval.ads
@@ -159,6 +159,11 @@ package Sem_Eval is
    --  customer for this procedure is Sem_Attr (because Eval_Attribute is
    --  there). There is also one special case arising from ranges (see body of
    --  Resolve_Range).
+   --
+   --  Note: this procedure is also called by GNATprove on real literals
+   --  that are not sub-expressions of static expressions, to convert them to
+   --  machine numbers, as GNATprove cannot perform this conversion contrary
+   --  to gigi.
 
    procedure Check_String_Literal_Length (N : Node_Id; Ttype : Entity_Id);
    --  N is either a string literal, or a constraint error node. In the latter
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 7cf498de34d..1dfa862b3df 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7654,6 +7654,18 @@ package body Sem_Res is
          Normalize_Actuals (N, Nam, False, Norm_OK);
          pragma Assert (Norm_OK);
          Set_Etype (N, Etype (Nam));
+
+         --  Reset the Is_Overloaded flag, since resolution is now completed
+
+         if Nkind (Entry_Name) = N_Selected_Component then
+            --  Simple entry call
+            Set_Is_Overloaded (Selector_Name (Entry_Name), False);
+
+         else pragma Assert (Nkind (Entry_Name) = N_Indexed_Component);
+            --  Call to member of entry family
+            Set_Is_Overloaded (Selector_Name (Prefix (Entry_Name)), False);
+
+         end if;
       end if;
 
       Resolve_Actuals (N, Nam);