From: Claire Dross <dross@adacore.com>
Date: Tue, 17 Sep 2019 08:01:58 +0000 (+0000)
Subject: [Ada] Support chained calls to traversal functions in SPARK
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=77562afd5b514434c7f6cacaeb1eaaa234d19736;p=gcc.git

[Ada] Support chained calls to traversal functions in SPARK

This change only affects the SPARK toolset. In the part of semantic
analysis enforcing ownership rules for SPARK, it corrects a crash in
analysis of a declaration of a local borrower whose definition is a
chain of several calls to traversal functions.

2019-09-17  Claire Dross  <dross@adacore.com>

gcc/ada/

	* sem_spark.adb (Get_Observed_Or_Borrowed_Expr): If the
	definition of a local borrower contains calls to traversal
	functions, the borrowed expression is the first parameter of the
	first traversal function call in the definition.

From-SVN: r275785
---

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 7ccb70f8475..baf17ca0666 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,10 @@
+2019-09-17  Claire Dross  <dross@adacore.com>
+
+	* sem_spark.adb (Get_Observed_Or_Borrowed_Expr): If the
+	definition of a local borrower contains calls to traversal
+	functions, the borrowed expression is the first parameter of the
+	first traversal function call in the definition.
+
 2019-09-17  Ed Falis  <falis@adacore.com>
 
 	* doc/gnat_rm/implementation_defined_pragmas.rst: Remove
diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb
index 038c7cdd3e8..af53f69ba2c 100644
--- a/gcc/ada/sem_spark.adb
+++ b/gcc/ada/sem_spark.adb
@@ -708,8 +708,8 @@ package body Sem_SPARK is
    function Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id;
    pragma Precondition (Is_Path_Expression (Expr));
    --  Return the expression being borrowed/observed when borrowing or
-   --  observing Expr. If Expr is a call to a traversal function, this is
-   --  the first actual, otherwise it is Expr.
+   --  observing Expr. If Expr contains a call to traversal function, this is
+   --  the first actual of the first such call, otherwise it is Expr.
 
    function Get_Perm (N : Node_Or_Entity_Id) return Perm_Kind;
    --  The function that takes a name as input and returns a permission
@@ -3772,12 +3772,61 @@ package body Sem_SPARK is
    -----------------------------------
 
    function Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id is
+
+      function Find_Func_Call (Expr : Node_Id) return Node_Id;
+      --  Search for function calls in the prefixes of Expr
+
+      --------------------
+      -- Find_Func_Call --
+      --------------------
+
+      function Find_Func_Call (Expr : Node_Id) return Node_Id is
+      begin
+         case Nkind (Expr) is
+            when N_Expanded_Name
+               | N_Identifier
+            =>
+               return Empty;
+
+            when N_Explicit_Dereference
+               | N_Indexed_Component
+               | N_Selected_Component
+               | N_Slice
+            =>
+               return Find_Func_Call (Prefix (Expr));
+
+            when N_Qualified_Expression
+               | N_Type_Conversion
+               | N_Unchecked_Type_Conversion
+            =>
+               return Find_Func_Call (Expression (Expr));
+
+            when N_Function_Call =>
+               return Expr;
+
+            when others =>
+               raise Program_Error;
+         end case;
+      end Find_Func_Call;
+
+      B_Expr : Node_Id := Expr;
+
    begin
-      if Is_Traversal_Function_Call (Expr) then
-         return First_Actual (Expr);
-      else
-         return Expr;
-      end if;
+      --  Search for the first call to a traversal function in Expr. If there
+      --  is one, its first parameter is the borrowed expression. Otherwise,
+      --  it is Expr.
+
+      loop
+         declare
+            Call : constant Node_Id := Find_Func_Call (B_Expr);
+         begin
+            exit when No (Call);
+            pragma Assert (Is_Traversal_Function_Call (Call));
+            B_Expr := First_Actual (Call);
+         end;
+      end loop;
+
+      return B_Expr;
    end Get_Observed_Or_Borrowed_Expr;
 
    --------------