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] Illegal constituent in state refinement


This patch modifies the logic in the analysis of aspect/pragma Refined_State
to catch a case where a visible variable is used as a constituent in a state
refinement.

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

--  pack.ads

package Pack
  with Abstract_State => State
is
   Var : Integer;

   procedure Proc (Formal : Integer)
     with Global => (Output => State);
end Pack;

--  pack.adb

package body Pack
  with Refined_State => (State => Var)
is
   procedure Proc (Formal : Integer)
     with Refined_Global => (Output => Var)
   is begin null; end Proc;
end Pack;

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

$ gcc -c -gnatd.V pack.adb
pack.adb:2:35: cannot use "Var" in refinement, constituent is not a hidden
  state of package "Pack"
pack.adb:5:11: useless refinement, subprogram "Proc" does not mention abstract
  state with visible refinement

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

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

	* sem_prag.adb (Analyze_Constituent): Move the check
	concerning option Part_Of to routine Check_Matching_Constituent.
	(Check_Matching_Constituent): Verify that an abstract state
	that acts as a constituent has the prope Part_Op option in
	its aspect/pragma Abstract_State.  Account for the case when a
	constituent comes from a private child or private sibling.
	* sem_util.ads, sem_util.adb (Is_Child_Or_Sibling): 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]