This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |
Other format: | [Raw text] |
This patch ensures that all delayed SPARK aspects are analyzed with the proper SPARK mode of their related construct. ------------ -- Source -- ------------ -- modes.ads package Modes with SPARK_Mode => On, Abstract_State => State is Var : Integer := 1; procedure Disabled_1 (Formal : Integer) with SPARK_Mode => Off, Global => (Input => (Formal, State, Var)), -- suppressed Depends => (null => (Formal, Var)); -- suppressed procedure Enabled_1 (Formal : Integer) with SPARK_Mode => On, Global => (Input => (Formal, State, Var)), -- error Depends => (null => (Formal, Var)); -- error end Modes; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c modes.ads modes.ads:14:33: global item cannot reference parameter of subprogram modes.ads:14:41: state "State" must appear in at least one input dependence list Tested on x86_64-pc-linux-gnu, committed on trunk 2014-07-17 Hristian Kirtchev <kirtchev@adacore.com> * sem_ch6.adb (Analyze_Subprogram_Body_Contract, Analyze_Subprogram_Contract): Add new local variable Mode. Save and restore the SPARK mode of the related construct in a stack-like fashion. * sem_ch7.adb (Analyze_Package_Body_Contract, Analyze_Package_Contract): Add new local variable Mode. Save and restore the SPARK mode of the related construct in a stack-like fashion. * sem_util.adb Remove with and use clause for Opt. (Restore_SPARK_Mode): New routine. (Save_SPARK_Mode_And_Set): New routine. * sem_util.ads Add with and use clause for Opt. (Restore_SPARK_Mode): New routine. (Save_SPARK_Mode_And_Set): New routine.
Attachment:
difs
Description: Text document
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |