[Ada] Update references to the SPARK RM
2019-08-21 Yannick Moy <moy@adacore.com> gcc/ada/ * sem_spark.adb: Update references to the SPARK RM. From-SVN: r274787
This commit is contained in:
parent
3c488e6c86
commit
e9934e8c79
|
@ -1,3 +1,7 @@
|
||||||
|
2019-08-21 Yannick Moy <moy@adacore.com>
|
||||||
|
|
||||||
|
* sem_spark.adb: Update references to the SPARK RM.
|
||||||
|
|
||||||
2019-08-21 Eric Botcazou <ebotcazou@adacore.com>
|
2019-08-21 Eric Botcazou <ebotcazou@adacore.com>
|
||||||
|
|
||||||
* repinfo.adb (List_Array_Info): In -gnatR4 mode, set the
|
* repinfo.adb (List_Array_Info): In -gnatR4 mode, set the
|
||||||
|
|
|
@ -672,7 +672,7 @@ package body Sem_SPARK is
|
||||||
-- Main traversal procedure to check safe pointer usage
|
-- Main traversal procedure to check safe pointer usage
|
||||||
|
|
||||||
procedure Check_Old_Loop_Entry (N : Node_Id);
|
procedure Check_Old_Loop_Entry (N : Node_Id);
|
||||||
-- Check SPARK RM 3.10(14) regarding 'Old and 'Loop_Entry
|
-- Check SPARK RM 3.10(13) regarding 'Old and 'Loop_Entry
|
||||||
|
|
||||||
procedure Check_Package_Body (Pack : Node_Id);
|
procedure Check_Package_Body (Pack : Node_Id);
|
||||||
|
|
||||||
|
@ -1085,7 +1085,7 @@ package body Sem_SPARK is
|
||||||
Borrowed : constant Node_Id := Get_Observed_Or_Borrowed_Expr (Expr);
|
Borrowed : constant Node_Id := Get_Observed_Or_Borrowed_Expr (Expr);
|
||||||
|
|
||||||
begin
|
begin
|
||||||
-- SPARK RM 3.10(8): If the type of the target is an anonymous
|
-- SPARK RM 3.10(7): If the type of the target is an anonymous
|
||||||
-- access-to-variable type (an owning access type), the source shall
|
-- access-to-variable type (an owning access type), the source shall
|
||||||
-- be an owning access object [..] whose root object is the target
|
-- be an owning access object [..] whose root object is the target
|
||||||
-- object itself.
|
-- object itself.
|
||||||
|
@ -1100,7 +1100,7 @@ package body Sem_SPARK is
|
||||||
if Emit_Messages then
|
if Emit_Messages then
|
||||||
Error_Msg_NE
|
Error_Msg_NE
|
||||||
("source of assignment must have & as root" &
|
("source of assignment must have & as root" &
|
||||||
" (SPARK RM 3.10(8)))",
|
" (SPARK RM 3.10(7)))",
|
||||||
Expr, Var);
|
Expr, Var);
|
||||||
end if;
|
end if;
|
||||||
return;
|
return;
|
||||||
|
@ -1132,7 +1132,7 @@ package body Sem_SPARK is
|
||||||
if Emit_Messages then
|
if Emit_Messages then
|
||||||
Error_Msg_NE
|
Error_Msg_NE
|
||||||
("source of assignment must have & as root" &
|
("source of assignment must have & as root" &
|
||||||
" (SPARK RM 3.10(8)))",
|
" (SPARK RM 3.10(7)))",
|
||||||
Expr, Var);
|
Expr, Var);
|
||||||
end if;
|
end if;
|
||||||
return;
|
return;
|
||||||
|
@ -2855,7 +2855,7 @@ package body Sem_SPARK is
|
||||||
Error_Msg_Name_1 := Aname;
|
Error_Msg_Name_1 := Aname;
|
||||||
Error_Msg_N
|
Error_Msg_N
|
||||||
("prefix of % attribute must be a function call "
|
("prefix of % attribute must be a function call "
|
||||||
& "(SPARK RM 3.10(14))", Pref);
|
& "(SPARK RM 3.10(13))", Pref);
|
||||||
end if;
|
end if;
|
||||||
|
|
||||||
elsif Is_Traversal_Function_Call (Pref) then
|
elsif Is_Traversal_Function_Call (Pref) then
|
||||||
|
@ -2863,7 +2863,7 @@ package body Sem_SPARK is
|
||||||
Error_Msg_Name_1 := Aname;
|
Error_Msg_Name_1 := Aname;
|
||||||
Error_Msg_N
|
Error_Msg_N
|
||||||
("prefix of % attribute should not call a traversal "
|
("prefix of % attribute should not call a traversal "
|
||||||
& "function (SPARK RM 3.10(14))", Pref);
|
& "function (SPARK RM 3.10(13))", Pref);
|
||||||
end if;
|
end if;
|
||||||
end if;
|
end if;
|
||||||
end if;
|
end if;
|
||||||
|
|
Loading…
Reference in New Issue