[multiple changes]

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.

From-SVN: r235145

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index b72d52477fc1f35f3559cb1abe4712e0b2b91b3e..47029de63f0675969b30776c369403fe7efd8e55 100644 (file)
--- 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 2e7b36b54e8c0c2be09044d8b2a56df0c545dcd0..2832d615c76588ce801be4a9eea4b8bbe562d13d 100644 (file)
--- 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 d1e97fc13bc4636c22fe6f6e103344381b1c7461..bd86d18c7ff5871257bcc8697aef9384760aa214 100644 (file)
--- 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 9703943bdd1ea6693c39cf724b0b1e1595d09def..620c1663e0393d67fa870fb3125d83b0e4bcf9c8 100644 (file)
--- 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 b59fb6c11378e49f25cc00820a462731cb4845c9..b689b80011db530488f6a928263a2f75ea8483d9 100644 (file)
--- 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 7cf498de34d51d030cbd764fce938baad967d278..1dfa862b3df79bf79178838054a0f3b8a7cc7319 100644 (file)
--- 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);