Commit 77562afd by Claire Dross Committed by Pierre-Marie de Rodat

[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
parent 402b9150
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> 2019-09-17 Ed Falis <falis@adacore.com>
* doc/gnat_rm/implementation_defined_pragmas.rst: Remove * doc/gnat_rm/implementation_defined_pragmas.rst: Remove
......
...@@ -708,8 +708,8 @@ package body Sem_SPARK is ...@@ -708,8 +708,8 @@ package body Sem_SPARK is
function Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id; function Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id;
pragma Precondition (Is_Path_Expression (Expr)); pragma Precondition (Is_Path_Expression (Expr));
-- Return the expression being borrowed/observed when borrowing or -- Return the expression being borrowed/observed when borrowing or
-- observing Expr. If Expr is a call to a traversal function, this is -- observing Expr. If Expr contains a call to traversal function, this is
-- the first actual, otherwise it is Expr. -- the first actual of the first such call, otherwise it is Expr.
function Get_Perm (N : Node_Or_Entity_Id) return Perm_Kind; function Get_Perm (N : Node_Or_Entity_Id) return Perm_Kind;
-- The function that takes a name as input and returns a permission -- The function that takes a name as input and returns a permission
...@@ -3772,12 +3772,61 @@ package body Sem_SPARK is ...@@ -3772,12 +3772,61 @@ package body Sem_SPARK is
----------------------------------- -----------------------------------
function Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id 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 begin
if Is_Traversal_Function_Call (Expr) then case Nkind (Expr) is
return First_Actual (Expr); when N_Expanded_Name
else | 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; return Expr;
end if;
when others =>
raise Program_Error;
end case;
end Find_Func_Call;
B_Expr : Node_Id := Expr;
begin
-- 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; end Get_Observed_Or_Borrowed_Expr;
-------------- --------------
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment