diff options
| author | Hristian Kirtchev <kirtchev@adacore.com> | 2014-08-04 10:55:30 +0000 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-08-04 12:55:30 +0200 |
| commit | f3124d8f6431bcfce76eca31a198ba89ce0d15fe (patch) | |
| tree | 121b03cc943bf71264e84e46bed57fea3f122034 /gcc/ada/sem_ch13.adb | |
| parent | f10ff6cc46ab7e851afbaf05818f4e9db0f8a335 (diff) | |
| download | gcc-f3124d8f6431bcfce76eca31a198ba89ce0d15fe.zip gcc-f3124d8f6431bcfce76eca31a198ba89ce0d15fe.tar.gz gcc-f3124d8f6431bcfce76eca31a198ba89ce0d15fe.tar.bz2 | |
2014-08-04 Hristian Kirtchev <kirtchev@adacore.com>
* opt.ads Alphabetize various global flags. New flag
Ignore_Pragma_SPARK_Mode along with a comment on usage.
* sem_ch6.adb (Analyze_Generic_Subprogram_Body):
Pragma SPARK_Mode is now allowed in generic units.
(Analyze_Subprogram_Body_Helper): Do not verify the compatibility
between the SPARK_Mode of a spec and that of a body when inside
a generic.
* sem_ch7.adb (Analyze_Package_Body_Helper): Do not verify the
compatibility between the SPARK_Mode of a spec and that of a
body when inside a generic.
* sem_ch12.adb (Analyze_Generic_Subprogram_Declaration):
Pragma SPARK_Mode is now allowed in generic units.
(Analyze_Package_Instantiation): Save and restore the value of
flag Ignore_ Pragma_SPARK_Mode in a stack-like fasion. Set
the governing SPARK_Mode before analyzing the instance.
(Analyze_Subprogram_Instantiation): Save and restore the value
of flag Ignore_ Pragma_SPARK_Mode in a stack-like fasion. Set
the governing SPARK_Mode before analyzing the instance.
* sem_ch13.adb (Analyze_Aspect_Specifications): Emulate the
placement of a source pragma when inserting the generated pragma
for aspect SPARK_Mode.
* sem_prag.adb (Analyze_Pragma): Reimplement the handling of
pragma SPARK_Mode to allow for generics and their respective
instantiations.
* sem_util.ads, sem_util.adb (Check_SPARK_Mode_In_Generic): Removed.
(Set_Ignore_Pragma_SPARK_Mode): New routine.
From-SVN: r213570
Diffstat (limited to 'gcc/ada/sem_ch13.adb')
| -rw-r--r-- | gcc/ada/sem_ch13.adb | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index ca52755..dc226b3 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -2418,11 +2418,11 @@ package body Sem_Ch13 is Expression => Relocate_Node (Expr))), Pragma_Name => Name_SPARK_Mode); - -- When the aspect appears on a package body, insert the - -- generated pragma at the top of the body declarations to - -- emulate the behavior of a source pragma. + -- When the aspect appears on a package or a subprogram + -- body, insert the generated pragma at the top of the body + -- declarations to emulate the behavior of a source pragma. - if Nkind (N) = N_Package_Body then + if Nkind_In (N, N_Package_Body, N_Subprogram_Body) then Decorate (Aspect, Aitem); Decls := Declarations (N); @@ -2435,11 +2435,14 @@ package body Sem_Ch13 is Prepend_To (Decls, Aitem); goto Continue; - -- When the aspect is associated with package declaration, - -- insert the generated pragma at the top of the visible - -- declarations to emulate the behavior of a source pragma. + -- When the aspect is associated with a [generic] package + -- declaration, insert the generated pragma at the top of + -- the visible declarations to emulate the behavior of a + -- source pragma. - elsif Nkind (N) = N_Package_Declaration then + elsif Nkind_In (N, N_Generic_Package_Declaration, + N_Package_Declaration) + then Decorate (Aspect, Aitem); Decls := Visible_Declarations (Specification (N)); |