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] Aspect Initializes


This patch provides the initial implementation of aspect/pragma Initializes.
This construct is intended for formal verification purposes.

The syntax of the aspect/pragma is as follows:

   pragma Initializes (INITIALIZATION_SPEC);

   INITIALIZATION_SPEC ::= null | INITIALIZATION_LIST

   INITIALIZATION_LIST ::=
     INITIALIZATION_ITEM
     | (INITIALIZATION_ITEM {, INITIALIZATION_ITEM})

   INITIALIZATION_ITEM ::= name [=> INPUT_LIST]

   INPUT_LIST ::=
     null
     | INPUT
     | (INPUT {, INPUT})

   INPUT ::= name

The semantics of the aspect/pragma are as follows:

An Initializes aspect shall only appear in the aspect_specification of a
package_specification.

The Initializes aspect shall follow the Abstract_State aspect if one is
present.

The name of each initialization_item in the Initializes aspect definition for a
package shall denote a state abstraction of the package or an entire variable
declared immediately within the visible part of the package.

Each name in the input_list shall denote an entire variable or a state
abstraction but shall not denote an entity declared in the package with the
aspect_specification containing the Initializes aspect.

Each entity in a single input_list shall be distinct.

The Initializes aspect of a package has visibility of the declarations
occurring immediately within the visible part of the package.

------------
-- Source --
------------

--  semantics.ads

package Semantics
  with Abstract_State => State_1,
       Initializes    =>
         (State_1,
          Var_1,
          Var_2.Data,               --  not a whole object
          Priv,                     --  not visible
          "Junk",                   --  not a whole object or state
          null,                     --  cannot have null
          Var_1,                    --  duplicate
          Var_7 => Var_1,           --  item cannot be local
          Var_8 => (Var_2, Var_7))  --  items cannot be local
is
   type Rec is record
      Data : Integer;
   end record;

   Var_1 : Integer;
   Var_2 : Rec;

   package Error_1
     with Initializes    => (State_2, Var_3),  --  out of order
          Abstract_State =>  State_2
   is
      Var_3 : Integer;
   end Error_1;

   package Error_2
     with Initializes =>   ((State_3, Var_4))
   is
      pragma Abstract_State (State_3);  --  out of order
      Var_4 : Integer;
   end Error_2;

   package Error_3 is
      pragma Initializes   ((State_4, Var_5));
      pragma Abstract_State (State_4);  --  out of order
      Var_5 : Integer;
   end Error_3;

   package Error_4
     with Initializes => Var_6  --  no such entity
   is end Error_4;

   Var_7 : Integer;
   Var_8 : Integer;

private
   Priv : Integer;
end Semantics;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c -gnat12 -gnatd.V semantics.ads
semantics.ads:6:16: initialization item must denote variable or state
semantics.ads:7:11: "Priv" is undefined
semantics.ads:8:11: initialization item must denote variable or state
semantics.ads:9:11: package "Semantics" has non-null initialization
semantics.ads:10:11: duplicate initialization item
semantics.ads:11:20: input item "Var_1" cannot denote a visible variable or
  state of package "Semantics"
semantics.ads:12:21: input item "Var_2" cannot denote a visible variable or
  state of package "Semantics"
semantics.ads:12:28: input item "Var_7" cannot denote a visible variable or
  state of package "Semantics"
semantics.ads:23:11: aspect "Abstract_State" must come before aspect
  "Initializes"
semantics.ads:31:07: pragma "Abstract_State" cannot come after aspect
  "Initializes"
semantics.ads:37:07: pragma "Abstract_State" cannot come after pragma
  "Initializes"
semantics.ads:42:26: "Var_6" is undefined

Tested on x86_64-pc-linux-gnu, committed on trunk

2013-10-14  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb: Add an entry in table Canonical_Aspect for
	Initializes.
	* aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument,
	Aspect_Names and Aspect_Delay for Initializes.
	* atree.ads, atree.adb (Ekind_In): New seven argument versions of the
	routines.
	* einfo.adb: Remove Refined_State_Pragma from the list of node
	usage. Finalizer is now at position 28.
	(Contract): Package
	and package bodies now have a contract.
	(Finalizer): Update
	the assertion and node usage.
	(Get_Pragma): Update the Is_CDG
	flag to include Abstract_State, Initializes and Refined_State.
	(Refined_State_Pragma): Removed.
	(Set_Contract): Package and
	package bodies now have a contract.
	(Set_Finalizer): Update the
	assertion and node usage.
	(Set_Refined_State_Pragma): Removed.
	(Write_Field8_Name): Remove the output for Refined_State_Pragma.
	(Write_Field24_Name): Remove the output for Finalizer. Package
	and package bodies now have a contract.
	(Write_Field28_Name):
	Add output for Finalizer.
	* einfo.ads: Update the documentation and usage in entities
	of attribute Contract. Update the node position and usage in
	entities of attribute Finalizer. Remove the documentation
	and usage in entities for attribute Refined_State_Pragma.
	(Refined_State_Pragma): Removed along with pragma Inline.
	(Set_Refined_State_Pragma): Removed along with pragma Inline.
	* par-prag.adb: Add Initializes to the pragmas that do not
	require special processing by the parser.
	* sem_ch3.adb (Analyze_Declarations): Add local variable
	Prag. Update the retrieval of pragma Refined_State. Analyze
	aspect/pragma Initializes at the end of the visible declarations
	of the related package.
	* sem_ch6.adb (Analyze_Subprogram_Body_Contract):
	Add local variables Ref_Depends and Ref_Global. Analyze
	pragmas Refined_Global and Refined_Depends in that order.
	(Analyze_Subprogram_Contract): Add local variables Depends and
	Global. Analyze pragmas Global and Depends in that order.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Package
	bodies now have a contract. Move the analysis of the aspect
	specifications after the defining entity has been decorated.
	(Analyze_Package_Declaration): Packages now have a contract. Move
	the analysis of the aspect specifications after the defining
	entity has been decorated.
	* sem_ch12.adb (Analyze_Generic_Package_Declaration): Packages
	now have contracts.
	* sem_ch13.adb (Analyze_Pragma): Code cleanup for aspect
	Abstract_State. Add processing for aspect Initializes.
	(Check_Aspect_At_Freeze_Point): Add an entry for Initializes.
	* sem_prag.adb: Use Get_Pragma_Arg to extract the expression
	of a pragma argument. Add an entry in table Sig_Flags for
	Initializes.
	(Analyze_Initializes_In_Decl_Part): New routine.
	(Analyze_Pragma): Check the declaration order of pragmas
	Abstract_State and Initializes. Abstract_State is now part of
	the package contract. Analyze pragma Initializes. Check for
	duplicate Refined_State pragma. Refined_State is now part of
	the package contract.
	(Check_Declaration_Order): New routine.
	(Check_Test_Case): Alphabetized.
	* sem_prag.ads (Analyze_Initializes_In_Decl_Part): New routine.
	* sem_util.adb (Add_Contract_Item): Rename formal Subp_Id
	to Id. This routine can now support contracts on packages and
	package bodies.
	* sem_util.ads (Add_Contract_Item): Rename formal Subp_Id to
	Id. Update comment on usage.
	* sinfo.ads: Update the usage of N_Contract nodes.
	* snames.ads-tmpl: Add predefined name Initializes. Add new
	pragma id for Initializes.

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]