ada: Support aspect Program_Exit with no expression

New aspect Program_Exit for SPARK was originally designed to require an
expression, but now we want this expression to be optional.

gcc/ada/ChangeLog:

	* aspects.ads (Aspect_Argument): Argument for Program_Exit is now
	optional.
	* doc/gnat_rm/implementation_defined_pragmas.rst
	(Pragma Program_Exit): Change documentation for pragma syntax.
	* sem_prag.adb (Analyze_Pragma): Argument for Program_Exit is now
	optional.
	(Analyze_Program_Exit_In_Decl_Part): Likewise.
	* gnat_rm.texi: Regenerate.
	* gnat_ugn.texi: Regenerate.

diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index fc91ca23cbafc5e271fe6a9ae2db0e6162bcb38f..5e61450748ffd8e3de84f667ec1c14eb8cd70e51 100644 (file)
--- a/gcc/ada/aspects.ads
+++ b/gcc/ada/aspects.ads
@@ -482,7 +482,7 @@ package Aspects is
       Aspect_Predicate                  => Expression,
       Aspect_Predicate_Failure          => Expression,
       Aspect_Priority                   => Expression,
-      Aspect_Program_Exit               => Expression,
+      Aspect_Program_Exit               => Optional_Expression,
       Aspect_Put_Image                  => Name,
       Aspect_Read                       => Name,
       Aspect_Real_Literal               => Name,

diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
index 50de68a4cea2e8c6e35ec96a4c76d88e038bb506..685bdde48a5dc6a84feadb027f1273685b338795 100644 (file)
--- a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
+++ b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
@@ -5294,7 +5294,7 @@ Syntax:
 
 .. code-block:: ada
 
-  pragma Program_Exit (boolean_EXPRESSION);
+  pragma Program_Exit [ (boolean_EXPRESSION) ];
 
 For the semantics of this pragma, see the entry for aspect ``Program_Exit``
 in the SPARK 2014 Reference Manual, section 6.1.10.

diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index fb7c6238856b5786c9b4b872cc00711834b6824a..c67c198b8c4b3b7af01acacd9093864a32c6d0b1 100644 (file)
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -6942,7 +6942,7 @@ of error messages.
 Syntax:
 
 @example
-pragma Program_Exit (boolean_EXPRESSION);
+pragma Program_Exit [ (boolean_EXPRESSION) ];
 @end example
 
 For the semantics of this pragma, see the entry for aspect @code{Program_Exit}

diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi
index ca1d7bcc1abf2925498bb0c80df47603b5eef884..5331a318c0d875d1f7a4307a535b3cb6df5a0c5f 100644 (file)
--- a/gcc/ada/gnat_ugn.texi
+++ b/gcc/ada/gnat_ugn.texi
@@ -29833,8 +29833,8 @@ to permit their use in free software.
 
 @printindex ge
 
-@anchor{gnat_ugn/gnat_utility_programs switches-related-to-project-files}@w{                              }
 @anchor{d2}@w{                              }
+@anchor{gnat_ugn/gnat_utility_programs switches-related-to-project-files}@w{                              }
 
 @c %**end of body
 @bye

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index b35aa4aa2519464a860b98e4b89d97eebfb86069..9964f70ce201705958cf85c76b4e7ce30fd84ebf 100644 (file)
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -23640,7 +23640,7 @@ package body Sem_Prag is
          begin
             GNAT_Pragma;
             Check_No_Identifiers;
-            Check_Arg_Count (1);
+            Check_At_Most_N_Arguments (1);
 
             --  Ensure the proper placement of the pragma. Program_Exit must be
             --  associated with a subprogram declaration or a body that acts as
@@ -28413,8 +28413,8 @@ package body Sem_Prag is
    is
       Subp_Decl : constant Node_Id   := Find_Related_Declaration_Or_Body (N);
       Spec_Id   : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
