[Ada] Prevent inlining-for-proof for calls inside ELSIF condition
Commit Message
In GNATprove we don't want inlining-for-proof to expand subprogram
bodies into actions attached to nodes. These actions are attached either
to expressions or to statements.
For expressions, we prevented inlining by Is_Potentially_Unevaluated.
For statements, we prevented inlining by In_While_Loop_Condition, but
forgot about actions attached to ELSIF condition.
There are no other expression or statements nodes where actions could be
attached, so this fix is exhaustive.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* sem_util.ads (In_Statement_Condition_With_Actions): Renamed
from In_While_Loop_Condition; move to fit the alphabetic order.
* sem_util.adb (In_Statement_Condition_With_Actions): Detect
Elsif condition; stop search on other statements; prevent search
from going too far; move to fit the alphabetic order.
* sem_res.adb (Resolve_Call): Adapt caller.
@@ -7346,7 +7346,7 @@ package body Sem_Res is
-- loops, as this would create complex actions inside
-- the condition, that are not handled by GNATprove.
- elsif In_While_Loop_Condition (N) then
+ elsif In_Statement_Condition_With_Actions (N) then
Cannot_Inline
("cannot inline & (in while loop condition)?", N, Nam_UA);
@@ -14986,41 +14986,58 @@ package body Sem_Util is
return False;
end In_Return_Value;
- ---------------------
- -- In_Visible_Part --
- ---------------------
-
- function In_Visible_Part (Scope_Id : Entity_Id) return Boolean is
- begin
- return Is_Package_Or_Generic_Package (Scope_Id)
- and then In_Open_Scopes (Scope_Id)
- and then not In_Package_Body (Scope_Id)
- and then not In_Private_Part (Scope_Id);
- end In_Visible_Part;
-
- -----------------------------
- -- In_While_Loop_Condition --
- -----------------------------
+ -----------------------------------------
+ -- In_Statement_Condition_With_Actions --
+ -----------------------------------------
- function In_While_Loop_Condition (N : Node_Id) return Boolean is
+ function In_Statement_Condition_With_Actions (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
+ while Present (P) loop
+ if Nkind (P) = N_Iteration_Scheme
and then Prev = Condition (P)
then
return True;
- else
- Prev := P;
- P := Parent (P);
+
+ elsif Nkind (P) = N_Elsif_Part
+ and then Prev = Condition (P)
+ then
+ return True;
+
+ -- No point in going beyond statements
+
+ elsif Nkind (N) in N_Statement_Other_Than_Procedure_Call
+ | N_Procedure_Call_Statement
+ then
+ exit;
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (P) then
+ exit;
end if;
+
+ Prev := P;
+ P := Parent (P);
end loop;
- end In_While_Loop_Condition;
+
+ return False;
+ end In_Statement_Condition_With_Actions;
+
+ ---------------------
+ -- In_Visible_Part --
+ ---------------------
+
+ function In_Visible_Part (Scope_Id : Entity_Id) return Boolean is
+ begin
+ return Is_Package_Or_Generic_Package (Scope_Id)
+ and then In_Open_Scopes (Scope_Id)
+ and then not In_Package_Body (Scope_Id)
+ and then not In_Private_Part (Scope_Id);
+ end In_Visible_Part;
--------------------------------
-- Incomplete_Or_Partial_View --
@@ -1723,14 +1723,18 @@ package Sem_Util is
-- This version is more efficient than calling the single root version of
-- Is_Subtree twice.
+ function In_Statement_Condition_With_Actions (N : Node_Id) return Boolean;
+ -- Returns true if the expression N occurs within the condition of a
+ -- statement node with actions. Subsidiary to inlining for GNATprove, where
+ -- inlining of function calls in such expressions would expand the called
+ -- body into actions list of the condition node. GNATprove cannot yet cope
+ -- with such a complex AST.
+
function In_Visible_Part (Scope_Id : Entity_Id) return Boolean;
-- Determine whether a declaration occurs within the visible part of a
-- 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