[Ada] Turn off SPARK_Mode for generated subprograms

[Arnaud Charlet]

SPARK_Mode should always be off for internally generated subprograms
When the following is compiled with -gnatdt:

     1. package IntSPARK is
     2.    pragma SPARK_Mode (ON);
     3.    type R is record
     4.       X : Integer := 4;
     5.       Y : Integer := 5;
     6.    end record;
     7. end;

The resulting file should have just one instance of the SPARK_Pragma
field being set (in the entity for the package), it should not be
set in the spec of body of the generated initialization procedure.

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

2014-01-24  Robert Dewar  <de...@adacore.com>

        * sem_ch6.adb (Analyze_Subprogram_Body_Helper): SPARK_Mode OFF
        for generated subprograms.
        (Analyze_Subprogram_Specification): Ditto.


Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 207026)
+++ sem_ch6.adb (working copy)
@@ -2995,9 +2995,17 @@
 
             Push_Scope (Spec_Id);
 
-            --  Set SPARK_Mode from spec if spec had a SPARK_Mode pragma
+            --  Set SPARK_Mode
 
-            if Present (SPARK_Pragma (Spec_Id))
+            --  For internally generated subprogram, always off
+
+            if not Comes_From_Source (Spec_Id) then
+               SPARK_Mode := Off;
+               SPARK_Mode_Pragma := Empty;
+
+            --  Inherited from spec
+
+            elsif Present (SPARK_Pragma (Spec_Id))
               and then not SPARK_Pragma_Inherited (Spec_Id)
             then
                SPARK_Mode_Pragma := SPARK_Pragma (Spec_Id);
@@ -3058,12 +3066,19 @@
               (Body_Id, Body_Id, 'b', Set_Ref => False, Force => True);
             Install_Formals (Body_Id);
 
-            --  Set SPARK_Mode from context
+            Push_Scope (Body_Id);
 
-            Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
-            Set_SPARK_Pragma_Inherited (Body_Id, True);
+            --  Set SPARK_Mode from context or OFF for internal routine
 
-            Push_Scope (Body_Id);
+            if Comes_From_Source (Body_Id) then
+               Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+               Set_SPARK_Pragma_Inherited (Body_Id, True);
+            else
+               Set_SPARK_Pragma (Body_Id, Empty);
+               Set_SPARK_Pragma_Inherited (Body_Id, False);
+               SPARK_Mode := Off;
+               SPARK_Mode_Pragma := Empty;
+            end if;
          end if;
 
          --  For stubs and bodies with no previous spec, generate references to
@@ -3609,9 +3624,17 @@
 
       Generate_Definition (Designator);
 
-      Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
-      Set_SPARK_Pragma_Inherited (Designator, True);
+      --  Set SPARK mode, always off for internal routines, otherwise set
+      --  from current context (may be overwritten later with explicit pragma)
 
+      if Comes_From_Source (Designator) then
+         Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
+         Set_SPARK_Pragma_Inherited (Designator, True);
+      else
+         Set_SPARK_Pragma (Designator, Empty);
+         Set_SPARK_Pragma_Inherited (Designator, False);
+      end if;
+
       if Debug_Flag_C then
          Write_Str ("==> subprogram spec ");
          Write_Name (Chars (Designator));