From: "Marc Poulhiès" <poulhies@adacore.com>
To: gcc-patches@gcc.gnu.org
Cc: Yannick Moy <moy@adacore.com>
Subject: [Ada] Accept explicit SPARK_Mode Auto as configuration pragma
Date: Mon, 12 Sep 2022 10:19:35 +0200 [thread overview]
Message-ID: <20220912081935.GA1513026@poulhies-Precision-5550> (raw)
[-- Attachment #1: Type: text/plain, Size: 467 bytes --]
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.
Tested on x86_64-pc-linux-gnu, committed on trunk
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.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 2360 bytes --]
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
--- a/gcc/ada/sem_prag.adb
+++ b/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;
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
--- a/gcc/ada/snames.ads-tmpl
+++ b/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 + $;
reply other threads:[~2022-09-12 8:19 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20220912081935.GA1513026@poulhies-Precision-5550 \
--to=poulhies@adacore.com \
--cc=gcc-patches@gcc.gnu.org \
--cc=moy@adacore.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).