[Ada] Check for attempt to bind GNATprove files

[Arnaud Charlet]

If one or more objects is compiled in GNATprove mode (either by using
GNATprove directly, or by using -gnatd.F), then the ALI file is marked
and gnatbind will exit with a message as shown here. Given:

     1. procedure linkdf is
     2. begin
     3.    null;
     4. end;

If we first compile this with

  gcc -c linkdf.adb -gnatd.F

then we try to do a gnatmake, we get

error: one or more files compiled in GNATprove mode
gnatmake: *** bind failed.

Previously this was not detected and the linker bombed
with peculiar error messages.

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

2014-10-10  Robert Dewar  <dewar@adacore.com>

	* ali.adb (Scan_ALI): Read and process new GP flag on ALI P line.
	* ali.ads (GNATprove_Mode): New component in ALI table.
	(GNATprove_Mode_Specified): New global.
	* gnatbind.adb (Gnatbind): Give fatal error if any file compiled
	in GNATProve mode.
	* lib-writ.ads, lib-writ.adb (GP): New flag on P line for
	GNATProve_Mode.

-------------- next part --------------
Index: lib-writ.adb
===================================================================
--- lib-writ.adb	(revision 216063)
+++ lib-writ.adb	(working copy)
@@ -1153,6 +1153,10 @@
          end if;
       end if;
 
+      if GNATprove_Mode then
+         Write_Info_Str (" GP");
+      end if;
+
       if Partition_Elaboration_Policy /= ' ' then
          Write_Info_Str  (" E");
          Write_Info_Char (Partition_Elaboration_Policy);
Index: lib-writ.ads
===================================================================
--- lib-writ.ads	(revision 216063)
+++ lib-writ.ads	(working copy)
@@ -192,6 +192,9 @@
    --              the units in this file, where x is the first character
    --              (upper case) of the policy name (e.g. 'C' for Concurrent).
 
+   --         GP   Set if this compilation was done in GNATprove mode, either
+   --              from direct use of GNATprove, or from use of -gnatdF.
+
    --         Lx   A valid Locking_Policy pragma applies to all the units in
    --              this file, where x is the first character (upper case) of
    --              the policy name (e.g. 'C' for Ceiling_Locking).
@@ -200,7 +203,9 @@
    --              were not compiled to produce an object. This can occur as a
    --              result of the use of -gnatc, or if no object can be produced
    --              (e.g. when a package spec is compiled instead of the body,
-   --              or a subunit on its own).
+   --              or a subunit on its own). Note that in GNATprove mode, we
+   --              do produce an object. The object is not suitable for binding
+   --              and linking, but we do not set NO, instead we set GP.
 
    --         NR   No_Run_Time. Indicates that a pragma No_Run_Time applies
    --              to all units in the file.
Index: ali.adb
===================================================================
--- ali.adb	(revision 216063)
+++ ali.adb	(working copy)
@@ -111,6 +111,7 @@
       Locking_Policy_Specified               := ' ';
       No_Normalize_Scalars_Specified         := False;
       No_Object_Specified                    := False;
+      GNATprove_Mode_Specified               := False;
       Normalize_Scalars_Specified            := False;
       Partition_Elaboration_Policy_Specified := ' ';
       Queuing_Policy_Specified               := ' ';
@@ -875,6 +876,7 @@
         First_Sdep                   => No_Sdep_Id,
         First_Specific_Dispatching   => Specific_Dispatching.Last + 1,
         First_Unit                   => No_Unit_Id,
+        GNATprove_Mode               => False,
         Last_Interrupt_State         => Interrupt_States.Last,
         Last_Sdep                    => No_Sdep_Id,
         Last_Specific_Dispatching    => Specific_Dispatching.Last,
@@ -1089,6 +1091,13 @@
                ALIs.Table (Id).Partition_Elaboration_Policy :=
                  Partition_Elaboration_Policy_Specified;
 
+            --  Processing for GP
+
+            elsif C = 'G' then
+               Checkc ('P');
+               GNATprove_Mode_Specified := True;
+               ALIs.Table (Id).GNATprove_Mode := True;
+
             --  Processing for Lx
 
             elsif C = 'L' then
Index: ali.ads
===================================================================
--- ali.ads	(revision 216063)
+++ ali.ads	(working copy)
@@ -176,6 +176,11 @@
       --  always be set as well in this case. Not set if 'P' appears in
       --  Ignore_Lines.
 
+      GNATprove_Mode : Boolean;
+      --  Set to True if ALI and object file produced in GNATprove_Mode as
+      --  signalled by GP appearing on the P line. Not set if 'P' appears in
+      --  Ignore_Lines.
+
       No_Object : Boolean;
       --  Set to True if no object file generated. Not set if 'P' appears in
       --  Ignore_Lines.
@@ -465,6 +470,9 @@
    --  Set to False by Initialize_ALI. Set to True if Scan_ALI reads
    --  a unit for which dynamic elaboration checking is enabled.
 
+   GNATprove_Mode_Specified : Boolean := False;
+   --  Set to True if an ali file was produced in GNATprove mode.
+
    Initialize_Scalars_Used : Boolean := False;
    --  Set True if an ali file contains the Initialize_Scalars flag
 
Index: gnatbind.adb
===================================================================
--- gnatbind.adb	(revision 216063)
+++ gnatbind.adb	(working copy)
@@ -776,6 +776,13 @@
          raise Unrecoverable_Error;
       end if;
 
+      --  Quit with message if we had a GNATprove file
+
+      if GNATprove_Mode_Specified then
+         Error_Msg ("one or more files compiled in GNATprove mode");
+         raise Unrecoverable_Error;
+      end if;
+
       --  Output list of ALI files in closure
 
       if Output_ALI_List then