* [Ada] Spurious error on SPARK_Mode in generic package instantiation
@ 2015-10-16 13:52 Arnaud Charlet
0 siblings, 0 replies; only message in thread
From: Arnaud Charlet @ 2015-10-16 13:52 UTC (permalink / raw)
To: gcc-patches; +Cc: Hristian Kirtchev
[-- Attachment #1: Type: text/plain, Size: 1954 bytes --]
This patch modifies the generic instantiation to ensure that a context with a
missing SPARK_Mode annotation is treated as having SPARK_Mode set to Off. This
ensures that the following SPARK UG rule 9.4.1
Code where SPARK_Mode is Off shall not enclose code where Spark_Mode is
On. However, if an instance of a generic unit is enclosed by code where
SPARK_Mode is Off and if any SPARK_Mode specifications occur within the
generic unit, then the corresponding SPARK_Mode specifications occurring
within the instance have no semantic effect.
does not lead to spurious errors.
------------
-- Source --
------------
-- gen_pack.ads
generic
type T is private;
package Gen_Pack with SPARK_Mode is
procedure Force_Body;
generic
type Inner_T is private;
package Inner_Gen_Pack with SPARK_Mode => Off is
type Inner_T_Ptr is access Inner_T;
end Inner_Gen_Pack;
package Inner_Inst is new Inner_Gen_Pack (Inner_T => T);
type T_Ptr is private;
private
pragma SPARK_Mode (Off);
type T_Ptr is new Inner_Inst.Inner_T_Ptr;
end Gen_Pack;
-- gen_pack.adb
package body Gen_Pack with SPARK_Mode => Off is
procedure Force_Body is begin null; end Force_Body;
end Gen_Pack;
-- main.adb
with Gen_Pack;
procedure Main is
package Inst is new Gen_Pack (T => Integer);
begin
null;
end Main;
-----------------
-- Compilation --
-----------------
$ gcc -c main.adb
Tested on x86_64-pc-linux-gnu, committed on trunk
2015-10-16 Hristian Kirtchev <kirtchev@adacore.com>
* sem_ch12.adb (Analyze_Package_Instantiation):
Treat a missing SPARK_Mode annotation as having mode "Off".
(Analyze_Subprogram_Instantiation): Treat a missing SPARK_Mode
annotation as having mode "Off".
(Instantiate_Package_Body): Code
reformatting. Treat a missing SPARK_Mode annotation as having mode
"Off".
(Instantiate_Subprogram_Body): Code reformatting. Treat
a missing SPARK_Mode annotation as having mode "Off".
[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 5130 bytes --]
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb (revision 228884)
+++ sem_ch12.adb (working copy)
@@ -3723,11 +3723,12 @@
goto Leave;
else
- -- If the context of the instance is subject to SPARK_Mode "off",
- -- set the global flag which signals Analyze_Pragma to ignore all
- -- SPARK_Mode pragmas within the instance.
+ -- If the context of the instance is subject to SPARK_Mode "off" or
+ -- the annotation is altogether missing, set the global flag which
+ -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
+ -- the instance.
- if SPARK_Mode = Off then
+ if SPARK_Mode /= On then
Ignore_Pragma_SPARK_Mode := True;
end if;
@@ -5098,11 +5099,12 @@
Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit);
else
- -- If the context of the instance is subject to SPARK_Mode "off",
- -- set the global flag which signals Analyze_Pragma to ignore all
- -- SPARK_Mode pragmas within the instance.
+ -- If the context of the instance is subject to SPARK_Mode "off" or
+ -- the annotation is altogether missing, set the global flag which
+ -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
+ -- the instance.
- if SPARK_Mode = Off then
+ if SPARK_Mode /= On then
Ignore_Pragma_SPARK_Mode := True;
end if;
@@ -10632,18 +10634,19 @@
Act_Spec : constant Node_Id := Specification (Act_Decl);
Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Spec);
+ Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
+ Save_Style_Check : constant Boolean := Style_Check;
+
+ Act_Body : Node_Id;
+ Act_Body_Id : Entity_Id;
Act_Body_Name : Node_Id;
Gen_Body : Node_Id;
Gen_Body_Id : Node_Id;
- Act_Body : Node_Id;
- Act_Body_Id : Entity_Id;
+ Par_Ent : Entity_Id := Empty;
+ Par_Vis : Boolean := False;
Parent_Installed : Boolean := False;
- Save_Style_Check : constant Boolean := Style_Check;
- Par_Ent : Entity_Id := Empty;
- Par_Vis : Boolean := False;
-
Vis_Prims_List : Elist_Id := No_Elist;
-- List of primitives made temporarily visible in the instantiation
-- to match the visibility of the formal type
@@ -10783,8 +10786,17 @@
if Present (Gen_Body_Id) then
Save_Env (Gen_Unit, Act_Decl_Id);
Style_Check := False;
+
+ -- If the context of the instance is subject to SPARK_Mode "off" or
+ -- the annotation is altogether missing, set the global flag which
+ -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
+ -- the instance.
+
+ if SPARK_Mode /= On then
+ Ignore_Pragma_SPARK_Mode := True;
+ end if;
+
Current_Sem_Unit := Body_Info.Current_Sem_Unit;
-
Gen_Body := Unit_Declaration_Node (Gen_Body_Id);
Create_Instantiation_Source
@@ -10943,6 +10955,7 @@
end if;
Restore_Env;
+ Ignore_Pragma_SPARK_Mode := Save_IPSM;
Style_Check := Save_Style_Check;
-- If we have no body, and the unit requires a body, then complain. This
@@ -11019,6 +11032,7 @@
Pack_Id : constant Entity_Id :=
Defining_Unit_Name (Parent (Act_Decl));
+ Saved_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
Saved_Style_Check : constant Boolean := Style_Check;
Saved_Warnings : constant Warning_Record := Save_Warnings;
@@ -11104,6 +11118,16 @@
Save_Env (Gen_Unit, Anon_Id);
Style_Check := False;
+
+ -- If the context of the instance is subject to SPARK_Mode "off" or
+ -- the annotation is altogether missing, set the global flag which
+ -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
+ -- the instance.
+
+ if SPARK_Mode /= On then
+ Ignore_Pragma_SPARK_Mode := True;
+ end if;
+
Current_Sem_Unit := Body_Info.Current_Sem_Unit;
Create_Instantiation_Source
(Inst_Node,
@@ -11203,6 +11227,7 @@
end if;
Restore_Env;
+ Ignore_Pragma_SPARK_Mode := Saved_IPSM;
Style_Check := Saved_Style_Check;
Restore_Warnings (Saved_Warnings);
@@ -11268,9 +11293,10 @@
(Make_Simple_Return_Statement (Loc, Ret_Expr))));
end if;
- Pack_Body := Make_Package_Body (Loc,
- Defining_Unit_Name => New_Copy (Pack_Id),
- Declarations => New_List (Act_Body));
+ Pack_Body :=
+ Make_Package_Body (Loc,
+ Defining_Unit_Name => New_Copy (Pack_Id),
+ Declarations => New_List (Act_Body));
Insert_After (Inst_Node, Pack_Body);
Set_Corresponding_Spec (Pack_Body, Pack_Id);
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2015-10-16 13:50 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2015-10-16 13:52 [Ada] Spurious error on SPARK_Mode in generic package instantiation Arnaud Charlet
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).