diff mbox

[Ada] Fix side-effect removal for GNATprove

Message ID 20170427101516.GA100543@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet April 27, 2017, 10:15 a.m. UTC
GNATprove relies on side-effects being removed and value being fixed from
renamings, which was not the case for the renaming of a qualified
expression. Now done.

Tested on x86_64-pc-linux-gnu, committed on trunk

2017-04-27  Yannick Moy  <moy@adacore.com>

	* exp_util.ads, exp_util.adb (Evaluate_Name): Force evaluation
	of expression being qualified, when not an object name, or else
	evaluate the underlying name.
diff mbox

Patch

Index: exp_util.adb
===================================================================
--- exp_util.adb	(revision 247293)
+++ exp_util.adb	(working copy)
@@ -4724,72 +4724,85 @@ 
    -------------------
 
    procedure Evaluate_Name (Nam : Node_Id) is
-      K : constant Node_Kind := Nkind (Nam);
-
    begin
-      --  For an explicit dereference, we simply force the evaluation of the
-      --  name expression. The dereference provides a value that is the address
-      --  for the renamed object, and it is precisely this value that we want
-      --  to preserve.
+      --  For an attribute reference or an indexed component, evaluate the
+      --  prefix, which is itself a name, recursively, and then force the
+      --  evaluation of all the subscripts (or attribute expressions).
 
-      if K = N_Explicit_Dereference then
-         Force_Evaluation (Prefix (Nam));
+      case Nkind (Nam) is
+         when N_Attribute_Reference
+            | N_Indexed_Component
+         =>
+            Evaluate_Name (Prefix (Nam));
 
-      --  For a selected component, we simply evaluate the prefix
+            declare
+               E : Node_Id;
 
-      elsif K = N_Selected_Component then
-         Evaluate_Name (Prefix (Nam));
+            begin
+               E := First (Expressions (Nam));
+               while Present (E) loop
+                  Force_Evaluation (E);
 
-      --  For an indexed component, or an attribute reference, we evaluate the
-      --  prefix, which is itself a name, recursively, and then force the
-      --  evaluation of all the subscripts (or attribute expressions).
+                  if Original_Node (E) /= E then
+                     Set_Do_Range_Check (E,
+                                         Do_Range_Check (Original_Node (E)));
+                  end if;
 
-      elsif Nkind_In (K, N_Indexed_Component, N_Attribute_Reference) then
-         Evaluate_Name (Prefix (Nam));
+                  Next (E);
+               end loop;
+            end;
 
-         declare
-            E : Node_Id;
+         --  For an explicit dereference, we simply force the evaluation of
+         --  the name expression. The dereference provides a value that is the
+         --  address for the renamed object, and it is precisely this value
+         --  that we want to preserve.
 
-         begin
-            E := First (Expressions (Nam));
-            while Present (E) loop
-               Force_Evaluation (E);
+         when N_Explicit_Dereference =>
+            Force_Evaluation (Prefix (Nam));
 
-               if Original_Node (E) /= E then
-                  Set_Do_Range_Check (E, Do_Range_Check (Original_Node (E)));
-               end if;
+         --  For a function call, we evaluate the call
 
-               Next (E);
-            end loop;
-         end;
+         when N_Function_Call =>
+            Force_Evaluation (Nam);
 
-      --  For a slice, we evaluate the prefix, as for the indexed component
-      --  case and then, if there is a range present, either directly or as the
-      --  constraint of a discrete subtype indication, we evaluate the two
-      --  bounds of this range.
+         --  For a qualified expression, we evaluate the underlying object
+         --  name if any, otherwise we force the evaluation of the underlying
+         --  expression.
 
-      elsif K = N_Slice then
-         Evaluate_Name (Prefix (Nam));
-         Evaluate_Slice_Bounds (Nam);
+         when N_Qualified_Expression =>
+            if Is_Object_Reference (Expression (Nam)) then
+               Evaluate_Name (Expression (Nam));
+            else
+               Force_Evaluation (Expression (Nam));
+            end if;
 
-      --  For a type conversion, the expression of the conversion must be the
-      --  name of an object, and we simply need to evaluate this name.
+         --  For a selected component, we simply evaluate the prefix
 
-      elsif K = N_Type_Conversion then
-         Evaluate_Name (Expression (Nam));
+         when N_Selected_Component =>
+            Evaluate_Name (Prefix (Nam));
 
-      --  For a function call, we evaluate the call
+         --  For a slice, we evaluate the prefix, as for the indexed component
+         --  case and then, if there is a range present, either directly or as
+         --  the constraint of a discrete subtype indication, we evaluate the
+         --  two bounds of this range.
 
-      elsif K = N_Function_Call then
-         Force_Evaluation (Nam);
+         when N_Slice =>
+            Evaluate_Name (Prefix (Nam));
+            Evaluate_Slice_Bounds (Nam);
 
-      --  The remaining cases are direct name, operator symbol and character
-      --  literal. In all these cases, we do nothing, since we want to
-      --  reevaluate each time the renamed object is used.
+         --  For a type conversion, the expression of the conversion must be
+         --  the name of an object, and we simply need to evaluate this name.
 
-      else
-         return;
-      end if;
+         when N_Type_Conversion =>
+            Evaluate_Name (Expression (Nam));
+
+         --  The remaining cases are direct name, operator symbol and character
+         --  literal. In all these cases, we do nothing, since we want to
+         --  reevaluate each time the renamed object is used.
+
+         when others =>
+            null;
+      end case;
    end Evaluate_Name;
 
    ---------------------------
@@ -6933,7 +6946,7 @@ 
             --  existing actions of the expression with actions, and should
             --  never reach here: if actions are inserted on a statement
             --  within the Actions of an expression with actions, or on some
-            --  sub-expression of such a statement, then the outermost proper
+            --  subexpression of such a statement, then the outermost proper
             --  insertion point is right before the statement, and we should
             --  never climb up as far as the N_Expression_With_Actions itself.
 
Index: exp_util.ads
===================================================================
--- exp_util.ads	(revision 247293)
+++ exp_util.ads	(working copy)
@@ -518,8 +518,11 @@ 
 
    procedure Evaluate_Name (Nam : Node_Id);
    --  Remove all side effects from a name which appears as part of an object
-   --  renaming declaration. More comments are needed here that explain how
-   --  this differs from Force_Evaluation and Remove_Side_Effects ???
+   --  renaming declaration. Similarly to Force_Evaluation, it removes the
+   --  side effects and captures the values of the variables, except for the
+   --  variable being renamed. Hence this differs from Force_Evaluation and
+   --  Remove_Side_Effects (but it calls Force_Evaluation on subexpressions
+   --  whose value needs to be fixed).
 
    procedure Evolve_And_Then (Cond : in out Node_Id; Cond1 : Node_Id);
    --  Rewrites Cond with the expression: Cond and then Cond1. If Cond is