===================================================================
@@ -3925,7 +3925,7 @@
-- The Ghost policy in effect at the point of declaration
-- and at the point of completion must match
- -- (SPARK RM 6.9(14)).
+ -- (SPARK RM 6.9(15)).
if Present (Prev_Entity)
and then Is_Ghost_Entity (Prev_Entity)
@@ -4112,7 +4112,7 @@
Set_Is_Ghost_Entity (Id);
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(14)).
+ -- point of completion must match (SPARK RM 6.9(16)).
if Present (Prev_Entity) and then Is_Ghost_Entity (Prev_Entity) then
Check_Ghost_Completion (Prev_Entity, Id);
@@ -19786,7 +19786,7 @@
Set_Is_Ghost_Entity (Full_T);
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(14)).
+ -- point of completion must match (SPARK RM 6.9(15)).
Check_Ghost_Completion (Priv_T, Full_T);
===================================================================
@@ -735,7 +735,7 @@
Set_Is_Ghost_Entity (Body_Id);
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(14)).
+ -- point of completion must match (SPARK RM 6.9(15)).
Check_Ghost_Completion (Spec_Id, Body_Id);
end if;
===================================================================
@@ -23473,7 +23473,7 @@
-- The Ghost policy in effect at the point of abstract
-- state declaration and constituent must match
- -- (SPARK RM 6.9(15)).
+ -- (SPARK RM 6.9(16)).
if Is_Checked_Ghost_Entity (State_Id)
and then Is_Ignored_Ghost_Entity (Constit_Id)
===================================================================
@@ -2681,7 +2681,7 @@
begin
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(14)).
+ -- point of completion must match (SPARK RM 6.9(15)).
if Is_Checked_Ghost_Entity (Partial_View)
and then Policy = Name_Ignore
===================================================================
@@ -841,7 +841,7 @@
begin
-- The Ghost policy in effect a the point of declaration and at the
- -- point of use must match (SPARK RM 6.9(13)).
+ -- point of use must match (SPARK RM 6.9(14)).
if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then
Error_Msg_Sloc := Sloc (Err_N);
@@ -4625,6 +4625,26 @@
("\subprogram & has Extensions_Visible True", A, Nam);
end if;
+ -- The actual parameter of a Ghost subprogram whose formal is of
+ -- mode IN OUT or OUT must be a Ghost variable (SPARK RM 6.9(13)).
+
+ if Is_Ghost_Entity (Nam)
+ and then Ekind_In (F, E_In_Out_Parameter, E_Out_Parameter)
+ and then Is_Entity_Name (A)
+ and then Present (Entity (A))
+ and then not Is_Ghost_Entity (Entity (A))
+ then
+ Error_Msg_NE
+ ("non-ghost variable & cannot appear as actual in call to "
+ & "ghost procedure", A, Entity (A));
+
+ if Ekind (F) = E_In_Out_Parameter then
+ Error_Msg_N ("\corresponding formal has mode `IN OUT`", A);
+ else
+ Error_Msg_N ("\corresponding formal has mode OUT", A);
+ end if;
+ end if;
+
Next_Actual (A);
-- Case where actual is not present
===================================================================
@@ -1220,7 +1220,7 @@
Set_Is_Ghost_Entity (Body_Id);
-- The Ghost policy in effect at the point of declaration and at
- -- the point of completion must match (SPARK RM 6.9(14)).
+ -- the point of completion must match (SPARK RM 6.9(15)).
Check_Ghost_Completion (Gen_Id, Body_Id);
end if;
@@ -3343,7 +3343,7 @@
Set_Is_Ghost_Entity (Body_Id);
-- The Ghost policy in effect at the point of declaration and
- -- at the point of completion must match (SPARK RM 6.9(14)).
+ -- at the point of completion must match (SPARK RM 6.9(15)).
Check_Ghost_Completion (Spec_Id, Body_Id);
end if;