[Ada] Analyze instance with SPARK_Mode at point of instantiation

Arnaud Charlet charlet@adacore.com
Wed Jan 29 15:22:00 GMT 2014


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  <moy@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.

-------------- next part --------------
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 :=


More information about the Gcc-patches mailing list