===================================================================
@@ -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);
===================================================================
@@ -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.
===================================================================
@@ -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
===================================================================
@@ -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
===================================================================
@@ -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