@@ -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;
--------------