GNATprove needs traversal subprograms that do not simply traverse
syntactic nodes like Atree.Traverse_Func and Atree.Traverse_Proc, but
also traverse semantic nodes which are logically children of the nodes.
Now available through Sem_Util.Traverse_More_Func and
Sem_Util.Traverse_More_Proc.
There is no impact on compilation.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-08-12 Yannick Moy <m...@adacore.com>
gcc/ada/
* sem_util.adb, sem_util.ads (Traverse_More_Func,
Traverse_More_Proc): New traversal subprograms.--- gcc/ada/sem_util.adb
+++ gcc/ada/sem_util.adb
@@ -26,7 +26,6 @@
with Treepr; -- ???For debugging code below
with Aspects; use Aspects;
-with Atree; use Atree;
with Casing; use Casing;
with Checks; use Checks;
with Debug; use Debug;
@@ -25437,6 +25436,205 @@ package body Sem_Util is
end if;
end Transfer_Entities;
+ ------------------------
+ -- Traverse_More_Func --
+ ------------------------
+
+ function Traverse_More_Func (Node : Node_Id) return Traverse_Final_Result is
+
+ Processing_Itype : Boolean := False;
+ -- Set to True while traversing the nodes under an Itype, to prevent
+ -- looping on Itype handling during that traversal.
+
+ function Process_More (N : Node_Id) return Traverse_Result;
+ -- Wrapper over the Process callback to handle parts of the AST that
+ -- are not normally traversed as syntactic children.
+
+ function Traverse_Rec (N : Node_Id) return Traverse_Final_Result;
+ -- Main recursive traversal implemented as an instantiation of
+ -- Traverse_Func over a modified Process callback.
+
+ ------------------
+ -- Process_More --
+ ------------------
+
+ function Process_More (N : Node_Id) return Traverse_Result is
+
+ procedure Traverse_More (N : Node_Id;
+ Res : in out Traverse_Result);
+ procedure Traverse_More (L : List_Id;
+ Res : in out Traverse_Result);
+ -- Traverse a node or list and update the traversal result to value
+ -- Abandon when needed.
+
+ -------------------
+ -- Traverse_More --
+ -------------------
+
+ procedure Traverse_More (N : Node_Id;
+ Res : in out Traverse_Result)
+ is
+ begin
+ -- Do not process any more nodes if Abandon was reached
+
+ if Res = Abandon then
+ return;
+ end if;
+
+ if Traverse_Rec (N) = Abandon then
+ Res := Abandon;
+ end if;
+ end Traverse_More;
+
+ procedure Traverse_More (L : List_Id;
+ Res : in out Traverse_Result)
+ is
+ N : Node_Id := First (L);
+
+ begin
+ -- Do not process any more nodes if Abandon was reached
+
+ if Res = Abandon then
+ return;
+ end if;
+
+ while Present (N) loop
+ Traverse_More (N, Res);
+ Next (N);
+ end loop;
+ end Traverse_More;
+
+ -- Local variables
+
+ Node : Node_Id;
+ Result : Traverse_Result;
+
+ -- Start of processing for Process_More
+
+ begin
+ -- Initial callback to Process. Return immediately on Skip/Abandon.
+ -- Otherwise update the value of Node for further processing of
+ -- non-syntactic children.
+
+ Result := Process (N);
+
+ case Result is
+ when OK => Node := N;
+ when OK_Orig => Node := Original_Node (N);
+ when Skip => return Skip;
+ when Abandon => return Abandon;
+ end case;
+
+ -- Process the relevant semantic children which are a logical part of
+ -- the AST under this node before returning for the processing of
+ -- syntactic children.
+
+ -- Start with all non-syntactic lists of action nodes
+
+ case Nkind (Node) is
+ when N_Component_Association =>
+ Traverse_More (Loop_Actions (Node), Result);
+
+ when N_Elsif_Part =>
+ Traverse_More (Condition_Actions (Node), Result);
+
+ when N_Short_Circuit =>
+ Traverse_More (Actions (Node), Result);
+
+ when N_Case_Expression_Alternative =>
+ Traverse_More (Actions (Node), Result);
+
+ when N_Iteration_Scheme =>
+ Traverse_More (Condition_Actions (Node), Result);
+
+ when N_If_Expression =>
+ Traverse_More (Then_Actions (Node), Result);
+ Traverse_More (Else_Actions (Node), Result);
+
+ -- Various nodes have a field Actions as a syntactic node,
+ -- so it will be traversed in the regular syntactic traversal.
+
+ when N_Compilation_Unit_Aux
+ | N_Compound_Statement
+ | N_Expression_With_Actions
+ | N_Freeze_Entity
+ =>
+ null;
+
+ when others =>
+ null;
+ end case;
+
+ -- Then process unattached nodes which come from Itypes. This only
+ -- concerns currently ranges of scalar (possibly as index) types.
+ -- This traversal is protected against looping with Processing_Itype.
+
+ if not Processing_Itype
+ and then Nkind (Node) in N_Has_Etype
+ and then Present (Etype (Node))
+ and then Is_Itype (Etype (Node))
+ then
+ declare
+ Typ : constant Entity_Id := Etype (Node);
+ begin
+ Processing_Itype := True;
+
+ case Ekind (Typ) is
+ when Scalar_Kind =>
+ Traverse_More (Scalar_Range (Typ), Result);
+
+ when Array_Kind =>
+ declare
+ Index : Node_Id := First_Index (Typ);
+ Rng : Node_Id;
+ begin
+ while Present (Index) loop
+ if Nkind (Index) in N_Has_Entity then
+ Rng := Scalar_Range (Entity (Index));
+ else
+ Rng := Index;
+ end if;
+
+ Traverse_More (Rng, Result);
+ Next_Index (Index);
+ end loop;
+ end;
+ when others =>
+ null;
+ end case;
+
+ Processing_Itype := False;
+ end;
+ end if;
+
+ return Result;
+ end Process_More;
+
+ -- Define Traverse_Rec as a renaming of the instantiation, as an
+ -- instantiation cannot complete a previous spec.
+
+ function Traverse_Recursive is new Traverse_Func (Process_More);
+ function Traverse_Rec (N : Node_Id) return Traverse_Final_Result
+ renames Traverse_Recursive;
+
+ -- Start of processing for Traverse_More_Func
+
+ begin
+ return Traverse_Rec (Node);
+ end Traverse_More_Func;
+
+ ------------------------
+ -- Traverse_More_Proc --
+ ------------------------
+
+ procedure Traverse_More_Proc (Node : Node_Id) is
+ function Traverse is new Traverse_More_Func (Process);
+ Discard : Traverse_Final_Result;
+ pragma Warnings (Off, Discard);
+ begin
+ Discard := Traverse (Node);
+ end Traverse_More_Proc;
+
-----------------------
-- Type_Access_Level --
-----------------------
--- gcc/ada/sem_util.ads
+++ gcc/ada/sem_util.ads
@@ -25,6 +25,7 @@
-- Package containing utility procedures used throughout the semantics
+with Atree; use Atree;
with Einfo; use Einfo;
with Exp_Tss; use Exp_Tss;
with Namet; use Namet;
@@ -2811,6 +2812,22 @@ package Sem_Util is
-- Move a list of entities from one scope to another, and recompute
-- Is_Public based upon the new scope.
+ generic
+ with function Process (N : Node_Id) return Traverse_Result is <>;
+ function Traverse_More_Func (Node : Node_Id) return Traverse_Final_Result;
+ -- This is a version of Atree.Traverse_Func that not only traverses
+ -- syntactic children of nodes, but also semantic children which are
+ -- logically children of the node. This concerns currently lists of
+ -- action nodes and ranges under Itypes, both inserted by the compiler.
+
+ generic
+ with function Process (N : Node_Id) return Traverse_Result is <>;
+ procedure Traverse_More_Proc (Node : Node_Id);
+ pragma Inline (Traverse_More_Proc);
+ -- This is the same as Traverse_More_Func except that no result is
+ -- returned, i.e. Traverse_More_Func is called and the result is simply
+ -- discarded.
+
function Type_Access_Level (Typ : Entity_Id) return Uint;
-- Return the accessibility level of Typ