-
-      Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
+      Arg1      : constant Node_Id   :=
+        First (Pragma_Argument_Associations (N));
 
       Saved_GM  : constant Ghost_Mode_Type := Ghost_Mode;
       Saved_IGR : constant Node_Id         := Ignored_Ghost_Region;
@@ -28440,56 +28440,61 @@ package body Sem_Prag is
             "for subprograms with side effects", N);
       end if;
 
-      --  Set the Ghost mode in effect from the pragma. Due to the delayed
-      --  analysis of the pragma, the Ghost mode at point of declaration and
-      --  point of analysis may not necessarily be the same. Use the mode in
-      --  effect at the point of declaration.
+      if Present (Arg1) then
 
-      Set_Ghost_Mode (N);
+         --  Set the Ghost mode in effect from the pragma. Due to the delayed
+         --  analysis of the pragma, the Ghost mode at point of declaration and
+         --  point of analysis may not necessarily be the same. Use the mode in
+         --  effect at the point of declaration.
 
-      --  Ensure that the subprogram and its formals are visible when analyzing
-      --  the expression of the pragma.
+         Set_Ghost_Mode (N);
 
-      if not In_Open_Scopes (Spec_Id) then
-         Restore_Scope := True;
+         --  Ensure that the subprogram and its formals are visible when
+         --  analyzing the expression of the pragma.
 
-         if Is_Generic_Subprogram (Spec_Id) then
-            Push_Scope (Spec_Id);
-            Install_Generic_Formals (Spec_Id);
-         else
-            Push_Scope (Spec_Id);
-            Install_Formals (Spec_Id);
+         if not In_Open_Scopes (Spec_Id) then
+            Restore_Scope := True;
+
+            if Is_Generic_Subprogram (Spec_Id) then
+               Push_Scope (Spec_Id);
+               Install_Generic_Formals (Spec_Id);
+            else
+               Push_Scope (Spec_Id);
+               Install_Formals (Spec_Id);
+            end if;
          end if;
-      end if;
 
-      Errors := Serious_Errors_Detected;
+         Errors := Serious_Errors_Detected;
 
-      --  Preanalyze_And_Resolve_Assert_Expression enforcing the expression
-      --  type.
+         --  Preanalyze_And_Resolve_Assert_Expression enforcing the expression
+         --  type.
 
-      Preanalyze_And_Resolve_Assert_Expression (Expr, Any_Boolean);
+         Preanalyze_And_Resolve_Assert_Expression
+           (Expression (Arg1), Any_Boolean);
 
-      --  Emit a clarification message when the expression contains at least
-      --  one undefined reference, possibly due to contract freezing.
+         --  Emit a clarification message when the expression contains at least
+         --  one undefined reference, possibly due to contract freezing.
 
-      if Errors /= Serious_Errors_Detected
-        and then Present (Freeze_Id)
-        and then Has_Undefined_Reference (Expr)
-      then
-         Contract_Freeze_Error (Spec_Id, Freeze_Id);
-      end if;
+         if Errors /= Serious_Errors_Detected
+           and then Present (Freeze_Id)
+           and then Has_Undefined_Reference (Expression (Arg1))
+         then
+            Contract_Freeze_Error (Spec_Id, Freeze_Id);
+         end if;
 
-      if Restore_Scope then
-         End_Scope;
-      end if;
+         if Restore_Scope then
+            End_Scope;
+         end if;
 
-      --  Currently it is not possible to inline pre/postconditions on a
-      --  subprogram subject to pragma Inline_Always.
+         --  Currently it is not possible to inline pre/postconditions on a
+         --  subprogram subject to pragma Inline_Always.
 
-      Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
-      Set_Is_Analyzed_Pragma (N);
+         Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
 
-      Restore_Ghost_Region (Saved_GM, Saved_IGR);
+         Restore_Ghost_Region (Saved_GM, Saved_IGR);
+      end if;
+
+      Set_Is_Analyzed_Pragma (N);
    end Analyze_Program_Exit_In_Decl_Part;
 
    ------------------------------------------