This patch adds a check to ensure that the actual parameter of a Ghost subprogram call whose formal is of mode IN OUT or OUT is Ghost.
------------ -- Source -- ------------ -- ghost_procs.ads package Ghost_Procs is procedure In_Proc (Formal : Integer) with Ghost; procedure In_Out_Proc (Formal : in out Integer) with Ghost; procedure Out_Proc (Formal : out Integer) with Ghost; end Ghost_Procs; -- ghost_procs.adb package body Ghost_Procs is procedure In_Proc (Formal : Integer) is begin null; In_Proc; procedure In_Out_Proc (Formal : in out Integer) is begin null; In_Out_Proc; procedure Out_Proc (Formal : out Integer) is begin null; Out_Proc; end Ghost_Procs; -- ghost_params.adb with Ghost_Procs; use Ghost_Procs; procedure Ghost_Params is -- 6.9(13) - An out or in out mode actual parameter in a call to a ghost -- subprogram shall be a ghost variable. Ghost_Obj : Integer := 1 with Ghost; Obj : Integer := 2; begin In_Proc (Ghost_Obj); -- OK In_Proc (Obj); -- OK In_Out_Proc (Ghost_Obj); -- OK In_Out_Proc (Obj); -- Error Out_Proc (Ghost_Obj); -- OK Out_Proc (Obj); -- Error end Ghost_Params; --------------------------- -- Compilaton and output -- --------------------------- $ gcc -c ghost_params.adb ghost_params.adb:15:17: non-ghost variable "Obj" cannot appear as actual in call to ghost procedure ghost_params.adb:15:17: corresponding formal has mode "in out" ghost_params.adb:17:14: non-ghost variable "Obj" cannot appear as actual in call to ghost procedure ghost_params.adb:17:14: corresponding formal has mode "out" Tested on x86_64-pc-linux-gnu, committed on trunk 2014-11-07 Hristian Kirtchev <kirtc...@adacore.com> * sem_ch3.adb (Analyze_Object_Declaration): Update references to SPARK RM. (Process_Full_View): Update references to SPARK RM. * sem_ch6.adb (Analyze_Generic_Subprogram_Body): Update references to SPARK RM. (Analyze_Subprogram_Body_Helper): Update references to SPARK RM. * sem_ch7.adb (Analyze_Package_Body_Helper): Update references to SPARK RM. * sem_prag.adb (Check_Ghost_Constituent): Update references to SPARK RM. * sem_res.adb (Check_Ghost_Policy): Update references to SPARK RM. (Resolve_Actuals): Ensure that the actual parameter of a Ghost subprogram whose formal is of mode IN OUT or OUT is Ghost. * sem_util.adb (Check_Ghost_Completion): Update references to SPARK RM.
Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 217225) +++ sem_ch3.adb (working copy) @@ -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); Index: sem_ch7.adb =================================================================== --- sem_ch7.adb (revision 217215) +++ sem_ch7.adb (working copy) @@ -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; Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 217226) +++ sem_prag.adb (working copy) @@ -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) Index: sem_util.adb =================================================================== --- sem_util.adb (revision 217224) +++ sem_util.adb (working copy) @@ -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 Index: sem_res.adb =================================================================== --- sem_res.adb (revision 217226) +++ sem_res.adb (working copy) @@ -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 Index: sem_ch6.adb =================================================================== --- sem_ch6.adb (revision 217226) +++ sem_ch6.adb (working copy) @@ -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;