diff options
author | Piotr Trojanek <trojanek@adacore.com> | 2023-05-02 16:03:18 +0200 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2023-06-13 09:31:45 +0200 |
commit | dcc601423c21a3902d6dd22d40a9a828ce9658b0 (patch) | |
tree | fd4c08f457c25ee27ea57fe3962b79151ba47b73 /gcc/ada/sem_util.ads | |
parent | 204dba400b42b75271071b05102a5b46fd2a34d0 (diff) | |
download | gcc-dcc601423c21a3902d6dd22d40a9a828ce9658b0.zip gcc-dcc601423c21a3902d6dd22d40a9a828ce9658b0.tar.gz gcc-dcc601423c21a3902d6dd22d40a9a828ce9658b0.tar.bz2 |
ada: Implement new aspect Always_Terminates for SPARK
This patch allows subprograms to be annotated with aspect
Always_Terminates that requires a boolean expression. When this
expression evaluates to True, the subprogram is required to terminate or
raise an exception, but not loop infinitely.
This aspect is only meant to be used by GNATprove and it has no
meaningful run-time semantics: either the annotated subprogram
terminates and then the aspect expression doesn't matter, or the
subprogram loops infinitely and there is nothing we can do. (We could
also evaluate the aspect expression just to detect run-time errors in
the expression itself, but this can be implemented later, after a
backend support for the aspect is added to GNATprove.)
Implementation of this aspect is heavily based on the implementation of
Subprogram_Variant, which in turn is heavily based on the implementation
of Contract_Cases. Since the new aspect is not yet expanded, there is no
corresponding assertion kind that would control the expansion.
gcc/ada/
* aspects.ads (Aspect_Id): Add new aspect.
(Implementation_Defined_Aspect): New aspect is
implementation-defined.
(Aspect_Argument): New aspect has an expression argument.
(Is_Representation_Aspect): New aspect is not a representation
aspect.
(Aspect_Names): Link new aspect identifier with a name.
(Aspect_Delay): New aspect is never delayed.
* contracts.adb (Expand_Subprogram_Contract): Mention new aspect
in comment.
(Add_Contract_Item): Attach pragma corresponding to the new aspect
to contract items.
(Analyze_Entry_Or_Subprogram_Contract): Analyze pragma
corresponding to the new aspect that appears with subprogram spec.
(Analyze_Subprogram_Body_Stub_Contract): Expand pragma
corresponding to the new aspect.
* contracts.ads
(Add_Contract_Item, Analyze_Entry_Or_Subprogram_Contract)
(Analyze_Entry_Or_Subprogram_Body_Contract)
(Analyze_Subprogram_Body_Stub_Contract): Mention new aspect in
comment.
* einfo-utils.adb (Get_Pragma): Return pragma attached to
contract.
* einfo-utils.ads (Get_Pragma): Mention new contract in comment.
* exp_prag.adb (Expand_Pragma_Always_Terminates): Placeholder for
possibly expanding new aspect.
* exp_prag.ads (Expand_Pragma_Always_Terminates): Dedicated
routine for expansion of the new aspect.
* inline.adb (Remove_Aspects_And_Pragmas): Remove aspect from
inlined bodies.
* par-prag.adb (Prag): Postpone checking of the pragma until
analysis.
* sem_ch12.adb: Mention new aspect in explanation of handling
contracts on generic units.
* sem_ch13.adb (Analyze_Aspect_Specifications): Convert new aspect
into a corresponding pragma.
(Check_Aspect_At_Freeze_Point): Don't expect new aspect.
* sem_prag.adb (Analyze_Always_Terminates_In_Decl_Part): Analyze
pragma corresponding to the new aspect.
(Analyze_Pragma): Handle pragma corresponding to the new aspect.
(Is_Non_Significant_Pragma_Reference): Handle references appearing
within new aspect.
* sem_prag.ads (Aspect_Specifying_Pragma): New aspect can be
emulated with a pragma.
(Assertion_Expression_Pragma): New aspect has an assertion
expression.
(Pragma_Significant_To_Subprograms): New aspect is significant to
subprograms.
(Analyze_Always_Terminates_In_Decl_Part): Add spec for routine
that analyses new aspect.
(Find_Related_Declaration_Or_Body): Mention new aspect in comment.
* sem_util.adb (Is_Subprogram_Contract_Annotation): New aspect is
a subprogram contract annotation.
* sem_util.ads (Is_Subprogram_Contract_Annotation): Mention new
aspect in comment.
* sinfo.ads (Is_Generic_Contract_Pragma): New pragma is a generic
contract.
(Contract): Explain attaching new pragma to subprogram contract.
* snames.ads-tmpl (Name_Always_Terminates): New name for the new
contract.
(Pragma_Always_Terminates): New pragma identifier.
Diffstat (limited to 'gcc/ada/sem_util.ads')
-rw-r--r-- | gcc/ada/sem_util.ads | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 539ebeb..3751fb7 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -2349,6 +2349,7 @@ package Sem_Util is function Is_Subprogram_Contract_Annotation (Item : Node_Id) return Boolean; -- Determine whether aspect specification or pragma Item is one of the -- following subprogram contract annotations: + -- Always_Terminates -- Contract_Cases -- Depends -- Exceptional_Cases |