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]

[Ada] Proper resolution of Initializes and Initial_Condition


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]