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] Poor error message on pragma SPARK_Mode


This patch modifies the mode conformance checks of pragma SPARK_Mode to account
for the case where the pragma appears without an argument.

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

--  pack.ads

package Pack is
   procedure Error;
end Pack;

--  pack.adb

package body Pack is
   procedure Error with SPARK_Mode is
   begin null; end Error;
end Pack;

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

$ gcc -c -gnatd.F pack.adb
pack.adb:2:25: incorrect use of SPARK_Mode
pack.adb:2:25: no value was set for SPARK_Mode on "Error" at pack.ads:2

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

2015-02-05  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Check_Pragma_Conformance): Add
	local variable Arg. Ensure that all errors are associated with
	the pragma if it appears without an argument. Add comments on
	various cases.

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]