A generic instance should be analyzed with the value of SPARK_Mode
defined at the point of instantiation. Now, the following code
compiles without errors:
$ gcc -c -gnatec=test.adc pinst.adb
-- test.adc
1. pragma SPARK_Mode (On);
-- pinst.ads
1. with Ada.Containers.Formal_Doubly_Linked_Lists;
2. package Pinst is
3. function Eq (X, Y : Integer) return Boolean is (X = Y);
4. package My_Lists is new
Ada.Containers.Formal_Doubly_Linked_Lists (Integer, Eq);
5. procedure P;
6. end Pinst;
-- pinst.adb
1. package body Pinst is
2. procedure P is begin null; end;
3. end Pinst;
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-01-29 Yannick Moy <m...@adacore.com>
* inline.ads (Pending_Body_Info): Add SPARK_Mode and
SPARK_Mode_Pragma components to be able to analyze generic
instance.
* sem_ch12.adb (Analyze_Package_Instantiation,
Inline_Instance_Body, Need_Subprogram_Instance_Body,
Load_Parent_Of_Generic): Pass in SPARK_Mode from instantiation
for future analysis of the instance.
(Instantiate_Package_Body,
Instantiate_Subprogram_Body, Set_Instance_Inv): Set SPARK_Mode
from instantiation to analyze the instance.
Index: inline.ads
===================================================================
--- inline.ads (revision 207241)
+++ inline.ads (working copy)
@@ -96,6 +96,11 @@
Warnings : Warning_Record;
-- Capture values of warning flags
+
+ SPARK_Mode : SPARK_Mode_Type;
+ SPARK_Mode_Pragma : Node_Id;
+ -- SPARK_Mode for an instance is the one applicable at the point of
+ -- instantiation.
end record;
package Pending_Instantiations is new Table.Table (
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb (revision 207241)
+++ sem_ch12.adb (working copy)
@@ -3899,7 +3899,9 @@
Local_Suppress_Stack_Top => Local_Suppress_Stack_Top,
Version => Ada_Version,
Version_Pragma => Ada_Version_Pragma,
- Warnings => Save_Warnings));
+ Warnings => Save_Warnings,
+ SPARK_Mode => SPARK_Mode,
+ SPARK_Mode_Pragma => SPARK_Mode_Pragma));
end if;
end if;
@@ -4245,7 +4247,9 @@
Local_Suppress_Stack_Top => Local_Suppress_Stack_Top,
Version => Ada_Version,
Version_Pragma => Ada_Version_Pragma,
- Warnings => Save_Warnings)),
+ Warnings => Save_Warnings,
+ SPARK_Mode => SPARK_Mode,
+ SPARK_Mode_Pragma => SPARK_Mode_Pragma)),
Inlined_Body => True);
Pop_Scope;
@@ -4363,7 +4367,9 @@
Local_Suppress_Stack_Top => Local_Suppress_Stack_Top,
Version => Ada_Version,
Version_Pragma => Ada_Version_Pragma,
- Warnings => Save_Warnings)),
+ Warnings => Save_Warnings,
+ SPARK_Mode => SPARK_Mode,
+ SPARK_Mode_Pragma => SPARK_Mode_Pragma)),
Inlined_Body => True);
end if;
end Inline_Instance_Body;
@@ -4421,7 +4427,9 @@
Local_Suppress_Stack_Top => Local_Suppress_Stack_Top,
Version => Ada_Version,
Version_Pragma => Ada_Version_Pragma,
- Warnings => Save_Warnings));
+ Warnings => Save_Warnings,
+ SPARK_Mode => SPARK_Mode,
+ SPARK_Mode_Pragma => SPARK_Mode_Pragma));
return True;
-- Here if not inlined, or we ignore the inlining
@@ -9913,6 +9921,8 @@
Opt.Ada_Version := Body_Info.Version;
Opt.Ada_Version_Pragma := Body_Info.Version_Pragma;
Restore_Warnings (Body_Info.Warnings);
+ Opt.SPARK_Mode := Body_Info.SPARK_Mode;
+ Opt.SPARK_Mode_Pragma := Body_Info.SPARK_Mode_Pragma;
if No (Gen_Body_Id) then
Load_Parent_Of_Generic
@@ -10203,6 +10213,8 @@
Opt.Ada_Version := Body_Info.Version;
Opt.Ada_Version_Pragma := Body_Info.Version_Pragma;
Restore_Warnings (Body_Info.Warnings);
+ Opt.SPARK_Mode := Body_Info.SPARK_Mode;
+ Opt.SPARK_Mode_Pragma := Body_Info.SPARK_Mode_Pragma;
if No (Gen_Body_Id) then
@@ -12091,7 +12103,9 @@
Local_Suppress_Stack_Top,
Version => Ada_Version,
Version_Pragma => Ada_Version_Pragma,
- Warnings => Save_Warnings);
+ Warnings => Save_Warnings,
+ SPARK_Mode => SPARK_Mode,
+ SPARK_Mode_Pragma => SPARK_Mode_Pragma);
-- Package instance
@@ -12133,7 +12147,9 @@
Local_Suppress_Stack_Top => Local_Suppress_Stack_Top,
Version => Ada_Version,
Version_Pragma => Ada_Version_Pragma,
- Warnings => Save_Warnings)),
+ Warnings => Save_Warnings,
+ SPARK_Mode => SPARK_Mode,
+ SPARK_Mode_Pragma => SPARK_Mode_Pragma)),
Body_Optional => Body_Optional);
end;
end if;
@@ -13799,7 +13815,9 @@
(Gen_Unit : Entity_Id;
Act_Unit : Entity_Id)
is
- Assertion_Status : constant Boolean := Assertions_Enabled;
+ Assertion_Status : constant Boolean := Assertions_Enabled;
+ Save_SPARK_Mode : constant SPARK_Mode_Type := SPARK_Mode;
+ Save_SPARK_Mode_Pragma : constant Node_Id := SPARK_Mode_Pragma;
begin
-- Regardless of the current mode, predefined units are analyzed in the
@@ -13822,6 +13840,12 @@
if Ada_Version >= Ada_2012 then
Assertions_Enabled := Assertion_Status;
end if;
+
+ -- SPARK_Mode for an instance is the one applicable at the point of
+ -- instantiation.
+
+ SPARK_Mode := Save_SPARK_Mode;
+ SPARK_Mode_Pragma := Save_SPARK_Mode_Pragma;
end if;
Current_Instantiated_Parent :=
