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 modifies the processing of SPARK annotations Initializes and Initial_Condition to perform the resolution of the related expressions at the end of the enclosing package visible declarations. ------------ -- Source -- ------------ -- init_cond.ads package Init_Cond with SPARK_Mode, Initial_Condition => Vis_Var -- OK and Vis_Func -- OK and Vis_Nested.Var -- OK and Vis_Nested.Func -- OK and Priv_Var -- Error and Priv_Func -- Error and Priv_Nested.Var -- Error and Priv_Nested.Func -- Error is Vis_Var : Boolean := False; function Vis_Func return Boolean; package Vis_Nested is Var : Boolean := True; function Func return Boolean; end Vis_Nested; private Priv_Var : Boolean := False; function Priv_Func return Boolean; package Priv_Nested is Var : Boolean := True; function Func return Boolean; end Priv_Nested; end Init_Cond; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c init_cond.ads init_cond.ads:8:16: "Priv_Var" is undefined init_cond.ads:9:16: "Priv_Func" is undefined init_cond.ads:10:16: "Priv_Nested" is undefined (more references follow) Tested on x86_64-pc-linux-gnu, committed on trunk 2017-10-14 Hristian Kirtchev <kirtchev@adacore.com> * sem_ch3.adb (Analyze_Declarations): Analyze the contract of an enclosing package at the end of the visible declarations. * sem_prag.adb (Analyze_Initialization_Item): Suppress the analysis of an initialization item which is undefined due to some illegality.
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] |