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/pragma SPARK_Mode in generic


This patch allows the uses of aspect/pragma SPARK_Mode in generic units. It
also implements the following rule concerning the interplay between instances
and SPARK_Mode "off":

   However, if an instance of a generic unit is enclosed by code where
   SPARK_Mode is Off and if any SPARK_Mode specifications occur within the
   generic unit, then the corresponding SPARK_Mode specifications occurring
   within the instance have no semantic effect.

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

--  pack_gen_pragmas.ads

generic
package Pack_Gen_Pragmas with SPARK_Mode => On is
   Var_1 : Integer := 1
     with Volatile, Async_Readers, Effective_Reads;

   procedure Force_Body;
private
   pragma SPARK_Mode (Off);

   Var_2 : Integer := 2
     with Volatile, Async_Readers, Effective_Reads;
end Pack_Gen_Pragmas;

--  pack_gen_pragmas.adb

package body Pack_Gen_Pragmas is
   procedure Force_Body is begin null; end Force_Body;
end Pack_Gen_Pragmas;

--  pack_pragmas_inst_4.ads

with Pack_Gen_Pragmas;

package Pack_Pragmas_Inst_4 is
   package Inst is new Pack_Gen_Pragmas
     with SPARK_Mode => Off;
end Pack_Pragmas_Inst_4;

--  pack_pragmas_inst_5.ads

with Pack_Gen_Pragmas;

package Pack_Pragmas_Inst_5 is new Pack_Gen_Pragmas;
pragma SPARK_Mode (On);

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

$ gcc -c pack_pragmas_inst_4.ads
$ gcc -c pack_pragmas_inst_5.ads
pack_pragmas_inst_5.ads:3:01: instantiation error at pack_gen_pragmas.ads:3
pack_pragmas_inst_5.ads:3:01: illegal combination of external properties
  (SPARK RM 7.1.2(6))

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

2014-08-04  Hristian Kirtchev  <kirtchev@adacore.com>

	* opt.ads Alphabetize various global flags. New flag
	Ignore_Pragma_SPARK_Mode along with a comment on usage.
	* sem_ch6.adb (Analyze_Generic_Subprogram_Body):
	Pragma SPARK_Mode is now allowed in generic units.
	(Analyze_Subprogram_Body_Helper): Do not verify the compatibility
	between the SPARK_Mode of a spec and that of a body when inside
	a generic.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Do not verify the
	compatibility between the SPARK_Mode of a spec and that of a
	body when inside a generic.
	* sem_ch12.adb (Analyze_Generic_Subprogram_Declaration):
	Pragma SPARK_Mode is now allowed in generic units.
	(Analyze_Package_Instantiation): Save and restore the value of
	flag Ignore_ Pragma_SPARK_Mode in a stack-like fasion. Set
	the governing SPARK_Mode before analyzing the instance.
	(Analyze_Subprogram_Instantiation): Save and restore the value
	of flag Ignore_ Pragma_SPARK_Mode in a stack-like fasion. Set
	the governing SPARK_Mode before analyzing the instance.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Emulate the
	placement of a source pragma when inserting the generated pragma
	for aspect SPARK_Mode.
	* sem_prag.adb (Analyze_Pragma): Reimplement the handling of
	pragma SPARK_Mode to allow for generics and their respective
	instantiations.
	* sem_util.ads, sem_util.adb (Check_SPARK_Mode_In_Generic): Removed.
	(Set_Ignore_Pragma_SPARK_Mode): 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]