diff options
| author | Yannick Moy <moy@adacore.com> | 2022-09-05 12:20:18 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2022-09-12 10:16:52 +0200 |
| commit | 4caf4b5ef315a8e902471fe8797e504967f66a6b (patch) | |
| tree | 9cbd5b9b9aa511bfc5b12318e20887389be54ec4 /gcc | |
| parent | 517817a434f0c15a355cb1e9ab3aaea14a54e9a6 (diff) | |
| download | gcc-4caf4b5ef315a8e902471fe8797e504967f66a6b.zip gcc-4caf4b5ef315a8e902471fe8797e504967f66a6b.tar.gz gcc-4caf4b5ef315a8e902471fe8797e504967f66a6b.tar.bz2 | |
[Ada] Accept explicit SPARK_Mode Auto as configuration pragma
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.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/sem_prag.adb | 17 | ||||
| -rw-r--r-- | gcc/ada/snames.ads-tmpl | 1 |
2 files changed, 15 insertions, 3 deletions
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 509a04e..67d00d2 100644 --- 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 index 79557e7..8f71ad9 100644 --- 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 + $; |