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 <de...@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.
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;
