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