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] Use of SPARK_Mode with front end inlining (-gnatN)


This patch modifies the front end inlining mechanism to ensure that a package
body is always analyzed with the SPARK_Mode of the enclosing context.

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

--  front_end_inlining.adc

pragma SPARK_Mode (On);

--  front_end_inlining.ads

package Front_End_Inlining is
   procedure P;
end Front_End_Inlining;

--  front_end_inlining.adb

with Ada.Text_IO; use Ada.Text_IO;

package body Front_End_Inlining with SPARK_Mode => Off is
   subtype Small_Int is Integer range 0 .. 3;

   procedure P is
      package Small_Int_IO is new Integer_IO (Small_Int);
   begin
      null;
   end P;
end Front_End_Inlining;

-----------------
-- Compilation --
-----------------

$ gcc -c -gnatec=front_end_inlining.adc -gnatN front_end_inlining.adb

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

2014-10-23  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch12.adb (Inline_Instance_Body): Alphabetize
	local variables and constants. Add constants Save_SM and Save_SMP
	to capture SPARK_Mode-related attributes.  Compile the inlined
	body with the SPARK_Mode of the enclosing context.

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]