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] Allow generic package holding state

From: Pierre-Marie de Rodat <derodat at adacore dot com>
To: gcc-patches at gcc dot gnu dot org
Cc: Yannick Moy <moy at adacore dot com>
Date: Mon, 18 Sep 2017 04:48:04 -0400
Subject: [Ada] Allow generic package holding state
Authentication-results: sourceware.org; auth=none

SPARK RM 7.2.6(5) allows the hidden state of a generic package to be Part_Of
the state of the generic package. This was not properly supported. Now fixed.

The following code compiles without errors.

$ gcc -c gen.ads

 1. generic
 2.	 J : Integer;
 3. package Gen with
 4.   SPARK_Mode => On,
 5.   Abstract_State => State
 6. is
 7.	G : Boolean;
 8. private
 9.	 H : Boolean with Part_Of => State;
10. end Gen;

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

2017-09-18  Yannick Moy  <moy@adacore.com>

	* sem_util.adb (Find_Placement_In_State_Space): Allow generic package
	holding state.

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]