diff options
author | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-04-25 12:49:34 +0200 |
---|---|---|
committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-04-25 12:49:34 +0200 |
commit | cf9a473e6494aef4d6e36dfdab64b3c42bfe5958 (patch) | |
tree | 3ba8a2ea4ab83bda23bcdc99817bc62e7a3b9002 /gcc/ada/sem_ch7.adb | |
parent | 1f0bcd44fe7967cd994a2a1d1397305b4b8f2e47 (diff) | |
download | gcc-cf9a473e6494aef4d6e36dfdab64b3c42bfe5958.zip gcc-cf9a473e6494aef4d6e36dfdab64b3c42bfe5958.tar.gz gcc-cf9a473e6494aef4d6e36dfdab64b3c42bfe5958.tar.bz2 |
[multiple changes]
2017-04-25 Hristian Kirtchev <kirtchev@adacore.com>
* einfo.adb Flag301 is now known as Ignore_SPARK_Mode_Pragmas.
(Ignore_SPARK_Mode_Pragmas): New routine.
(Set_Ignore_SPARK_Mode_Pragmas): New routine.
(Write_Entity_Flags): Add an entry for Ignore_SPARK_Mode_Pragmas.
* einfo.ads Add new attribute Ignore_SPARK_Mode_Pragmas and update
related entities.
(Ignore_SPARK_Mode_Pragmas): New routine
along with pragma Inline.
(Set_Ignore_SPARK_Mode_Pragmas): New routine along with pragma Inline.
* opt.ads Rename flag Ignore_Pragma_SPARK_Mode to
Ignore_SPARK_Mode_Pragmas_In_Instance.
* sem_ch6.adb (Analyze_Subprogram_Body_Helper):
Save and restore the value of global flag
Ignore_SPARK_Mode_Pragmas_In_Instance. Set or reinstate the value
of global flag Ignore_SPARK_Mode_Pragmas_In_Instance when either
the corresponding spec or the body must ignore all SPARK_Mode
pragmas found within.
(Analyze_Subprogram_Declaration): Mark
the spec when it needs to ignore all SPARK_Mode pragmas found
within to allow the body to infer this property in case it is
instantiated or inlined later.
* sem_ch7.adb (Analyze_Package_Body_Helper): Save and restore the
value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set
the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance
when the corresponding spec also ignored all SPARK_Mode pragmas
found within.
(Analyze_Package_Declaration): Mark the spec when
it needs to ignore all SPARK_Mode pragmas found within to allow
the body to infer this property in case it is instantiated or
inlined later.
* sem_ch12.adb (Analyze_Formal_Package_Declaration):
Save and restore the value of flag
Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the
formal spec when it needs to ignore all SPARK_Mode
pragmas found within to allow the body to infer this
property in case it is instantiated or inlined later.
(Analyze_Package_Instantiation): Save and restore the value
of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark
the instance spec when it needs to ignore all SPARK_Mode
pragmas found within to allow the body to infer this
property in case it is instantiated or inlined later.
(Analyze_Subprogram_Instantiation): Save and restore the value
of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the
instance spec and anonymous package when they need to ignore
all SPARK_Mode pragmas found within to allow the body to infer
this property in case it is instantiated or inlined later.
(Instantiate_Package_Body): Save and restore the value of global
flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set the value of
global flag Ignore_SPARK_Mode_Pragmas_In_Instance when the
corresponding instance spec also ignored all SPARK_Mode pragmas
found within.
(Instantiate_Subprogram_Body): Save and restore the
value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set
the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance
when the corresponding instance spec also ignored all SPARK_Mode
pragmas found within.
* sem_prag.adb (Analyze_Pragma): Update the reference to
Ignore_Pragma_SPARK_Mode.
* sem_util.adb (SPARK_Mode_Is_Off): A construct which ignored
all SPARK_Mode pragmas defined within yields mode "off".
2017-04-25 Hristian Kirtchev <kirtchev@adacore.com>
* bindgen.adb, exp_dbug.adb, errout.adb, fname.adb: Minor reformatting.
2017-04-25 Bob Duff <duff@adacore.com>
* exp_atag.adb (Build_CW_Membership): Add "Suppress =>
All_Checks" to avoid generating unnecessary checks.
* exp_ch4.adb (Expand_N_In, Make_Tag_Check): Add "Suppress =>
All_Checks".
* sem.ads: Fix comment.
* expander.ads: Fix comment.
* exp_atag.ads: Fix comment: "Index = 0" should be
"Index >= 0".
2017-04-25 Gary Dismukes <dismukes@adacore.com>
* s-taprop-linux.adb: Minor editorial fixes.
From-SVN: r247182
Diffstat (limited to 'gcc/ada/sem_ch7.adb')
-rw-r--r-- | gcc/ada/sem_ch7.adb | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index e5879df..260f923 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -539,6 +539,8 @@ package body Sem_Ch7 is -- Local variables + Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; + Body_Id : Entity_Id; HSS : Node_Id; Last_Spec_Entity : Entity_Id; @@ -738,6 +740,14 @@ package body Sem_Ch7 is Set_SPARK_Aux_Pragma (Body_Id, SPARK_Mode_Pragma); Set_SPARK_Pragma_Inherited (Body_Id); Set_SPARK_Aux_Pragma_Inherited (Body_Id); + + -- A package body may be instantiated or inlined at a later pass. + -- Restore the state of Ignore_SPARK_Mode_Pragmas_In_Instance when + -- it applied to the package spec. + + if Ignore_SPARK_Mode_Pragmas (Spec_Id) then + Ignore_SPARK_Mode_Pragmas_In_Instance := True; + end if; end if; Set_Categorization_From_Pragmas (N); @@ -931,6 +941,8 @@ package body Sem_Ch7 is end if; end if; + Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP; + Restore_Ghost_Mode (Mode); end Analyze_Package_Body_Helper; @@ -969,6 +981,15 @@ package body Sem_Ch7 is Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma); Set_SPARK_Pragma_Inherited (Id); Set_SPARK_Aux_Pragma_Inherited (Id); + + -- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in + -- case the body of this package is instantiated or inlined later and + -- out of context. The body uses this attribute to restore the value + -- of the global flag. + + if Ignore_SPARK_Mode_Pragmas_In_Instance then + Set_Ignore_SPARK_Mode_Pragmas (Id); + end if; end if; -- Analyze aspect specifications immediately, since we need to recognize |