mirror/gcc
2
0
Fork 0
mirror of git://gcc.gnu.org/git/gcc.git synced 2025-04-13 16:31:20 +08:00
Code Issues Packages Projects Releases Wiki Activity

[Ada] Accept explicit SPARK_Mode Auto as configuration pragma

Browse Source 
An explicit value of Auto is now accepted for a configuration pragma
SPARK_Mode, as a way to exempt a unit from complete adherence to
SPARK rules when using a global configuration pragma file where
SPARK_Mode=>On is specified.

gcc/ada/

	* sem_prag.adb (Analyze_Pragma): Accept SPARK_Mode=>Auto as
	configuration pragma.
	(Get_SPARK_Mode): Make the value for Auto explicit.
	* snames.ads-tmpl (Name_Auto): Add name.
This commit is contained in:
Yannick Moy 2022-09-05 12:20:18 +02:00 committed by Marc Poulhiès
parent 517817a434
commit 4caf4b5ef3
2 changed files with 15 additions and 3 deletions

17
gcc/ada/sem_prag.adb

@ -23176,7 +23176,7 @@ package body Sem_Prag is
-- SPARK_Mode --
----------------
-- pragma SPARK_Mode [(On | Off)];
-- pragma SPARK_Mode [(Auto | On | Off)];
when Pragma_SPARK_Mode => Do_SPARK_Mode : declare
Mode_Id : SPARK_Mode_Type;
@ -23662,7 +23662,7 @@ package body Sem_Prag is
-- Check the legality of the mode (no argument = ON)
if Arg_Count = 1 then
Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off);
Check_Arg_Is_One_Of (Arg1, Name_Auto, Name_On, Name_Off);
Mode := Chars (Get_Pragma_Arg (Arg1));
else
Mode := Name_On;
@ -23713,6 +23713,15 @@ package body Sem_Prag is
-- the pragma resides to find a potential construct.
else
-- An explicit mode of Auto is only allowed as a configuration
-- pragma. Escape "pragma" to avoid replacement with "aspect".
if Mode_Id = None then
Error_Pragma_Arg
("only configuration 'p'r'a'g'm'a% can have value &",
Arg1);
end if;
Stmt := Prev (N);
while Present (Stmt) loop
@ -31169,7 +31178,9 @@ package body Sem_Prag is
function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type is
begin
if N = Name_On then
if N = Name_Auto then
return None;
elsif N = Name_On then
return On;
elsif N = Name_Off then
return Off;

1
gcc/ada/snames.ads-tmpl

@ -782,6 +782,7 @@ package Snames is
Name_Assertion : constant Name_Id := N + $;
Name_Assertions : constant Name_Id := N + $;
Name_Attribute_Name : constant Name_Id := N + $;
Name_Auto : constant Name_Id := N + $;
Name_Body_File_Name : constant Name_Id := N + $;
Name_Boolean_Entry_Barriers : constant Name_Id := N + $;
Name_By_Any : constant Name_Id := N + $;