https://gcc.gnu.org/g:8952d7caf9e6bd9b19dc4efb3af702c566d8e474
commit r16-1237-g8952d7caf9e6bd9b19dc4efb3af702c566d8e474
Author: Piotr Trojanek <troja...@adacore.com>
Date: Thu Feb 13 16:39:43 2025 +0100
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:
---
gcc/ada/aspects.ads | 2 +-
.../doc/gnat_rm/implementation_defined_pragmas.rst | 2 +-
gcc/ada/gnat_rm.texi | 2 +-
gcc/ada/gnat_ugn.texi | 2 +-
gcc/ada/sem_prag.adb | 83 ++++++++++++----------
5 files changed, 48 insertions(+), 43 deletions(-)
diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index fc91ca23cbaf..5e61450748ff 100644
--- 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 50de68a4cea2..685bdde48a5d 100644
--- 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 fb7c6238856b..c67c198b8c4b 100644
--- 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 ca1d7bcc1abf..5331a318c0d8 100644
--- 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 b35aa4aa2519..9964f70ce201 100644
--- 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;
------------------------------------------
