[Ada] Prevent inlining inside condition of while loop in GNATprove

2019-12-13  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_res.adb (Resolve_Call): Prevent inlining inside while loop
	conditions.
	* sem_util.adb, sem_util.ads (In_While_Loop_Condition): New
	query function.

From-SVN: r279347

gcc/ada/ChangeLog

+2019-12-13  Yannick Moy  <moy@adacore.com>
+
+	* sem_res.adb (Resolve_Call): Prevent inlining inside while loop
+	conditions.
+	* sem_util.adb, sem_util.ads (In_While_Loop_Condition): New
+	query function.
+
 2019-12-13  Bob Duff  <duff@adacore.com>
 
 	* impunit.ads: Add Ada_202X_Unit.

gcc/ada/sem_res.adb

@@ -7172,6 +7172,14 @@ package body Sem_Res is
                     ("cannot inline & (in potentially unevaluated context)?",
                      N, Nam_UA);
 
+               --  Calls cannot be inlined inside the conditions of while
+               --  loops, as this would create complex actions inside
+               --  the condition, that are not handled by GNATprove.
+
+               elsif In_While_Loop_Condition (N) then
+                  Cannot_Inline
+                    ("cannot inline & (in while loop condition)?", N, Nam_UA);
+
                --  Do not inline calls which would possibly lead to missing a
                --  type conversion check on an input parameter.
 

gcc/ada/sem_util.adb

@@ -12855,6 +12855,30 @@ package body Sem_Util is
         and then not In_Private_Part (Scope_Id);
    end In_Visible_Part;
 
+   -----------------------------
+   -- In_While_Loop_Condition --
+   -----------------------------
+
+   function In_While_Loop_Condition (N : Node_Id) return Boolean is
+      Prev : Node_Id := N;
+      P    : Node_Id := Parent (N);
+      --  P and Prev will be used for traversing the AST, while maintaining an
+      --  invariant that P = Parent (Prev).
+   begin
+      loop
+         if No (P) then
+            return False;
+         elsif Nkind (P) = N_Iteration_Scheme
+           and then Prev = Condition (P)
+         then
+            return True;
+         else
+            Prev := P;
+            P := Parent (P);
+         end if;
+      end loop;
+   end In_While_Loop_Condition;
+
    --------------------------------
    -- Incomplete_Or_Partial_View --
    --------------------------------

gcc/ada/sem_util.ads

@@ -1446,6 +1446,9 @@ package Sem_Util is
    --  package specification. The package must be on the scope stack, and the
    --  corresponding private part must not.
 
+   function In_While_Loop_Condition (N : Node_Id) return Boolean;
+   --  Returns true if the expression N occurs within the condition of a while
+
    function Incomplete_Or_Partial_View (Id : Entity_Id) return Entity_Id;
    --  Given the entity of a constant or a type, retrieve the incomplete or
    --  partial view of the same entity. Note that Id may not have a partial