[Ada] Issue error on invalid use of Ghost inside pragma Predicate

Message ID 20211025150853.GA346257@adacore.com
State Committed
Commit 5145d173a85d9cc7afe351ce33639d559c344e9d
Headers
Series [Ada] Issue error on invalid use of Ghost inside pragma Predicate |

Commit Message

Pierre-Marie de Rodat Oct. 25, 2021, 3:08 p.m. UTC
  Checking for ghost placement was only occurring inside the various
versions of predicate aspects, not inside the pragma Predicate. Now
fixed.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* sem_ch13.adb (Freeze_Entity_Checks): Perform same check on
	predicate expression inside pragma as inside aspect.
	* sem_util.adb (Is_Current_Instance): Recognize possible
	occurrence of subtype as current instance inside the pragma
	Predicate.
  

Patch

diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -13144,6 +13144,28 @@  package body Sem_Ch13 is
                   else
                      Check_Aspect_At_Freeze_Point (Ritem);
                   end if;
+
+               --  A pragma Predicate should be checked like one of the
+               --  corresponding aspects, wrt possible misuse of ghost
+               --  entities.
+
+               elsif Nkind (Ritem) = N_Pragma
+                 and then No (Corresponding_Aspect (Ritem))
+                 and then
+                   Get_Pragma_Id (Pragma_Name (Ritem)) = Pragma_Predicate
+               then
+                  --  Retrieve the visibility to components and discriminants
+                  --  in order to properly analyze the pragma.
+
+                  declare
+                     Arg : constant Node_Id :=
+                        Next (First (Pragma_Argument_Associations (Ritem)));
+                  begin
+                     Push_Type (E);
+                     Preanalyze_Spec_Expression
+                       (Expression (Arg), Standard_Boolean);
+                     Pop_Type (E);
+                  end;
                end if;
 
                Next_Rep_Item (Ritem);


diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -16644,7 +16644,8 @@  package body Sem_Util is
             --  Predicate_Failure aspect, for which we do not construct a
             --  wrapper procedure. The subtype will be replaced by the
             --  expression being tested when the corresponding predicate
-            --  check is expanded.
+            --  check is expanded. It may also appear in the pragma Predicate
+            --  expression during legality checking.
 
             elsif Nkind (P) = N_Aspect_Specification
               and then Nkind (Parent (P)) = N_Subtype_Declaration
@@ -16652,7 +16653,8 @@  package body Sem_Util is
                return True;
 
             elsif Nkind (P) = N_Pragma
-              and then Get_Pragma_Id (P) = Pragma_Predicate_Failure
+              and then Get_Pragma_Id (P) in Pragma_Predicate
+                                          | Pragma_Predicate_Failure
             then
                return True;
             end if;