[Ada] Fix problem in save/restore of SPARK_Mode

Arnaud Charlet charlet@adacore.com
Thu Jan 23 17:04:00 GMT 2014


The previous checkin for saving and restoring SPARK_Mode was not
complete, and as a result the SPARK_Mode_Pragma was not properly
set in some cases. The following test program:

     1. package Pack_Size1 is
     2.    pragma SPARK_Mode (On);
     3.    procedure P;
     4. end Pack_Size1;

     1. package body Pack_Size1 is
     2.    type T_Bit is range 0 .. 1;
     3.    type T_Bit_Buffer is
     4.      array (Natural range <>) of T_Bit;
     5.    pragma Pack (T_Bit_Buffer);
     6.    procedure P is begin null; end;
     7. end Pack_Size1;

Should set SPARK_Mode_Pragma in the body node procedure P, but
failed to do so (because Rtsfind was clobbering SPARK_Mode_Pragma).
An easy test is

   gcc -c pack_size1.adb -gnatdt >log
   grep "SPARK_Pragma " log | wc -l

this should output 3, prior to this patch it output 1

Tested on x86_64-pc-linux-gnu, committed on trunk

2014-01-23  Robert Dewar  <dewar@adacore.com>

	* opt.adb (Save_Opt_Config_Switches): Save SPARK_Mode_Pragma
	(Restore_Opt_Config_Switches): Restore SPARK_Mode_Pragma.
	* sem.adb (Semantics): Remove save/restore of
	SPARK_Mode[_Pragma]. Not needed since already done in
	Save/Restore_Opt_Config_Switches.

-------------- next part --------------
Index: sem.adb
===================================================================
--- sem.adb	(revision 206990)
+++ sem.adb	(working copy)
@@ -1311,8 +1311,6 @@
       S_Inside_A_Generic  : constant Boolean          := Inside_A_Generic;
       S_Outer_Gen_Scope   : constant Entity_Id        := Outer_Generic_Scope;
       S_Style_Check       : constant Boolean          := Style_Check;
-      S_SPARK_Mode        : constant SPARK_Mode_Type  := SPARK_Mode;
-      S_SPARK_Mode_Pragma : constant Node_Id          := SPARK_Mode_Pragma;
 
       Generic_Main : constant Boolean :=
                        Nkind (Unit (Cunit (Main_Unit)))
@@ -1512,8 +1510,6 @@
       Inside_A_Generic     := S_Inside_A_Generic;
       Outer_Generic_Scope  := S_Outer_Gen_Scope;
       Style_Check          := S_Style_Check;
-      SPARK_Mode           := S_SPARK_Mode;
-      SPARK_Mode_Pragma    := S_SPARK_Mode_Pragma;
 
       Restore_Opt_Config_Switches (Save_Config_Switches);
 
Index: opt.adb
===================================================================
--- opt.adb	(revision 206990)
+++ opt.adb	(working copy)
@@ -100,6 +100,7 @@
       Polling_Required               := Save.Polling_Required;
       Short_Descriptors              := Save.Short_Descriptors;
       SPARK_Mode                     := Save.SPARK_Mode;
+      SPARK_Mode_Pragma              := Save.SPARK_Mode_Pragma;
       Use_VADS_Size                  := Save.Use_VADS_Size;
 
       --  Update consistently the value of Init_Or_Norm_Scalars. The value of
@@ -137,6 +138,7 @@
       Save.Polling_Required               := Polling_Required;
       Save.Short_Descriptors              := Short_Descriptors;
       Save.SPARK_Mode                     := SPARK_Mode;
+      Save.SPARK_Mode_Pragma              := SPARK_Mode_Pragma;
       Save.Use_VADS_Size                  := Use_VADS_Size;
    end Save_Opt_Config_Switches;
 


More information about the Gcc-patches mailing list