A traversal function, especially when implemented as an expression
function, may need to return an if-expression or case-expression, while
still respecting Legality Rule SPARK RM 3.10(5). This case is now
allowed in GNATprove.
There is no impact on compilation.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-07-22 Yannick Moy <m...@adacore.com>
gcc/ada/
* sem_spark.adb (Get_Root_Object, Is_Path_Expression,
Is_Subpath_Expression): Add parameter Is_Traversal to adapt
these functions to the case of paths returned from a traversal
function.
(Read_Indexes): Handle the case of an if-expression or
case-expression.
(Check_Statement): Check Emit_Messages only when issuing an
error message. This is important as Emit_Messages may store the
information that an error was detected.--- gcc/ada/sem_spark.adb
+++ gcc/ada/sem_spark.adb
@@ -715,10 +715,14 @@ package body Sem_SPARK is
function Get_Root_Object
(Expr : Node_Id;
- Through_Traversal : Boolean := True) return Entity_Id;
+ Through_Traversal : Boolean := True;
+ Is_Traversal : Boolean := False) return Entity_Id;
-- Return the root of the path expression Expr, or Empty for an allocator,
-- NULL, or a function call. Through_Traversal is True if it should follow
- -- through calls to traversal functions.
+ -- through calls to traversal functions. Is_Traversal is True if this
+ -- corresponds to a value returned from a traversal function, which should
+ -- allow if-expressions and case-expressions that refer to the same root,
+ -- even if the paths are not the same in all branches.
generic
with procedure Handle_Parameter_Or_Global
@@ -745,11 +749,19 @@ package body Sem_SPARK is
-- A procedure that is called when deep globals or aliased globals are used
-- without any global aspect.
- function Is_Path_Expression (Expr : Node_Id) return Boolean;
- -- Return whether Expr corresponds to a path
+ function Is_Path_Expression
+ (Expr : Node_Id;
+ Is_Traversal : Boolean := False) return Boolean;
+ -- Return whether Expr corresponds to a path. Is_Traversal is True if this
+ -- corresponds to a value returned from a traversal function, which should
+ -- allow if-expressions and case-expressions.
- function Is_Subpath_Expression (Expr : Node_Id) return Boolean;
- -- Return True if Expr can be part of a path expression
+ function Is_Subpath_Expression
+ (Expr : Node_Id;
+ Is_Traversal : Boolean := False) return Boolean;
+ -- Return True if Expr can be part of a path expression. Is_Traversal is
+ -- True if this corresponds to a value returned from a traversal function,
+ -- which should allow if-expressions and case-expressions.
function Is_Prefix_Or_Almost (Pref, Expr : Node_Id) return Boolean;
-- Determine if the candidate Prefix is indeed a prefix of Expr, or almost
@@ -1749,6 +1761,31 @@ package body Sem_SPARK is
end loop;
end;
+ when N_If_Expression =>
+ declare
+ Cond : constant Node_Id := First (Expressions (Expr));
+ Then_Part : constant Node_Id := Next (Cond);
+ Else_Part : constant Node_Id := Next (Then_Part);
+ begin
+ Read_Expression (Cond);
+ Read_Indexes (Then_Part);
+ Read_Indexes (Else_Part);
+ end;
+
+ when N_Case_Expression =>
+ declare
+ Cases : constant List_Id := Alternatives (Expr);
+ Cur_Case : Node_Id := First (Cases);
+
+ begin
+ Read_Expression (Expression (Expr));
+
+ while Present (Cur_Case) loop
+ Read_Indexes (Expression (Cur_Case));
+ Next (Cur_Case);
+ end loop;
+ end;
+
when N_Attribute_Reference =>
pragma Assert
(Get_Attribute_Id (Attribute_Name (Expr)) =
@@ -3115,14 +3152,14 @@ package body Sem_SPARK is
if Is_Anonymous_Access_Type (Return_Typ) then
pragma Assert (Is_Traversal_Function (Subp));
- if Nkind (Expr) /= N_Null and then Emit_Messages then
+ if Nkind (Expr) /= N_Null then
declare
Expr_Root : constant Entity_Id :=
- Get_Root_Object (Expr);
+ Get_Root_Object (Expr, Is_Traversal => True);
Param : constant Entity_Id :=
First_Formal (Subp);
begin
- if Param /= Expr_Root then
+ if Param /= Expr_Root and then Emit_Messages then
Error_Msg_NE
("returned value must be rooted in "
& "traversed parameter & "
@@ -3642,10 +3679,31 @@ package body Sem_SPARK is
function Get_Root_Object
(Expr : Node_Id;
- Through_Traversal : Boolean := True) return Entity_Id
+ Through_Traversal : Boolean := True;
+ Is_Traversal : Boolean := False) return Entity_Id
is
+ function GRO (Expr : Node_Id) return Entity_Id;
+ -- Local wrapper on the actual function, to propagate the values of
+ -- optional parameters.
+
+ ---------
+ -- GRO --
+ ---------
+
+ function GRO (Expr : Node_Id) return Entity_Id is
+ begin
+ return Get_Root_Object (Expr, Through_Traversal, Is_Traversal);
+ end GRO;
+
+ Get_Root_Object : Boolean;
+ pragma Unmodified (Get_Root_Object);
+ -- Local variable to mask the name of function Get_Root_Object, to
+ -- prevent direct call. Instead GRO wrapper should be called.
+
+ -- Start of processing for Get_Root_Object
+
begin
- if not Is_Subpath_Expression (Expr) then
+ if not Is_Subpath_Expression (Expr, Is_Traversal) then
if Emit_Messages then
Error_Msg_N ("name expected here for path", Expr);
end if;
@@ -3663,7 +3721,7 @@ package body Sem_SPARK is
| N_Selected_Component
| N_Slice
=>
- return Get_Root_Object (Prefix (Expr), Through_Traversal);
+ return GRO (Prefix (Expr));
-- There is no root object for an (extension) aggregate, allocator,
-- concat, or NULL.
@@ -3684,7 +3742,7 @@ package body Sem_SPARK is
if Through_Traversal
and then Is_Traversal_Function_Call (Expr)
then
- return Get_Root_Object (First_Actual (Expr), Through_Traversal);
+ return GRO (First_Actual (Expr));
else
return Empty;
end if;
@@ -3693,7 +3751,7 @@ package body Sem_SPARK is
| N_Type_Conversion
| N_Unchecked_Type_Conversion
=>
- return Get_Root_Object (Expression (Expr), Through_Traversal);
+ return GRO (Expression (Expr));
when N_Attribute_Reference =>
pragma Assert
@@ -3706,6 +3764,69 @@ package body Sem_SPARK is
Attribute_Image);
return Empty;
+ when N_If_Expression =>
+ if Is_Traversal then
+ declare
+ Cond : constant Node_Id := First (Expressions (Expr));
+ Then_Part : constant Node_Id := Next (Cond);
+ Else_Part : constant Node_Id := Next (Then_Part);
+ Then_Root : constant Entity_Id := GRO (Then_Part);
+ Else_Root : constant Entity_Id := GRO (Else_Part);
+ begin
+ if Nkind (Then_Part) = N_Null then
+ return Else_Root;
+ elsif Nkind (Else_Part) = N_Null then
+ return Then_Part;
+ elsif Then_Root = Else_Root then
+ return Then_Root;
+ else
+ if Emit_Messages then
+ Error_Msg_N
+ ("same name expected here in each branch", Expr);
+ end if;
+ return Empty;
+ end if;
+ end;
+ else
+ if Emit_Messages then
+ Error_Msg_N ("name expected here for path", Expr);
+ end if;
+ return Empty;
+ end if;
+
+ when N_Case_Expression =>
+ if Is_Traversal then
+ declare
+ Cases : constant List_Id := Alternatives (Expr);
+ Cur_Case : Node_Id := First (Cases);
+ Cur_Root : Entity_Id;
+ Common_Root : Entity_Id := Empty;
+
+ begin
+ while Present (Cur_Case) loop
+ Cur_Root := GRO (Expression (Cur_Case));
+
+ if Common_Root = Empty then
+ Common_Root := Cur_Root;
+ elsif Common_Root /= Cur_Root then
+ if Emit_Messages then
+ Error_Msg_N
+ ("same name expected here in each branch", Expr);
+ end if;
+ return Empty;
+ end if;
+ Next (Cur_Case);
+ end loop;
+
+ return Common_Root;
+ end;
+ else
+ if Emit_Messages then
+ Error_Msg_N ("name expected here for path", Expr);
+ end if;
+ return Empty;
+ end if;
+
when others =>
raise Program_Error;
end case;
@@ -3876,7 +3997,30 @@ package body Sem_SPARK is
-- Is_Path_Expression --
------------------------
- function Is_Path_Expression (Expr : Node_Id) return Boolean is
+ function Is_Path_Expression
+ (Expr : Node_Id;
+ Is_Traversal : Boolean := False) return Boolean
+ is
+ function IPE (Expr : Node_Id) return Boolean;
+ -- Local wrapper on the actual function, to propagate the values of
+ -- optional parameter Is_Traversal.
+
+ ---------
+ -- IPE --
+ ---------
+
+ function IPE (Expr : Node_Id) return Boolean is
+ begin
+ return Is_Path_Expression (Expr, Is_Traversal);
+ end IPE;
+
+ Is_Path_Expression : Boolean;
+ pragma Unmodified (Is_Path_Expression);
+ -- Local variable to mask the name of function Is_Path_Expression, to
+ -- prevent direct call. Instead IPE wrapper should be called.
+
+ -- Start of processing for Is_Path_Expression
+
begin
case Nkind (Expr) is
when N_Expanded_Name
@@ -3907,7 +4051,47 @@ package body Sem_SPARK is
| N_Type_Conversion
| N_Unchecked_Type_Conversion
=>
- return Is_Path_Expression (Expression (Expr));
+ return IPE (Expression (Expr));
+
+ -- When returning from a traversal function, consider an
+ -- if-expression as a possible path expression.
+
+ when N_If_Expression =>
+ if Is_Traversal then
+ declare
+ Cond : constant Node_Id := First (Expressions (Expr));
+ Then_Part : constant Node_Id := Next (Cond);
+ Else_Part : constant Node_Id := Next (Then_Part);
+ begin
+ return IPE (Then_Part)
+ and then IPE (Else_Part);
+ end;
+ else
+ return False;
+ end if;
+
+ -- When returning from a traversal function, consider
+ -- a case-expression as a possible path expression.
+
+ when N_Case_Expression =>
+ if Is_Traversal then
+ declare
+ Cases : constant List_Id := Alternatives (Expr);
+ Cur_Case : Node_Id := First (Cases);
+
+ begin
+ while Present (Cur_Case) loop
+ if not IPE (Expression (Cur_Case)) then
+ return False;
+ end if;
+ Next (Cur_Case);
+ end loop;
+
+ return True;
+ end;
+ else
+ return False;
+ end if;
when others =>
return False;
@@ -4033,9 +4217,12 @@ package body Sem_SPARK is
-- Is_Subpath_Expression --
---------------------------
- function Is_Subpath_Expression (Expr : Node_Id) return Boolean is
+ function Is_Subpath_Expression
+ (Expr : Node_Id;
+ Is_Traversal : Boolean := False) return Boolean
+ is
begin
- return Is_Path_Expression (Expr)
+ return Is_Path_Expression (Expr, Is_Traversal)
or else (Nkind (Expr) = N_Attribute_Reference
and then
(Get_Attribute_Id (Attribute_Name (Expr)) =
