The special inlining performed in GNATprove should not allow inlining
inside the condition of while loops, as this creates complex actions
inside the condition itself, which are not handled by GNATprove.
Other loops are not impacted, as the bounds are only computed once,
which allows to move the actions before the loop instead of storing them
as actions inside an expression.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-12-13 Yannick Moy <m...@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.--- gcc/ada/sem_res.adb
+++ 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
+++ 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
+++ 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
