[Ada] Use of Ghost actuals in Ghost subprogram calls
Arnaud Charlet
charlet@adacore.com
Fri Nov 7 14:00:00 GMT 2014
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 <kirtchev@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.
-------------- next part --------------
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;
More information about the Gcc-patches
mailing list