This patch implements several checks on use clauses to prevent mixing Ghost and
non-Ghost names. A context clause is marked as ignored Ghost when it mentions
an ignored Ghost package or type. Pruning of ignored Ghost code now looks at
compilation unit nodes in order to remove ignored Ghost clauses and pragmas.
------------
-- Source --
------------
-- g1.ads
package G1 with Ghost is
end G1;
-- g2.ads
package G2 with Ghost is
end G2;
-- l1.ads
package L1 is
end L1;
-- l2.ads
package L2 is
end L2;
-- types.ads
package Types is
type G1 is null record with Ghost;
type G2 is null record with Ghost;
type L1 is null record;
type L2 is null record;
end Types;
-- uses1.ads
with G1, G2;
use G1, G2; -- OK
with Types;
package Uses1 is
use type Types.G1, Types.G2; -- OK
end Uses1;
-- uses2.ads
with G1, L1;
use G1, L1; -- ERROR
with Types;
package Uses2 is
use type Types.G1, Types.L1; -- ERROR
end Uses2;
-- uses3.ads
with L1, L2, G2;
use L1, L2, G2; -- ERROR
with Types;
package Uses3 is
use type Types.L1, Types.L2, Types.G2; -- ERROR
end Uses3;
-- uses4.ads
with G1; use G1;
with G2; use G2;
with Types;
package Uses4 is
use type Types.G1, Types.G2;
end Uses4;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c uses1.ads
$ gcc -c uses2.ads
$ gcc -c uses3.ads
$ gcc -c uses4.ads -gnatDG
$ grep -c "g[12]" uses4.ads.dg
uses2.ads:2:01: use clause cannot mention ghost and non-ghost ghost units
uses2.ads:2:01: "G1" at g1.ads:1 declared as ghost
uses2.ads:2:01: "L1" at l1.ads:1 declared as non-ghost
uses2.ads:7:04: use clause cannot mention ghost and non-ghost ghost types
uses2.ads:7:04: "G1" at types.ads:2 declared as ghost
uses2.ads:7:04: "L1" at types.ads:5 declared as non-ghost
uses3.ads:2:01: use clause cannot mention ghost and non-ghost ghost units
uses3.ads:2:01: "G2" at g2.ads:1 declared as ghost
uses3.ads:2:01: "L1" at l1.ads:1 declared as non-ghost
uses3.ads:7:04: use clause cannot mention ghost and non-ghost ghost types
uses3.ads:7:04: "G2" at types.ads:3 declared as ghost
uses3.ads:7:04: "L1" at types.ads:5 declared as non-ghost
0
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-01-20 Hristian Kirtchev <kirtc...@adacore.com>
* ghost.adb (Mark_Ghost_Clause): New routine.
(Prune_Node): Do not prune compilation unit nodes.
(Remove_Ignored_Ghost_Code): Prune the compilation unit node directly.
This does not touch the node itself, but does prune all its fields.
* ghost.ads (Mark_Ghost_Clause): New routine.
* sem_ch8.adb (Analyze_Use_Package): Emit an error when a use
package clause mentions Ghost and non-Ghost packages. Mark a
use package clause as Ghost when it mentions a Ghost package.
(Analyze_Use_Type): Emit an error when a use type clause mentions
Ghost and non-Ghost types. Mark a use type clause as Ghost when
it mentions a Ghost type.
* sem_ch10.adb (Analyze_With_Clause): Mark a with clause as
Ghost when it withs a Ghost unit.
Index: sem_ch10.adb
===================================================================
--- sem_ch10.adb (revision 244703)
+++ sem_ch10.adb (working copy)
@@ -34,6 +34,7 @@
with Fname; use Fname;
with Fname.UF; use Fname.UF;
with Freeze; use Freeze;
+with Ghost; use Ghost;
with Impunit; use Impunit;
with Inline; use Inline;
with Lib; use Lib;
@@ -2826,6 +2827,8 @@
Set_Fatal_Error (Current_Sem_Unit, Error_Ignored);
end if;
end case;
+
+ Mark_Ghost_Clause (N);
end Analyze_With_Clause;
------------------------------
Index: ghost.adb
===================================================================
--- ghost.adb (revision 244691)
+++ ghost.adb (working copy)
@@ -1430,6 +1430,34 @@
end Mark_Ghost_Declaration_Or_Body;
-----------------------
+ -- Mark_Ghost_Clause --
+ -----------------------
+
+ procedure Mark_Ghost_Clause (N : Node_Id) is
+ Nam : Node_Id := Empty;
+
+ begin
+ if Nkind (N) = N_Use_Package_Clause then
+ Nam := First (Names (N));
+
+ elsif Nkind (N) = N_Use_Type_Clause then
+ Nam := First (Subtype_Marks (N));
+
+ elsif Nkind (N) = N_With_Clause then
+ Nam := Name (N);
+ end if;
+
+ if Present (Nam)
+ and then Is_Entity_Name (Nam)
+ and then Present (Entity (Nam))
+ and then Is_Ignored_Ghost_Entity (Entity (Nam))
+ then
+ Set_Is_Ignored_Ghost_Node (N);
+ Propagate_Ignored_Ghost_Code (N);
+ end if;
+ end Mark_Ghost_Clause;
+
+ -----------------------
-- Mark_Ghost_Pragma --
-----------------------
@@ -1574,10 +1602,17 @@
Id : Entity_Id;
begin
+ -- Do not prune compilation unit nodes because many mechanisms
+ -- depend on their presence. Note that context items must still
+ -- be processed.
+
+ if Nkind (N) = N_Compilation_Unit then
+ return OK;
+
-- The node is either declared as ignored Ghost or is a byproduct
-- of expansion. Destroy it and stop the traversal on this branch.
- if Is_Ignored_Ghost_Node (N) then
+ elsif Is_Ignored_Ghost_Node (N) then
Prune (N);
return Skip;
@@ -1628,7 +1663,7 @@
begin
for Index in Ignored_Ghost_Units.First .. Ignored_Ghost_Units.Last loop
- Prune_Tree (Unit (Ignored_Ghost_Units.Table (Index)));
+ Prune_Tree (Ignored_Ghost_Units.Table (Index));
end loop;
end Remove_Ignored_Ghost_Code;
Index: ghost.ads
===================================================================
--- ghost.ads (revision 244691)
+++ ghost.ads (working copy)
@@ -183,6 +183,11 @@
-- prior to processing the procedure call. This routine starts a Ghost
-- region and must be used in conjunction with Restore_Ghost_Mode.
+ procedure Mark_Ghost_Clause (N : Node_Id);
+ -- Mark use package, use type, or with clause N as Ghost when:
+ --
+ -- * The clause mentions a Ghost entity
+
procedure Mark_Ghost_Pragma
(N : Node_Id;
Id : Entity_Id);
Index: sem_ch8.adb
===================================================================
--- sem_ch8.adb (revision 244691)
+++ sem_ch8.adb (working copy)
@@ -3616,11 +3616,11 @@
-- within the package itself, ignore it.
procedure Analyze_Use_Package (N : Node_Id) is
+ Ghost_Id : Entity_Id := Empty;
+ Living_Id : Entity_Id := Empty;
+ Pack : Entity_Id;
Pack_Name : Node_Id;
- Pack : Entity_Id;
- -- Start of processing for Analyze_Use_Package
-
begin
Check_SPARK_05_Restriction ("use clause is not allowed", N);
@@ -3664,8 +3664,8 @@
if Entity (Pref) = Standard_Standard then
Error_Msg_N
- ("predefined package Standard cannot appear"
- & " in a context clause", Pref);
+ ("predefined package Standard cannot appear in a context "
+ & "clause", Pref);
end if;
end;
end if;
@@ -3673,8 +3673,8 @@
Next (Pack_Name);
end loop;
- -- Loop through package names to mark all entities as potentially
- -- use visible.
+ -- Loop through package names to mark all entities as potentially use
+ -- visible.
Pack_Name := First (Names (N));
while Present (Pack_Name) loop
@@ -3710,6 +3710,21 @@
if Applicable_Use (Pack_Name) then
Use_One_Package (Pack, N);
end if;
+
+ -- Capture the first Ghost package and the first living package
+
+ if Is_Entity_Name (Pack_Name) then
+ Pack := Entity (Pack_Name);
+
+ if Is_Ghost_Entity (Pack) then
+ if No (Ghost_Id) then
+ Ghost_Id := Pack;
+ end if;
+
+ elsif No (Living_Id) then
+ Living_Id := Pack;
+ end if;
+ end if;
end if;
-- Report error because name denotes something other than a package
@@ -3720,6 +3735,25 @@
Next (Pack_Name);
end loop;
+
+ -- Detect a mixture of Ghost packages and living packages within the
+ -- same use package clause. Ideally one would split a use package clause
+ -- with multiple names into multiple use package clauses with a single
+ -- name, however clients of the front end would have to adapt to this
+ -- change.
+
+ if Present (Ghost_Id) and then Present (Living_Id) then
+ Error_Msg_N
+ ("use clause cannot mention ghost and non-ghost ghost units", N);
+
+ Error_Msg_Sloc := Sloc (Ghost_Id);
+ Error_Msg_NE ("\& # declared as ghost", N, Ghost_Id);
+
+ Error_Msg_Sloc := Sloc (Living_Id);
+ Error_Msg_NE ("\& # declared as non-ghost", N, Living_Id);
+ end if;
+
+ Mark_Ghost_Clause (N);
end Analyze_Use_Package;
----------------------
@@ -3727,8 +3761,10 @@
----------------------
procedure Analyze_Use_Type (N : Node_Id) is
- E : Entity_Id;
- Id : Node_Id;
+ E : Entity_Id;
+ Ghost_Id : Entity_Id := Empty;
+ Id : Node_Id;
+ Living_Id : Entity_Id := Empty;
begin
Set_Hidden_By_Use_Clause (N, No_Elist);
@@ -3834,8 +3870,37 @@
end if;
end if;
+ -- Capture the first Ghost type and the first living type
+
+ if Is_Ghost_Entity (E) then
+ if No (Ghost_Id) then
+ Ghost_Id := E;
+ end if;
+
+ elsif No (Living_Id) then
+ Living_Id := E;
+ end if;
+
Next (Id);
end loop;
+
+ -- Detect a mixture of Ghost types and living types within the same use
+ -- type clause. Ideally one would split a use type clause with multiple
+ -- marks into multiple use type clauses with a single mark, however
+ -- clients of the front end will have to adapt to this change.
+
+ if Present (Ghost_Id) and then Present (Living_Id) then
+ Error_Msg_N
+ ("use clause cannot mention ghost and non-ghost ghost types", N);
+
+ Error_Msg_Sloc := Sloc (Ghost_Id);
+ Error_Msg_NE ("\& # declared as ghost", N, Ghost_Id);
+
+ Error_Msg_Sloc := Sloc (Living_Id);
+ Error_Msg_NE ("\& # declared as non-ghost", N, Living_Id);
+ end if;
+
+ Mark_Ghost_Clause (N);
end Analyze_Use_Type;
--------------------
