+2017-11-09 Arnaud Charlet <charlet@adacore.com>
+
+ * gnat1drv.adb (Adjust_Global_Switches): Suppress warnings in codepeer
+ mode here unless -gnateC is specified.
+ * switch-c.adb (Scan_Front_End_Switches): Do not suppress warnings with
+ -gnatC here.
+
+2017-11-09 Piotr Trojanek <trojanek@adacore.com>
+
+ * lib-writ.adb (Write_ALI): Remove processing of the frontend xrefs as
+ part of the ALI writing; they are now processed directly from memory
+ when requested by the backend.
+ * lib-xref.ads (Collect_SPARK_Xrefs): Remove.
+ (Iterate_SPARK_Xrefs): New routine for iterating over frontend xrefs.
+ * lib-xref-spark_specific.adb (Traverse_Compilation_Unit): Remove.
+ (Add_SPARK_File): Remove.
+ (Add_SPARK_Xref): Refactored from removed code; filters xref entries
+ that are trivially uninteresting to the SPARK backend.
+ * spark_xrefs.ads: Remove code that is no longer needed.
+ * spark_xrefs.adb (dspark): Adapt to use Iterate_SPARK_Xrefs.
+
+2017-11-09 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_elab.adb: Update the documentation on adding a new elaboration
+ schenario. Add new hash table Recorded_Top_Level_Scenarios.
+ (Is_Check_Emitting_Scenario): Removed.
+ (Is_Recorded_Top_Level_Scenario): New routine.
+ (Kill_Elaboration_Scenario): Reimplemented.
+ (Record_Elaboration_Scenario): Mark the scenario as recorded.
+ (Set_Is_Recorded_Top_Level_Scenario): New routine.
+ (Update_Elaboration_Scenario): Reimplemented.
+ * sinfo.adb (Is_Recorded_Scenario): Removed.
+ (Set_Is_Recorded_Scenario): Removed.
+ * sinfo.ads: Remove attribute Is_Recorded_Scenario along with
+ occurrences in nodes.
+ (Is_Recorded_Scenario): Removed along with pragma Inline.
+ (Set_Is_Recorded_Scenario): Removed along with pragma Inline.
+
+2017-11-09 Piotr Trojanek <trojanek@adacore.com>
+
+ * sem_prag.adb (Analyze_Part_Of): Change "designate" to "denote" in
+ error message.
+
+2017-11-09 Justin Squirek <squirek@adacore.com>
+
+ * sem_res.adb (Resolve_Allocator): Add warning messages corresponding
+ to the allocation of an anonymous access-to-controlled object.
+
2017-11-09 Jerome Lambourg <lambourg@adacore.com>
* sigtramp-qnx.c: Fix obvious typo.
Relaxed_RM_Semantics := True;
+ if not Generate_CodePeer_Messages then
+ -- Suppress compiler warnings by default when generating SCIL for
+ -- CodePeer, except when combined with -gnateC where we do want
+ -- to emit GNAT warnings.
+
+ Warning_Mode := Suppress;
+ end if;
+
-- Disable all simple value propagation. This is an optimization
-- which is valuable for code optimization, and also for generation
-- of compiler warnings, but these are being turned off by default,
SCO_Output;
end if;
- -- Output SPARK cross-reference information if needed
-
- if Opt.Xref_Active and then GNATprove_Mode then
- SPARK_Specific.Collect_SPARK_Xrefs (Sdep_Table => Sdep_Table,
- Num_Sdep => Num_Sdep);
- end if;
-
-- Output final blank line and we are done. This final blank line is
-- probably junk, but we don't feel like making an incompatible change.
with Nmake; use Nmake;
with SPARK_Xrefs; use SPARK_Xrefs;
-with GNAT.HTable;
-
separate (Lib.Xref)
package body SPARK_Specific is
's' => True,
others => False);
- type Entity_Hashed_Range is range 0 .. 255;
- -- Size of hash table headers
-
---------------------
-- Local Variables --
---------------------
-- "Heap". These references are added to the regular references when
-- computing SPARK cross-references.
- -----------------------
- -- Local Subprograms --
- -----------------------
-
- procedure Add_SPARK_File (Uspec, Ubody : Unit_Number_Type; Dspec : Nat);
- -- Add file and corresponding scopes for unit to the tables
- -- SPARK_File_Table and SPARK_Scope_Table. When two units are present
- -- for the same compilation unit, as it happens for library-level
- -- instantiations of generics, then Ubody is the number of the body
- -- unit; otherwise it is No_Unit.
-
- procedure Add_SPARK_Xrefs;
- -- Filter table Xrefs to add all references used in SPARK to the table
- -- SPARK_Xref_Table.
-
- function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range;
- -- Hash function for hash table
-
- generic
- with procedure Process (N : Node_Id) is <>;
- procedure Traverse_Compilation_Unit (CU : Node_Id);
- -- Call Process on all declarations within compilation unit CU. Bodies
- -- of stubs are also traversed, but generic declarations are ignored.
-
- --------------------
- -- Add_SPARK_File --
- --------------------
-
- procedure Add_SPARK_File (Uspec, Ubody : Unit_Number_Type; Dspec : Nat) is
- File : constant Source_File_Index := Source_Index (Uspec);
- From : constant Scope_Index := SPARK_Scope_Table.Last + 1;
-
- Scope_Id : Pos := 1;
-
- procedure Add_SPARK_Scope (N : Node_Id);
- -- Add scope N to the table SPARK_Scope_Table
-
- procedure Detect_And_Add_SPARK_Scope (N : Node_Id);
- -- Call Add_SPARK_Scope on scopes
-
- ---------------------
- -- Add_SPARK_Scope --
- ---------------------
-
- procedure Add_SPARK_Scope (N : Node_Id) is
- E : constant Entity_Id := Defining_Entity (N);
-
- begin
- -- Ignore scopes without a proper location
-
- if Sloc (N) = No_Location then
- return;
- end if;
-
- case Ekind (E) is
- when E_Entry
- | E_Entry_Family
- | E_Function
- | E_Generic_Function
- | E_Generic_Package
- | E_Generic_Procedure
- | E_Package
- | E_Package_Body
- | E_Procedure
- | E_Protected_Body
- | E_Protected_Type
- | E_Task_Body
- | E_Task_Type
- | E_Subprogram_Body
- =>
- null;
-
- when E_Void =>
-
- -- Compilation of prj-attr.adb with -gnatn creates a node with
- -- entity E_Void for the package defined at a-charac.ads16:13.
- -- ??? TBD
-
- return;
-
- when others =>
- raise Program_Error;
- end case;
-
- -- File_Num and Scope_Num are filled later. From_Xref and To_Xref
- -- are filled even later, but are initialized to represent an empty
- -- range.
-
- SPARK_Scope_Table.Append
- ((Entity => E,
- Scope_Num => Scope_Id,
- From_Xref => 1,
- To_Xref => 0));
-
- Scope_Id := Scope_Id + 1;
- end Add_SPARK_Scope;
-
- --------------------------------
- -- Detect_And_Add_SPARK_Scope --
- --------------------------------
-
- procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
- begin
- -- Entries
-
- if Nkind_In (N, N_Entry_Body, N_Entry_Declaration)
-
- -- Packages
-
- or else Nkind_In (N, N_Package_Body,
- N_Package_Declaration)
- -- Protected units
-
- or else Nkind_In (N, N_Protected_Body,
- N_Protected_Type_Declaration)
-
- -- Subprograms
-
- or else Nkind_In (N, N_Subprogram_Body,
- N_Subprogram_Declaration)
-
- -- Task units
-
- or else Nkind_In (N, N_Task_Body,
- N_Task_Type_Declaration)
- then
- Add_SPARK_Scope (N);
- end if;
- end Detect_And_Add_SPARK_Scope;
-
- procedure Traverse_Scopes is new
- Traverse_Compilation_Unit (Detect_And_Add_SPARK_Scope);
-
- -- Start of processing for Add_SPARK_File
-
- begin
- -- Source file could be inexistant as a result of an error, if option
- -- gnatQ is used.
-
- if File <= No_Source_File then
- return;
- end if;
-
- -- Subunits are traversed as part of the top-level unit to which they
- -- belong.
-
- if Nkind (Unit (Cunit (Uspec))) = N_Subunit then
- return;
- end if;
-
- Traverse_Scopes (CU => Cunit (Uspec));
-
- -- When two units are present for the same compilation unit, as it
- -- happens for library-level instantiations of generics, then add all
- -- scopes to the same SPARK file.
-
- if Ubody /= No_Unit then
- Traverse_Scopes (CU => Cunit (Ubody));
- end if;
-
- SPARK_File_Table.Append (
- (File_Num => Dspec,
- From_Scope => From,
- To_Scope => SPARK_Scope_Table.Last));
- end Add_SPARK_File;
-
- ---------------------
- -- Add_SPARK_Xrefs --
- ---------------------
-
- procedure Add_SPARK_Xrefs is
- function Entity_Of_Scope (S : Scope_Index) return Entity_Id;
- -- Return the entity which maps to the input scope index
+ -------------------------
+ -- Iterate_SPARK_Xrefs --
+ -------------------------
- function Get_Scope_Num (E : Entity_Id) return Nat;
- -- Return the scope number associated with the entity E
+ procedure Iterate_SPARK_Xrefs is
- function Is_Future_Scope_Entity
- (E : Entity_Id;
- S : Scope_Index) return Boolean;
- -- Check whether entity E is in SPARK_Scope_Table at index S or higher
+ procedure Add_SPARK_Xref (Index : Int; Xref : Xref_Entry);
function Is_SPARK_Reference
(E : Entity_Id;
-- Return whether the entity or reference scope meets requirements for
-- being a SPARK scope.
- function Lt (Op1 : Natural; Op2 : Natural) return Boolean;
- -- Comparison function for Sort call
-
- procedure Move (From : Natural; To : Natural);
- -- Move procedure for Sort call
-
- procedure Set_Scope_Num (E : Entity_Id; Num : Nat);
- -- Associate entity E with the scope number Num
-
- procedure Update_Scope_Range
- (S : Scope_Index;
- From : Xref_Index;
- To : Xref_Index);
- -- Update the scope which maps to S with the new range From .. To
-
- package Sorting is new GNAT.Heap_Sort_G (Move, Lt);
-
- No_Scope : constant Nat := 0;
- -- Initial scope counter
-
- package Scopes is new GNAT.HTable.Simple_HTable
- (Header_Num => Entity_Hashed_Range,
- Element => Nat,
- No_Element => No_Scope,
- Key => Entity_Id,
- Hash => Entity_Hash,
- Equal => "=");
- -- Package used to build a correspondence between entities and scope
- -- numbers used in SPARK cross references.
-
- Nrefs : Nat := Xrefs.Last;
- -- Number of references in table. This value may get reset (reduced)
- -- when we eliminate duplicate reference entries as well as references
- -- not suitable for local cross-references.
-
- Nrefs_Add : constant Nat := Drefs.Last;
- -- Number of additional references which correspond to dereferences in
- -- the source code.
-
- Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat;
- -- This array contains numbers of references in the Xrefs table. This
- -- list is sorted in output order. The extra 0'th entry is convenient
- -- for the call to sort. When we sort the table, we move the indices in
- -- Rnums around, but we do not move the original table entries.
-
- ---------------------
- -- Entity_Of_Scope --
- ---------------------
-
- function Entity_Of_Scope (S : Scope_Index) return Entity_Id is
- begin
- return SPARK_Scope_Table.Table (S).Entity;
- end Entity_Of_Scope;
-
- -------------------
- -- Get_Scope_Num --
- -------------------
-
- function Get_Scope_Num (E : Entity_Id) return Nat renames Scopes.Get;
-
- ----------------------------
- -- Is_Future_Scope_Entity --
- ----------------------------
-
- function Is_Future_Scope_Entity
- (E : Entity_Id;
- S : Scope_Index) return Boolean
- is
- function Is_Past_Scope_Entity return Boolean;
- -- Check whether entity E is in SPARK_Scope_Table at index strictly
- -- lower than S.
-
- --------------------------
- -- Is_Past_Scope_Entity --
- --------------------------
-
- function Is_Past_Scope_Entity return Boolean is
- begin
- for Index in SPARK_Scope_Table.First .. S - 1 loop
- if SPARK_Scope_Table.Table (Index).Entity = E then
- return True;
- end if;
- end loop;
-
- return False;
- end Is_Past_Scope_Entity;
-
- -- Start of processing for Is_Future_Scope_Entity
+ --------------------
+ -- Add_SPARK_Xref --
+ --------------------
+ procedure Add_SPARK_Xref (Index : Int; Xref : Xref_Entry) is
+ Ref : Xref_Key renames Xref.Key;
begin
- for Index in S .. SPARK_Scope_Table.Last loop
- if SPARK_Scope_Table.Table (Index).Entity = E then
- return True;
- end if;
- end loop;
+ -- Eliminate entries not appropriate for SPARK
- -- If this assertion fails, this means that the scope which we are
- -- looking for has been treated already, which reveals a problem in
- -- the order of cross-references.
-
- pragma Assert (not Is_Past_Scope_Entity);
+ if SPARK_Entities (Ekind (Ref.Ent))
+ and then SPARK_References (Ref.Typ)
+ and then Is_SPARK_Scope (Ref.Ent_Scope)
+ and then Is_SPARK_Scope (Ref.Ref_Scope)
+ and then Is_SPARK_Reference (Ref.Ent, Ref.Typ)
+ then
+ Process
+ (Index,
+ (Entity => Ref.Ent,
+ Ref_Scope => Ref.Ref_Scope,
+ Rtype => Ref.Typ));
+ end if;
- return False;
- end Is_Future_Scope_Entity;
+ end Add_SPARK_Xref;
------------------------
-- Is_SPARK_Reference --
begin
return Present (E)
and then not Is_Generic_Unit (E)
- and then (not Can_Be_Renamed or else No (Renamed_Entity (E)))
- and then Get_Scope_Num (E) /= No_Scope;
+ and then (not Can_Be_Renamed or else No (Renamed_Entity (E)));
end Is_SPARK_Scope;
- --------
- -- Lt --
- --------
-
- function Lt (Op1 : Natural; Op2 : Natural) return Boolean is
- T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1)));
- T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2)));
-
- begin
- -- First test: if entity is in different unit, sort by unit. Note:
- -- that we use Ent_Scope_File rather than Eun, as Eun may refer to
- -- the file where the generic scope is defined, which may differ from
- -- the file where the enclosing scope is defined. It is the latter
- -- which matters for a correct order here.
-
- if T1.Ent_Scope_File /= T2.Ent_Scope_File then
- return Dependency_Num (T1.Ent_Scope_File) <
- Dependency_Num (T2.Ent_Scope_File);
-
- -- Second test: within same unit, sort by location of the scope of
- -- the entity definition.
-
- elsif Get_Scope_Num (T1.Key.Ent_Scope) /=
- Get_Scope_Num (T2.Key.Ent_Scope)
- then
- return Get_Scope_Num (T1.Key.Ent_Scope) <
- Get_Scope_Num (T2.Key.Ent_Scope);
-
- -- Third test: within same unit and scope, sort by location of
- -- entity definition.
-
- elsif T1.Def /= T2.Def then
- return T1.Def < T2.Def;
-
- else
- -- Both entities must be equal at this point
-
- pragma Assert (T1.Key.Ent = T2.Key.Ent);
- pragma Assert (T1.Key.Ent_Scope = T2.Key.Ent_Scope);
- pragma Assert (T1.Ent_Scope_File = T2.Ent_Scope_File);
-
- -- Fourth test: if reference is in same unit as entity definition,
- -- sort first.
-
- if T1.Key.Lun /= T2.Key.Lun
- and then T1.Ent_Scope_File = T1.Key.Lun
- then
- return True;
-
- elsif T1.Key.Lun /= T2.Key.Lun
- and then T2.Ent_Scope_File = T2.Key.Lun
- then
- return False;
-
- -- Fifth test: if reference is in same unit and same scope as
- -- entity definition, sort first.
-
- elsif T1.Ent_Scope_File = T1.Key.Lun
- and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
- and then T1.Key.Ent_Scope = T1.Key.Ref_Scope
- then
- return True;
-
- elsif T2.Ent_Scope_File = T2.Key.Lun
- and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
- and then T2.Key.Ent_Scope = T2.Key.Ref_Scope
- then
- return False;
-
- -- Sixth test: for same entity, sort by reference location unit
-
- elsif T1.Key.Lun /= T2.Key.Lun then
- return Dependency_Num (T1.Key.Lun) <
- Dependency_Num (T2.Key.Lun);
-
- -- Seventh test: for same entity, sort by reference location scope
-
- elsif Get_Scope_Num (T1.Key.Ref_Scope) /=
- Get_Scope_Num (T2.Key.Ref_Scope)
- then
- return Get_Scope_Num (T1.Key.Ref_Scope) <
- Get_Scope_Num (T2.Key.Ref_Scope);
-
- -- Eighth test: order of location within referencing unit
-
- elsif T1.Key.Loc /= T2.Key.Loc then
- return T1.Key.Loc < T2.Key.Loc;
-
- -- Finally, for two locations at the same address prefer the one
- -- that does NOT have the type 'r', so that a modification or
- -- extension takes preference, when there are more than one
- -- reference at the same location. As a result, in the case of
- -- entities that are in-out actuals, the read reference follows
- -- the modify reference.
-
- else
- return T2.Key.Typ = 'r';
- end if;
- end if;
- end Lt;
-
- ----------
- -- Move --
- ----------
-
- procedure Move (From : Natural; To : Natural) is
- begin
- Rnums (Nat (To)) := Rnums (Nat (From));
- end Move;
-
- -------------------
- -- Set_Scope_Num --
- -------------------
-
- procedure Set_Scope_Num (E : Entity_Id; Num : Nat) renames Scopes.Set;
-
- ------------------------
- -- Update_Scope_Range --
- ------------------------
-
- procedure Update_Scope_Range
- (S : Scope_Index;
- From : Xref_Index;
- To : Xref_Index)
- is
- begin
- SPARK_Scope_Table.Table (S).From_Xref := From;
- SPARK_Scope_Table.Table (S).To_Xref := To;
- end Update_Scope_Range;
-
- -- Local variables
-
- From_Index : Xref_Index;
- Prev_Loc : Source_Ptr;
- Prev_Typ : Character;
- Ref_Count : Nat;
- Scope_Id : Scope_Index;
-
-- Start of processing for Add_SPARK_Xrefs
begin
- for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
- declare
- S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
- begin
- Set_Scope_Num (S.Entity, S.Scope_Num);
- end;
- end loop;
-
- declare
- Drefs_Table : Drefs.Table_Type
- renames Drefs.Table (Drefs.First .. Drefs.Last);
- begin
- Xrefs.Append_All (Xrefs.Table_Type (Drefs_Table));
- Nrefs := Nrefs + Drefs_Table'Length;
- end;
-
- -- Capture the definition Sloc values. As in the case of normal cross
- -- references, we have to wait until now to get the correct value.
-
- for Index in 1 .. Nrefs loop
- Xrefs.Table (Index).Def := Sloc (Xrefs.Table (Index).Key.Ent);
- end loop;
-
- -- Eliminate entries not appropriate for SPARK. Done prior to sorting
- -- cross-references, as it discards useless references which do not have
- -- a proper format for the comparison function (like no location).
-
- Ref_Count := Nrefs;
- Nrefs := 0;
-
- for Index in 1 .. Ref_Count loop
- declare
- Ref : Xref_Key renames Xrefs.Table (Index).Key;
-
- begin
- if SPARK_Entities (Ekind (Ref.Ent))
- and then SPARK_References (Ref.Typ)
- and then Is_SPARK_Scope (Ref.Ent_Scope)
- and then Is_SPARK_Scope (Ref.Ref_Scope)
- and then Is_SPARK_Reference (Ref.Ent, Ref.Typ)
-
- -- Discard references from unknown scopes, e.g. generic scopes
-
- and then Get_Scope_Num (Ref.Ent_Scope) /= No_Scope
- and then Get_Scope_Num (Ref.Ref_Scope) /= No_Scope
-
- -- Discard references to loop parameters introduced within
- -- expression functions, as they give two references: one from
- -- the analysis of the expression function itself and one from
- -- the analysis of the expanded body. We don't lose any globals
- -- by discarding them, because such loop parameters can only be
- -- accessed locally from within the expression function body.
- -- Note: some loop parameters are expanded into variables; they
- -- also must be ignored.
-
- and then not
- (Ekind_In (Ref.Ent, E_Loop_Parameter, E_Variable)
- and then Scope_Within
- (Ref.Ent, Unique_Entity (Ref.Ref_Scope))
- and then Is_Expression_Function (Ref.Ref_Scope))
- then
- Nrefs := Nrefs + 1;
- Rnums (Nrefs) := Index;
- end if;
- end;
- end loop;
-
- -- Sort the references
-
- Sorting.Sort (Integer (Nrefs));
-
- -- Eliminate duplicate entries
-
- -- We need this test for Ref_Count because if we force ALI file
- -- generation in case of errors detected, it may be the case that
- -- Nrefs is 0, so we should not reset it here.
-
- if Nrefs >= 2 then
- Ref_Count := Nrefs;
- Nrefs := 1;
-
- for Index in 2 .. Ref_Count loop
- if Xrefs.Table (Rnums (Index)) /= Xrefs.Table (Rnums (Nrefs)) then
- Nrefs := Nrefs + 1;
- Rnums (Nrefs) := Rnums (Index);
- end if;
- end loop;
- end if;
-
- -- Eliminate the reference if it is at the same location as the previous
- -- one, unless it is a read-reference indicating that the entity is an
- -- in-out actual in a call.
-
- Ref_Count := Nrefs;
- Nrefs := 0;
- Prev_Loc := No_Location;
- Prev_Typ := 'm';
-
- for Index in 1 .. Ref_Count loop
- declare
- Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key;
-
- begin
- if Ref.Loc /= Prev_Loc
- or else (Prev_Typ = 'm' and then Ref.Typ = 'r')
- then
- Prev_Loc := Ref.Loc;
- Prev_Typ := Ref.Typ;
- Nrefs := Nrefs + 1;
- Rnums (Nrefs) := Rnums (Index);
- end if;
- end;
- end loop;
-
- -- The two steps have eliminated all references, nothing to do
-
- if SPARK_Scope_Table.Last = 0 then
- return;
- end if;
-
- Scope_Id := 1;
- From_Index := 1;
-
- -- Loop to output references
+ -- Expose cross-references from private frontend tables to the backend
- for Refno in 1 .. Nrefs loop
- declare
- Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno));
- Ref : Xref_Key renames Ref_Entry.Key;
-
- begin
- -- If this assertion fails, the scope which we are looking for is
- -- not in SPARK scope table, which reveals either a problem in the
- -- construction of the scope table, or an erroneous scope for the
- -- current cross-reference.
-
- pragma Assert (Is_Future_Scope_Entity (Ref.Ent_Scope, Scope_Id));
-
- -- Update the range of cross references to which the current scope
- -- refers to. This may be the empty range only for the first scope
- -- considered.
-
- if Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) then
- Update_Scope_Range
- (S => Scope_Id,
- From => From_Index,
- To => SPARK_Xref_Table.Last);
-
- From_Index := SPARK_Xref_Table.Last + 1;
- end if;
-
- while Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) loop
- Scope_Id := Scope_Id + 1;
- pragma Assert (Scope_Id <= SPARK_Scope_Table.Last);
- end loop;
-
- SPARK_Xref_Table.Append (
- (Entity => Unique_Entity (Ref.Ent),
- Ref_Scope => Ref.Ref_Scope,
- Rtype => Ref.Typ));
- end;
+ for Index in Drefs.First .. Drefs.Last loop
+ Add_SPARK_Xref (Index, Drefs.Table (Index));
end loop;
- -- Update the range of cross references to which the scope refers to
-
- Update_Scope_Range
- (S => Scope_Id,
- From => From_Index,
- To => SPARK_Xref_Table.Last);
- end Add_SPARK_Xrefs;
-
- -------------------------
- -- Collect_SPARK_Xrefs --
- -------------------------
-
- procedure Collect_SPARK_Xrefs
- (Sdep_Table : Unit_Ref_Table;
- Num_Sdep : Nat)
- is
- Sdep : Pos;
- Sdep_Next : Pos;
- -- Index of the current and next source dependency
-
- Sdep_File : Pos;
- -- Index of the file to which the scopes need to be assigned; for
- -- library-level instances of generic units this points to the unit
- -- of the body, because this is where references are assigned to.
-
- Ubody : Unit_Number_Type;
- Uspec : Unit_Number_Type;
- -- Unit numbers for the dependency spec and possibly its body (only in
- -- the case of library-level instance of a generic package).
-
- begin
- -- Cross-references should have been computed first
-
- pragma Assert (Xrefs.Last /= 0);
-
- Initialize_SPARK_Tables;
-
- -- Generate file and scope SPARK cross-reference information
-
- Sdep := 1;
- while Sdep <= Num_Sdep loop
-
- -- Skip dependencies with no entity node, e.g. configuration files
- -- with pragmas (.adc) or target description (.atp), since they
- -- present no interest for SPARK cross references.
-
- if No (Cunit_Entity (Sdep_Table (Sdep))) then
- Sdep_Next := Sdep + 1;
-
- -- For library-level instantiation of a generic, two consecutive
- -- units refer to the same compilation unit node and entity (one to
- -- body, one to spec). In that case, treat them as a single unit for
- -- the sake of SPARK cross references by passing to Add_SPARK_File.
-
- else
- if Sdep < Num_Sdep
- and then Cunit_Entity (Sdep_Table (Sdep)) =
- Cunit_Entity (Sdep_Table (Sdep + 1))
- then
- declare
- Cunit1 : Node_Id renames Cunit (Sdep_Table (Sdep));
- Cunit2 : Node_Id renames Cunit (Sdep_Table (Sdep + 1));
-
- begin
- -- Both Cunits point to compilation unit nodes
-
- pragma Assert
- (Nkind (Cunit1) = N_Compilation_Unit
- and then Nkind (Cunit2) = N_Compilation_Unit);
-
- -- Do not depend on the sorting order, which is based on
- -- Unit_Name, and for library-level instances of nested
- -- generic packages they are equal.
-
- -- If declaration comes before the body
-
- if Nkind (Unit (Cunit1)) = N_Package_Declaration
- and then Nkind (Unit (Cunit2)) = N_Package_Body
- then
- Uspec := Sdep_Table (Sdep);
- Ubody := Sdep_Table (Sdep + 1);
-
- Sdep_File := Sdep + 1;
-
- -- If body comes before declaration
-
- elsif Nkind (Unit (Cunit1)) = N_Package_Body
- and then Nkind (Unit (Cunit2)) = N_Package_Declaration
- then
- Uspec := Sdep_Table (Sdep + 1);
- Ubody := Sdep_Table (Sdep);
-
- Sdep_File := Sdep;
-
- -- Otherwise it is an error
-
- else
- raise Program_Error;
- end if;
-
- Sdep_Next := Sdep + 2;
- end;
-
- -- ??? otherwise?
-
- else
- Uspec := Sdep_Table (Sdep);
- Ubody := No_Unit;
-
- Sdep_File := Sdep;
- Sdep_Next := Sdep + 1;
- end if;
-
- Add_SPARK_File
- (Uspec => Uspec,
- Ubody => Ubody,
- Dspec => Sdep_File);
- end if;
-
- Sdep := Sdep_Next;
+ for Index in Xrefs.First .. Xrefs.Last loop
+ Add_SPARK_Xref (-Index, Xrefs.Table (Index));
end loop;
-
- -- Generate SPARK cross-reference information
-
- Add_SPARK_Xrefs;
- end Collect_SPARK_Xrefs;
+ end Iterate_SPARK_Xrefs;
-------------------------------------
-- Enclosing_Subprogram_Or_Package --
return Context;
end Enclosing_Subprogram_Or_Library_Package;
- -----------------
- -- Entity_Hash --
- -----------------
-
- function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is
- begin
- return
- Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1));
- end Entity_Hash;
-
--------------------------
-- Generate_Dereference --
--------------------------
end if;
end Generate_Dereference;
- -------------------------------
- -- Traverse_Compilation_Unit --
- -------------------------------
-
- procedure Traverse_Compilation_Unit (CU : Node_Id) is
- procedure Traverse_Block (N : Node_Id);
- procedure Traverse_Declaration_Or_Statement (N : Node_Id);
- procedure Traverse_Declarations_And_HSS (N : Node_Id);
- procedure Traverse_Declarations_Or_Statements (L : List_Id);
- procedure Traverse_Handled_Statement_Sequence (N : Node_Id);
- procedure Traverse_Package_Body (N : Node_Id);
- procedure Traverse_Visible_And_Private_Parts (N : Node_Id);
- procedure Traverse_Protected_Body (N : Node_Id);
- procedure Traverse_Subprogram_Body (N : Node_Id);
- procedure Traverse_Task_Body (N : Node_Id);
-
- -- Traverse corresponding construct, calling Process on all declarations
-
- --------------------
- -- Traverse_Block --
- --------------------
-
- procedure Traverse_Block (N : Node_Id) renames
- Traverse_Declarations_And_HSS;
-
- ---------------------------------------
- -- Traverse_Declaration_Or_Statement --
- ---------------------------------------
-
- procedure Traverse_Declaration_Or_Statement (N : Node_Id) is
- function Traverse_Stub (N : Node_Id) return Boolean;
- -- Returns True iff stub N should be traversed
-
- function Traverse_Stub (N : Node_Id) return Boolean is
- begin
- pragma Assert (Nkind_In (N, N_Package_Body_Stub,
- N_Protected_Body_Stub,
- N_Subprogram_Body_Stub,
- N_Task_Body_Stub));
-
- return Present (Library_Unit (N));
- end Traverse_Stub;
-
- -- Start of processing for Traverse_Declaration_Or_Statement
-
- begin
- case Nkind (N) is
- when N_Package_Declaration =>
- Traverse_Visible_And_Private_Parts (Specification (N));
-
- when N_Package_Body =>
- Traverse_Package_Body (N);
-
- when N_Package_Body_Stub =>
- if Traverse_Stub (N) then
- Traverse_Package_Body (Get_Body_From_Stub (N));
- end if;
-
- when N_Subprogram_Body =>
- Traverse_Subprogram_Body (N);
-
- when N_Entry_Body =>
- Traverse_Subprogram_Body (N);
-
- when N_Subprogram_Body_Stub =>
- if Traverse_Stub (N) then
- Traverse_Subprogram_Body (Get_Body_From_Stub (N));
- end if;
-
- when N_Protected_Body =>
- Traverse_Protected_Body (N);
-
- when N_Protected_Body_Stub =>
- if Traverse_Stub (N) then
- Traverse_Protected_Body (Get_Body_From_Stub (N));
- end if;
-
- when N_Protected_Type_Declaration =>
- Traverse_Visible_And_Private_Parts (Protected_Definition (N));
-
- when N_Task_Type_Declaration =>
-
- -- Task type definition is optional (unlike protected type
- -- definition, which is mandatory).
-
- declare
- Task_Def : constant Node_Id := Task_Definition (N);
- begin
- if Present (Task_Def) then
- Traverse_Visible_And_Private_Parts (Task_Def);
- end if;
- end;
-
- when N_Task_Body =>
- Traverse_Task_Body (N);
-
- when N_Task_Body_Stub =>
- if Traverse_Stub (N) then
- Traverse_Task_Body (Get_Body_From_Stub (N));
- end if;
-
- when N_Block_Statement =>
- Traverse_Block (N);
-
- when N_If_Statement =>
-
- -- Traverse the statements in the THEN part
-
- Traverse_Declarations_Or_Statements (Then_Statements (N));
-
- -- Loop through ELSIF parts if present
-
- if Present (Elsif_Parts (N)) then
- declare
- Elif : Node_Id := First (Elsif_Parts (N));
-
- begin
- while Present (Elif) loop
- Traverse_Declarations_Or_Statements
- (Then_Statements (Elif));
- Next (Elif);
- end loop;
- end;
- end if;
-
- -- Finally traverse the ELSE statements if present
-
- Traverse_Declarations_Or_Statements (Else_Statements (N));
-
- when N_Case_Statement =>
-
- -- Process case branches
-
- declare
- Alt : Node_Id := First (Alternatives (N));
- begin
- loop
- Traverse_Declarations_Or_Statements (Statements (Alt));
- Next (Alt);
- exit when No (Alt);
- end loop;
- end;
-
- when N_Extended_Return_Statement =>
- Traverse_Handled_Statement_Sequence
- (Handled_Statement_Sequence (N));
-
- when N_Loop_Statement =>
- Traverse_Declarations_Or_Statements (Statements (N));
-
- -- Generic declarations are ignored
-
- when others =>
- null;
- end case;
- end Traverse_Declaration_Or_Statement;
-
- -----------------------------------
- -- Traverse_Declarations_And_HSS --
- -----------------------------------
-
- procedure Traverse_Declarations_And_HSS (N : Node_Id) is
- begin
- Traverse_Declarations_Or_Statements (Declarations (N));
- Traverse_Handled_Statement_Sequence (Handled_Statement_Sequence (N));
- end Traverse_Declarations_And_HSS;
-
- -----------------------------------------
- -- Traverse_Declarations_Or_Statements --
- -----------------------------------------
-
- procedure Traverse_Declarations_Or_Statements (L : List_Id) is
- N : Node_Id;
-
- begin
- -- Loop through statements or declarations
-
- N := First (L);
- while Present (N) loop
-
- -- Call Process on all declarations
-
- if Nkind (N) in N_Declaration
- or else Nkind (N) in N_Later_Decl_Item
- or else Nkind (N) = N_Entry_Body
- then
- if Nkind (N) in N_Body_Stub then
- Process (Get_Body_From_Stub (N));
- else
- Process (N);
- end if;
- end if;
-
- Traverse_Declaration_Or_Statement (N);
-
- Next (N);
- end loop;
- end Traverse_Declarations_Or_Statements;
-
- -----------------------------------------
- -- Traverse_Handled_Statement_Sequence --
- -----------------------------------------
-
- procedure Traverse_Handled_Statement_Sequence (N : Node_Id) is
- Handler : Node_Id;
-
- begin
- if Present (N) then
- Traverse_Declarations_Or_Statements (Statements (N));
-
- if Present (Exception_Handlers (N)) then
- Handler := First (Exception_Handlers (N));
- while Present (Handler) loop
- Traverse_Declarations_Or_Statements (Statements (Handler));
- Next (Handler);
- end loop;
- end if;
- end if;
- end Traverse_Handled_Statement_Sequence;
-
- ---------------------------
- -- Traverse_Package_Body --
- ---------------------------
-
- procedure Traverse_Package_Body (N : Node_Id) is
- Spec_E : constant Entity_Id := Unique_Defining_Entity (N);
-
- begin
- case Ekind (Spec_E) is
- when E_Package =>
- Traverse_Declarations_And_HSS (N);
-
- when E_Generic_Package =>
- null;
-
- when others =>
- raise Program_Error;
- end case;
- end Traverse_Package_Body;
-
- -----------------------------
- -- Traverse_Protected_Body --
- -----------------------------
-
- procedure Traverse_Protected_Body (N : Node_Id) is
- begin
- Traverse_Declarations_Or_Statements (Declarations (N));
- end Traverse_Protected_Body;
-
- ------------------------------
- -- Traverse_Subprogram_Body --
- ------------------------------
-
- procedure Traverse_Subprogram_Body (N : Node_Id) is
- Spec_E : constant Entity_Id := Unique_Defining_Entity (N);
-
- begin
- case Ekind (Spec_E) is
- when Entry_Kind
- | E_Function
- | E_Procedure
- =>
- Traverse_Declarations_And_HSS (N);
-
- when Generic_Subprogram_Kind =>
- null;
-
- when others =>
- raise Program_Error;
- end case;
- end Traverse_Subprogram_Body;
-
- ------------------------
- -- Traverse_Task_Body --
- ------------------------
-
- procedure Traverse_Task_Body (N : Node_Id) renames
- Traverse_Declarations_And_HSS;
-
- ----------------------------------------
- -- Traverse_Visible_And_Private_Parts --
- ----------------------------------------
-
- procedure Traverse_Visible_And_Private_Parts (N : Node_Id) is
- begin
- Traverse_Declarations_Or_Statements (Visible_Declarations (N));
- Traverse_Declarations_Or_Statements (Private_Declarations (N));
- end Traverse_Visible_And_Private_Parts;
-
- -- Local variables
-
- Lu : Node_Id;
-
- -- Start of processing for Traverse_Compilation_Unit
-
- begin
- -- Get Unit (checking case of subunit)
-
- Lu := Unit (CU);
-
- if Nkind (Lu) = N_Subunit then
- Lu := Proper_Body (Lu);
- end if;
-
- -- Do not add scopes for generic units
-
- if Nkind (Lu) = N_Package_Body
- and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
- then
- return;
- end if;
-
- -- Call Process on all declarations
-
- if Nkind (Lu) in N_Declaration
- or else Nkind (Lu) in N_Later_Decl_Item
- then
- Process (Lu);
- end if;
-
- -- Traverse the unit
-
- Traverse_Declaration_Or_Statement (Lu);
- end Traverse_Compilation_Unit;
-
end SPARK_Specific;
-- This package contains for collecting and outputting cross-reference
-- information.
-with Einfo; use Einfo;
+with Einfo; use Einfo;
+with SPARK_Xrefs;
package Lib.Xref is
-- This procedure is called to record a dereference. N is the location
-- of the dereference.
- procedure Collect_SPARK_Xrefs
- (Sdep_Table : Unit_Ref_Table;
- Num_Sdep : Nat);
- -- Collect SPARK cross-reference information from library units (for
- -- files and scopes) and from shared cross-references. Fill in the
- -- tables in library package called SPARK_Xrefs.
+ generic
+ with procedure Process
+ (Index : Int;
+ Xref : SPARK_Xrefs.SPARK_Xref_Record);
+ procedure Iterate_SPARK_Xrefs;
+ -- Call Process on cross-references relevant to the SPARK backend with
+ -- parameter Xref holding the relevant subset of the xref entry and
+ -- Index holding the position in the original tables with references
+ -- (if positive) or dereferences (if negative).
end SPARK_Specific;
-- * Diagnose at compile-time or install run-time checks to prevent ABE
-- access to data and behaviour.
--
- -- The high level idea is to accurately diagnose ABE issues within a
+ -- The high-level idea is to accurately diagnose ABE issues within a
-- single unit because the ABE mechanism can inspect the whole unit.
-- As soon as the elaboration graph extends to an external unit, the
-- diagnostics stop because the body of the unit may not be available.
-- the library level if it appears in a package library unit, ignoring
-- enclosng packages.
--
- -- * Non-library level encapsulator - A construct that cannot be elaborated
- -- on its own and requires elaboration by a top level scenario.
+ -- * Non-library-level encapsulator - A construct that cannot be elaborated
+ -- on its own and requires elaboration by a top-level scenario.
--
-- * Scenario - A construct or context which may be elaborated or executed
-- by elaboration code. The scenarios recognized by the ABE mechanism are
--
-- - For task activation, the target is the task body
--
- -- * Top level scenario - A scenario which appears in a non-generic main
+ -- * Top-level scenario - A scenario which appears in a non-generic main
-- unit. Depending on the elaboration model is in effect, the following
-- addotional restrictions apply:
--
-- The Recording phase coincides with the analysis/resolution phase of the
-- compiler. It has the following objectives:
--
- -- * Record all top level scenarios for examination by the Processing
+ -- * Record all top-level scenarios for examination by the Processing
-- phase.
--
-- Saving only a certain number of nodes improves the performance of
-- and/or inlining of bodies, but before the removal of Ghost code. It has
-- the following objectives:
--
- -- * Examine all top level scenarios saved during the Recording phase
+ -- * Examine all top-level scenarios saved during the Recording phase
--
- -- The top level scenarios act as roots for depth-first traversal of
+ -- The top-level scenarios act as roots for depth-first traversal of
-- the call/instantiation/task activation graph. The traversal stops
-- when an outgoing edge leaves the main unit.
--
-- The following steps describe how to add a new elaboration scenario and
-- preserve the existing architecture.
--
- -- 1) If necessary, update predicates Is_Check_Emitting_Scenario and
- -- Is_Scenario.
+ -- 1) If necessary, update predicate Is_Scenario
--
-- 2) Add predicate Is_Suitable_xxx. Include a call to it in predicate
-- Is_Suitable_Scenario.
Hash => Elaboration_Context_Hash,
Equal => "=");
+ -- The following table stores a status flag for each top-level scenario
+ -- recorded in table Top_Level_Scenarios.
+
+ Recorded_Top_Level_Scenarios_Max : constant := 503;
+
+ type Recorded_Top_Level_Scenarios_Index is
+ range 0 .. Recorded_Top_Level_Scenarios_Max - 1;
+
+ function Recorded_Top_Level_Scenarios_Hash
+ (Key : Node_Id) return Recorded_Top_Level_Scenarios_Index;
+ -- Obtain the hash value of entity Key
+
+ package Recorded_Top_Level_Scenarios is new Simple_HTable
+ (Header_Num => Recorded_Top_Level_Scenarios_Index,
+ Element => Boolean,
+ No_Element => False,
+ Key => Node_Id,
+ Hash => Recorded_Top_Level_Scenarios_Hash,
+ Equal => "=");
+
-- The following table stores all active scenarios in a recursive traversal
- -- starting from a top level scenario. This table must be maintained in a
+ -- starting from a top-level scenario. This table must be maintained in a
-- FIFO fashion.
package Scenario_Stack is new Table.Table
Table_Increment => 100,
Table_Name => "Scenario_Stack");
- -- The following table stores all top level scenario saved during the
+ -- The following table stores all top-level scenario saved during the
-- Recording phase. The contents of this table act as traversal roots
-- later in the Processing phase. This table must be maintained in a
-- LIFO fashion.
Table_Name => "Top_Level_Scenarios");
-- The following table stores the bodies of all eligible scenarios visited
- -- during a traversal starting from a top level scenario. The contents of
+ -- during a traversal starting from a top-level scenario. The contents of
-- this table must be reset upon each new traversal.
Visited_Bodies_Max : constant := 511;
-- Return the code unit which contains arbitrary node or entity N. This
-- is the unit of the file which physically contains the related construct
-- denoted by N except when N is within an instantiation. In that case the
- -- unit is that of the top level instantiation.
+ -- unit is that of the top-level instantiation.
procedure Find_Elaborated_Units;
-- Populate table Elaboration_Context with all units which have prior
pragma Inline (Is_Bodiless_Subprogram);
-- Determine whether subprogram Subp_Id will never have a body
- function Is_Check_Emitting_Scenario (N : Node_Id) return Boolean;
- pragma Inline (Is_Check_Emitting_Scenario);
- -- Determine whether arbitrary node N denotes a scenario which may emit a
- -- conditional ABE check.
-
function Is_Controlled_Proc
(Subp_Id : Entity_Id;
Subp_Nam : Name_Id) return Boolean;
-- Determine whether entity Id denotes the protected or unprotected version
-- of a protected subprogram.
+ function Is_Recorded_Top_Level_Scenario (N : Node_Id) return Boolean;
+ pragma Inline (Is_Recorded_Top_Level_Scenario);
+ -- Determine whether arbitrary node is a recorded top-level scenario which
+ -- appears in table Top_Level_Scenarios.
+
function Is_Safe_Activation
(Call : Node_Id;
Task_Decl : Node_Id) return Boolean;
-- routine.
procedure Process_Guaranteed_ABE (N : Node_Id);
- -- Top level dispatcher for processing of scenarios which result in a
+ -- Top-level dispatcher for processing of scenarios which result in a
-- guaranteed ABE.
procedure Process_Instantiation
(Exp_Inst : Node_Id;
In_Partial_Fin : Boolean;
In_Task_Body : Boolean);
- -- Top level dispatcher for processing of instantiations. Perform ABE
+ -- Top-level dispatcher for processing of instantiations. Perform ABE
-- checks and diagnostics for expanded instantiation Exp_Inst. Flag
-- In_Partial_Fin shoud be set when the processing is initiated by a
-- partial finalization routine. Flag In_Task_Body should be set when
(N : Node_Id;
In_Partial_Fin : Boolean := False;
In_Task_Body : Boolean := False);
- -- Top level dispatcher for processing of various elaboration scenarios.
+ -- Top-level dispatcher for processing of various elaboration scenarios.
-- Perform ABE checks and diagnostics for scenario N. Flag In_Partial_Fin
-- shoud be set when the processing is initiated by a partial finalization
-- routine. Flag In_Task_Body should be set when the processing is started
-- from a task body.
procedure Process_Variable_Assignment (Asmt : Node_Id);
- -- Top level dispatcher for processing of variable assignments. Perform ABE
+ -- Top-level dispatcher for processing of variable assignments. Perform ABE
-- checks and diagnostics for assignment statement Asmt.
procedure Process_Variable_Assignment_Ada
-- updates the value of variable Var_Id using the SPARK rules.
procedure Process_Variable_Reference (Ref : Node_Id);
- -- Top level dispatcher for processing of variable references. Perform ABE
+ -- Top-level dispatcher for processing of variable references. Perform ABE
-- checks and diagnostics for variable reference Ref.
procedure Process_Variable_Reference_Read
function Root_Scenario return Node_Id;
pragma Inline (Root_Scenario);
- -- Return the top level scenario which started a recursive search for other
- -- scenarios. It is assumed that there is a valid top level scenario on the
+ -- Return the top-level scenario which started a recursive search for other
+ -- scenarios. It is assumed that there is a valid top-level scenario on the
-- active scenario stack.
+ procedure Set_Is_Recorded_Top_Level_Scenario
+ (N : Node_Id;
+ Val : Boolean := True);
+ pragma Inline (Set_Is_Recorded_Top_Level_Scenario);
+ -- Mark scenario N as being recorded in table Top_Level_Scenarios
+
function Static_Elaboration_Checks return Boolean;
pragma Inline (Static_Elaboration_Checks);
-- Determine whether the static model is in effect
Find_Elaborated_Units;
- -- Examine each top level scenario saved during the Recording phase and
+ -- Examine each top-level scenario saved during the Recording phase and
-- perform various actions depending on the elaboration model in effect.
for Index in Top_Level_Scenarios.First .. Top_Level_Scenarios.Last loop
- -- Clear the table of visited scenario bodies for each new top level
+ -- Clear the table of visited scenario bodies for each new top-level
-- scenario.
Visited_Bodies.Reset;
Level := Find_Enclosing_Level (Call);
- -- Library level calls are always considered because they are part of
+ -- Library-level calls are always considered because they are part of
-- the associated unit's elaboration actions.
if Level in Library_Level then
return Declaration_Level;
end if;
- -- The current construct is a declaration level encapsulator
+ -- The current construct is a declaration-level encapsulator
elsif Nkind_In (Curr, N_Entry_Body,
N_Subprogram_Body,
return Declaration_Level;
end if;
- -- The current construct is a non-library level encapsulator which
+ -- The current construct is a non-library-level encapsulator which
-- indicates that the node cannot possibly appear at any level.
- -- Note that this check must come after the declaration level check
+ -- Note that this check must come after the declaration-level check
-- because both predicates share certain nodes.
elsif Is_Non_Library_Level_Encapsulator (Curr) then
Nested_OK : Boolean := False) return Boolean
is
function Find_Enclosing_Context (N : Node_Id) return Node_Id;
- -- Return the nearest enclosing non-library level or compilation unit
+ -- Return the nearest enclosing non-library-level or compilation unit
-- node which which encapsulates arbitrary node N. Return Empty is no
-- such context is available.
return Par;
end if;
- -- Reaching a compilation unit node without hitting a non-library
+ -- Reaching a compilation unit node without hitting a non-library-
-- level encapsulator indicates that N is at the library level in
-- which case the compilation unit is the context.
procedure Initialize is
begin
- -- Set the soft link which enables Atree.Rewrite to update a top level
+ -- Set the soft link which enables Atree.Rewrite to update a top-level
-- scenario each time it is transformed into another node.
Set_Rewriting_Proc (Update_Elaboration_Scenario'Access);
return False;
end Is_Bodiless_Subprogram;
- --------------------------------
- -- Is_Check_Emitting_Scenario --
- --------------------------------
-
- function Is_Check_Emitting_Scenario (N : Node_Id) return Boolean is
- begin
- return
- Nkind_In (N, N_Call_Marker,
- N_Function_Instantiation,
- N_Package_Instantiation,
- N_Procedure_Instantiation);
- end Is_Check_Emitting_Scenario;
-
------------------------
-- Is_Controlled_Proc --
------------------------
and then Present (Protected_Subprogram (Id));
end Is_Protected_Body_Subp;
+ ------------------------------------
+ -- Is_Recorded_Top_Level_Scenario --
+ ------------------------------------
+
+ function Is_Recorded_Top_Level_Scenario (N : Node_Id) return Boolean is
+ begin
+ return Recorded_Top_Level_Scenarios.Get (N);
+ end Is_Recorded_Top_Level_Scenario;
+
------------------------
-- Is_Safe_Activation --
------------------------
begin
-- The root appears within the declaratons of a block statement, entry
-- body, subprogram body, or task body ignoring enclosing packages. The
- -- root is always within the main unit. An up level target is a notion
+ -- root is always within the main unit. An up-level target is a notion
-- applicable only to the static model because scenarios are reached by
-- means of graph traversal started from a fixed declarative or library
-- level.
if Static_Elaboration_Checks
and then Find_Enclosing_Level (Root) = Declaration_Level
then
- -- The target is within the main unit. It acts as an up level target
+ -- The target is within the main unit. It acts as an up-level target
-- when it appears within a context which encloses the root.
-- package body Main_Unit is
return not In_Same_Context (Root, Target_Decl, Nested_OK => True);
-- Otherwise the target is external to the main unit which makes it
- -- an up level target.
+ -- an up-level target.
else
return True;
-------------------------------
procedure Kill_Elaboration_Scenario (N : Node_Id) is
+ package Scenarios renames Top_Level_Scenarios;
+
begin
- -- Eliminate the scenario by suppressing the generation of conditional
- -- ABE checks or guaranteed ABE failures. Note that other diagnostics
- -- must be carried out ignoring the fact that the scenario is within
- -- dead code.
+ -- Eliminate a recorded top-level scenario when it appears within dead
+ -- code because it will not be executed at elaboration time.
- if Is_Scenario (N) then
- Set_Is_Elaboration_Checks_OK_Node (N, False);
+ if Is_Scenario (N)
+ and then Is_Recorded_Top_Level_Scenario (N)
+ then
+ -- Performance node: list traversal
+
+ for Index in Scenarios.First .. Scenarios.Last loop
+ if Scenarios.Table (Index) = N then
+ Scenarios.Table (Index) := Empty;
+
+ -- The top-level scenario is no longer recorded
+
+ Set_Is_Recorded_Top_Level_Scenario (N, False);
+ return;
+ end if;
+ end loop;
+
+ -- A recorded top-level scenario must be in the table of recorded
+ -- top-level scenarios.
+
+ pragma Assert (False);
end if;
end Kill_Elaboration_Scenario;
return;
end if;
- -- Ensure that a library level call does not appear in a preelaborated
+ -- Ensure that a library-level call does not appear in a preelaborated
-- unit. The check must come before ignoring scenarios within external
-- units or inside generics because calls in those context must also be
-- verified.
Level := Find_Enclosing_Level (N);
- -- Declaration level scenario
+ -- Declaration-level scenario
if Declaration_Level_OK and then Level = Declaration_Level then
null;
- -- Library level scenario
+ -- Library-level scenario
elsif Level in Library_Level then
null;
- -- Instantiation library level scenario
+ -- Instantiation library-level scenario
elsif Level = Instantiation then
null;
-- Otherwise the scenario does not appear at the proper level and
- -- cannot possibly act as a top level scenario.
+ -- cannot possibly act as a top-level scenario.
else
return;
-- later processing by the ABE phase.
Top_Level_Scenarios.Append (N);
+ Set_Is_Recorded_Top_Level_Scenario (N);
+ end Record_Elaboration_Scenario;
- -- Mark a scenario which may produce run-time conditional ABE checks or
- -- guaranteed ABE failures as recorded. The flag ensures that scenario
- -- rewriting performed by Atree.Rewrite will be properly reflected in
- -- all relevant internal data structures.
+ ---------------------------------------
+ -- Recorded_Top_Level_Scenarios_Hash --
+ ---------------------------------------
- if Is_Check_Emitting_Scenario (N) then
- Set_Is_Recorded_Scenario (N);
- end if;
- end Record_Elaboration_Scenario;
+ function Recorded_Top_Level_Scenarios_Hash
+ (Key : Node_Id) return Recorded_Top_Level_Scenarios_Index
+ is
+ begin
+ return
+ Recorded_Top_Level_Scenarios_Index
+ (Key mod Recorded_Top_Level_Scenarios_Max);
+ end Recorded_Top_Level_Scenarios_Hash;
-------------------
-- Root_Scenario --
return Stack.Table (Stack.First);
end Root_Scenario;
+ ----------------------------------------
+ -- Set_Is_Recorded_Top_Level_Scenario --
+ ----------------------------------------
+
+ procedure Set_Is_Recorded_Top_Level_Scenario
+ (N : Node_Id;
+ Val : Boolean := True)
+ is
+ begin
+ Recorded_Top_Level_Scenarios.Set (N, Val);
+ end Set_Is_Recorded_Top_Level_Scenario;
+
-------------------------------
-- Static_Elaboration_Checks --
-------------------------------
-- Save a suitable scenario in the Nested_Scenarios list of the
-- subprogram body. As a result any subsequent traversals of the
- -- subprogram body started from a different top level scenario no
+ -- subprogram body started from a different top-level scenario no
-- longer need to reexamine the tree.
elsif Is_Suitable_Scenario (Nod) then
end if;
-- Nothing to do if the body was already traversed during the processing
- -- of the same top level scenario.
+ -- of the same top-level scenario.
if Visited_Bodies.Get (N) then
return;
Nested := Nested_Scenarios (Defining_Entity (N));
-- The subprogram body was already examined as part of the elaboration
- -- graph starting from a different top level scenario. There is no need
+ -- graph starting from a different top-level scenario. There is no need
-- to traverse the declarations and statements again because this will
-- yield the exact same scenarios. Use the nested scenarios collected
-- during the first inspection of the body.
package Scenarios renames Top_Level_Scenarios;
begin
+ -- Nothing to do when the old and new scenarios are one and the same
+
+ if Old_N = New_N then
+ return;
+
-- A scenario is being transformed by Atree.Rewrite. Update all relevant
-- internal data structures to reflect this change. This ensures that a
-- potential run-time conditional ABE check or a guaranteed ABE failure
-- is inserted at the proper place in the tree.
- if Is_Check_Emitting_Scenario (Old_N)
- and then Is_Recorded_Scenario (Old_N)
- and then Old_N /= New_N
+ elsif Is_Scenario (Old_N)
+ and then Is_Recorded_Top_Level_Scenario (Old_N)
then
-- Performance note: list traversal
if Scenarios.Table (Index) = Old_N then
Scenarios.Table (Index) := New_N;
- Set_Is_Recorded_Scenario (Old_N, False);
- Set_Is_Recorded_Scenario (New_N);
+ -- The old top-level scenario is no longer recorded, but the
+ -- new one is.
+
+ Set_Is_Recorded_Top_Level_Scenario (Old_N, False);
+ Set_Is_Recorded_Top_Level_Scenario (New_N);
return;
end if;
end loop;
- -- A recorded scenario must be in the table of recorded scenarios
+ -- A recorded top-level scenario must be in the table of recorded
+ -- top-level scenarios.
pragma Assert (False);
end if;
elsif Placement = Private_State_Space then
if Scope (Encap_Id) /= Pack_Id then
SPARK_Msg_NE
- ("indicator Part_Of must designate an abstract state of "
+ ("indicator Part_Of must denote an abstract state of "
& "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id);
Error_Msg_Name_1 := Chars (Pack_Id);
SPARK_Msg_NE
(Parent (Associated_Node_For_Itype (Typ))))
then
Error_Msg_N
- ("info: coextension will not be finalized when its "
+ ("??coextension will not be finalized when its "
& "associated owner is finalized", N);
else
Error_Msg_N
- ("info: coextension will not be finalized when its "
+ ("??coextension will not be finalized when its "
& "associated owner is deallocated", N);
end if;
else
(Parent (Associated_Node_For_Itype (Typ))))
then
Error_Msg_N
- ("info: coextension will not be deallocated when its "
- & "associated owner is finalized", N);
+ ("??coextension will not be deallocated when "
+ & "its associated owner is finalized", N);
else
Error_Msg_N
- ("info: coextension will not be deallocated when its "
- & "associated owner is deallocated", N);
+ ("??coextension will not be deallocated when "
+ & "its associated owner is deallocated", N);
end if;
end if;
end if;
else
Set_Is_Dynamic_Coextension (N, False);
Set_Is_Static_Coextension (N, False);
+
+ -- ??? It seems we also do not properly finalize anonymous
+ -- access-to-controlled objects within their declared scope and
+ -- instead finalize them with their associated unit. Warn the
+ -- user about it here.
+
+ if Ekind (Typ) = E_Anonymous_Access_Type
+ and then Is_Controlled_Active (Desig_T)
+ then
+ Error_Msg_N ("??anonymous access-to-controlled object will "
+ & "be finalized when its enclosing unit goes out "
+ & "of scope", N);
+ end if;
end if;
end if;
return Flag1 (N);
end Is_Read;
- function Is_Recorded_Scenario
- (N : Node_Id) return Boolean is
- begin
- pragma Assert (False
- or else NT (N).Nkind = N_Call_Marker
- or else NT (N).Nkind = N_Function_Instantiation
- or else NT (N).Nkind = N_Package_Instantiation
- or else NT (N).Nkind = N_Procedure_Instantiation);
- return Flag6 (N);
- end Is_Recorded_Scenario;
-
function Is_Source_Call
(N : Node_Id) return Boolean is
begin
Set_Flag1 (N, Val);
end Set_Is_Read;
- procedure Set_Is_Recorded_Scenario
- (N : Node_Id; Val : Boolean := True) is
- begin
- pragma Assert (False
- or else NT (N).Nkind = N_Call_Marker
- or else NT (N).Nkind = N_Function_Instantiation
- or else NT (N).Nkind = N_Package_Instantiation
- or else NT (N).Nkind = N_Procedure_Instantiation);
- Set_Flag6 (N, Val);
- end Set_Is_Recorded_Scenario;
-
procedure Set_Is_Source_Call
(N : Node_Id; Val : Boolean := True) is
begin
-- Present in variable reference markers. Set when the original variable
-- reference constitues a read of the variable.
- -- Is_Recorded_Scenario (Flag6-Sem)
- -- Present in call marker and instantiation nodes. Set when the scenario
- -- was saved by the ABE Recording phase. This flag aids the ABE machinery
- -- to keep its internal data up-to-date in case the node is transformed
- -- by Atree.Rewrite.
-
-- Is_Source_Call (Flag4-Sem)
-- Present in call marker nodes. Set when the related call came from
-- source.
-- Is_Elaboration_Checks_OK_Node (Flag1-Sem)
-- Is_SPARK_Mode_On_Node (Flag2-Sem)
-- Is_Declaration_Level_Node (Flag5-Sem)
- -- Is_Recorded_Scenario (Flag6-Sem)
-- Is_Known_Guaranteed_ABE (Flag18-Sem)
-- N_Procedure_Instantiation
-- Is_Elaboration_Checks_OK_Node (Flag1-Sem)
-- Is_SPARK_Mode_On_Node (Flag2-Sem)
-- Is_Declaration_Level_Node (Flag5-Sem)
- -- Is_Recorded_Scenario (Flag6-Sem)
-- Must_Override (Flag14) set if overriding indicator present
-- Must_Not_Override (Flag15) set if not_overriding indicator present
-- Is_Known_Guaranteed_ABE (Flag18-Sem)
-- Is_Elaboration_Checks_OK_Node (Flag1-Sem)
-- Is_SPARK_Mode_On_Node (Flag2-Sem)
-- Is_Declaration_Level_Node (Flag5-Sem)
- -- Is_Recorded_Scenario (Flag6-Sem)
-- Must_Override (Flag14) set if overriding indicator present
-- Must_Not_Override (Flag15) set if not_overriding indicator present
-- Is_Known_Guaranteed_ABE (Flag18-Sem)
-- Is_Dispatching_Call (Flag3-Sem)
-- Is_Source_Call (Flag4-Sem)
-- Is_Declaration_Level_Node (Flag5-Sem)
- -- Is_Recorded_Scenario (Flag6-Sem)
-- Is_Known_Guaranteed_ABE (Flag18-Sem)
------------------------
function Is_Read
(N : Node_Id) return Boolean; -- Flag1
- function Is_Recorded_Scenario
- (N : Node_Id) return Boolean; -- Flag6
-
function Is_Source_Call
(N : Node_Id) return Boolean; -- Flag4
procedure Set_Is_Read
(N : Node_Id; Val : Boolean := True); -- Flag1
- procedure Set_Is_Recorded_Scenario
- (N : Node_Id; Val : Boolean := True); -- Flag6
-
procedure Set_Is_Source_Call
(N : Node_Id; Val : Boolean := True); -- Flag4
pragma Inline (Is_Protected_Subprogram_Body);
pragma Inline (Is_Qualified_Universal_Literal);
pragma Inline (Is_Read);
- pragma Inline (Is_Recorded_Scenario);
pragma Inline (Is_Source_Call);
pragma Inline (Is_SPARK_Mode_On_Node);
pragma Inline (Is_Static_Coextension);
pragma Inline (Set_Is_Protected_Subprogram_Body);
pragma Inline (Set_Is_Qualified_Universal_Literal);
pragma Inline (Set_Is_Read);
- pragma Inline (Set_Is_Recorded_Scenario);
pragma Inline (Set_Is_Source_Call);
pragma Inline (Set_Is_SPARK_Mode_On_Node);
pragma Inline (Set_Is_Static_Coextension);
-- --
------------------------------------------------------------------------------
+with Lib.Xref;
with Output; use Output;
with Sem_Util; use Sem_Util;
------------
procedure dspark is
- begin
- -- Dump SPARK cross-reference file table
-
- Write_Line ("SPARK Xrefs File Table");
- Write_Line ("----------------------");
-
- for Index in SPARK_File_Table.First .. SPARK_File_Table.Last loop
- declare
- AFR : SPARK_File_Record renames SPARK_File_Table.Table (Index);
-
- begin
- Write_Str (" ");
- Write_Int (Int (Index));
- Write_Str (". File_Num = ");
- Write_Int (Int (AFR.File_Num));
- Write_Str (" From = ");
- Write_Int (Int (AFR.From_Scope));
- Write_Str (" To = ");
- Write_Int (Int (AFR.To_Scope));
- Write_Eol;
- end;
- end loop;
-
- -- Dump SPARK cross-reference scope table
- Write_Eol;
- Write_Line ("SPARK Xrefs Scope Table");
- Write_Line ("-----------------------");
+ procedure Dump (Index : Nat; AXR : SPARK_Xref_Record);
+
+ procedure Dump_SPARK_Xrefs is new
+ Lib.Xref.SPARK_Specific.Iterate_SPARK_Xrefs (Dump);
+
+ ----------
+ -- Dump --
+ ----------
+
+ procedure Dump (Index : Nat; AXR : SPARK_Xref_Record) is
+ begin
+ Write_Str (" ");
+ Write_Int (Index);
+ Write_Char ('.');
+
+ Write_Str (" Entity = " & Unique_Name (AXR.Entity));
+ Write_Str (" (");
+ Write_Int (Nat (AXR.Entity));
+ Write_Str (")");
- for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
- declare
- ASR : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
+ Write_Str (" Scope = " & Unique_Name (AXR.Ref_Scope));
+ Write_Str (" (");
+ Write_Int (Nat (AXR.Ref_Scope));
+ Write_Str (")");
- begin
- Write_Str (" ");
- Write_Int (Int (Index));
- Write_Str (" Scope_Name = """);
+ Write_Str (" Ref_Type = '" & AXR.Rtype & "'");
- Write_Str (Unique_Name (ASR.Entity));
+ Write_Eol;
+ end Dump;
- Write_Char ('"');
- Write_Str (" From = ");
- Write_Int (Int (ASR.From_Xref));
- Write_Str (" To = ");
- Write_Int (Int (ASR.To_Xref));
- Write_Eol;
- end;
- end loop;
+ -- Start of processing for dspark
+ begin
-- Dump SPARK cross-reference table
Write_Eol;
Write_Line ("SPARK Xref Table");
Write_Line ("----------------");
- for Index in SPARK_Xref_Table.First .. SPARK_Xref_Table.Last loop
- declare
- AXR : SPARK_Xref_Record renames SPARK_Xref_Table.Table (Index);
-
- begin
- Write_Str (" ");
- Write_Int (Int (Index));
- Write_Str (". Entity_Name = """);
-
- Write_Str (Unique_Name (AXR.Entity));
-
- Write_Char ('"');
- Write_Str (" Reference_Scope = ");
- Write_Str (Unique_Name (AXR.Ref_Scope));
- Write_Char ('"');
- Write_Str (" Type = ");
- Write_Char (AXR.Rtype);
- Write_Eol;
- end;
- end loop;
- end dspark;
-
- ----------------
- -- Initialize --
- ----------------
+ Dump_SPARK_Xrefs;
- procedure Initialize_SPARK_Tables is
- begin
- SPARK_File_Table.Init;
- SPARK_Scope_Table.Init;
- SPARK_Xref_Table.Init;
- end Initialize_SPARK_Tables;
+ end dspark;
end SPARK_Xrefs;
-- --
------------------------------------------------------------------------------
--- This package defines tables used to store information needed for the SPARK
--- mode. It is used by procedures in Lib.Xref.SPARK_Specific to build the
--- SPARK-specific cross-reference information.
+-- This package defines data structures used to expose frontend
+-- cross-references to the SPARK backend.
-with Table;
with Types; use Types;
package SPARK_Xrefs is
- -- SPARK cross-reference information is stored internally using three
- -- tables: SPARK_Xref_Table, SPARK_Scope_Table and SPARK_File_Table, which
- -- are defined in this unit.
-
- -- Lib.Xref.SPARK_Specific is part of the compiler. It extracts SPARK
- -- cross-reference information from the complete set of cross-references
- -- generated during compilation.
-
- -- -------------------------------
- -- -- Generated Globals Section --
- -- -------------------------------
-
- -- The Generated Globals section is located at the end of the ALI file
-
- -- All lines with information related to the Generated Globals begin with
- -- string "GG". This string should therefore not be used in the beginning
- -- of any line not related to Generated Globals.
-
- -- The processing (reading and writing) of this section happens in package
- -- Flow_Generated_Globals (from the SPARK 2014 sources), for further
- -- information please refer there.
-
- ----------------
- -- Xref Table --
- ----------------
-
- -- The following table records SPARK cross-references
-
- type Xref_Index is new Nat;
- -- Used to index values in this table. Values start at 1 and are assigned
- -- sequentially as entries are constructed; value 0 is used temporarily
- -- until a proper value is determined.
-
type SPARK_Xref_Record is record
Entity : Entity_Id;
-- Referenced entity
-- m = modification
-- s = call
end record;
-
- package SPARK_Xref_Table is new Table.Table (
- Table_Component_Type => SPARK_Xref_Record,
- Table_Index_Type => Xref_Index,
- Table_Low_Bound => 1,
- Table_Initial => 2000,
- Table_Increment => 300,
- Table_Name => "Xref_Table");
-
- -----------------
- -- Scope Table --
- -----------------
-
- -- This table keeps track of the scopes and the corresponding starting and
- -- ending indexes (From, To) in the Xref table.
-
- type Scope_Index is new Nat;
- -- Used to index values in this table. Values start at 1 and are assigned
- -- sequentially as entries are constructed; value 0 indicates that no
- -- entries have been constructed and is also used until a proper value is
- -- determined.
-
- type SPARK_Scope_Record is record
- Entity : Entity_Id;
- -- Entity that is represented by the scope
-
- Scope_Num : Pos;
- -- Set to the scope number within the enclosing unit
-
- From_Xref : Xref_Index;
- -- Starting index in Xref table for this scope
-
- To_Xref : Xref_Index;
- -- Ending index in Xref table for this scope
- end record;
-
- package SPARK_Scope_Table is new Table.Table (
- Table_Component_Type => SPARK_Scope_Record,
- Table_Index_Type => Scope_Index,
- Table_Low_Bound => 1,
- Table_Initial => 200,
- Table_Increment => 300,
- Table_Name => "Scope_Table");
-
- ----------------
- -- File Table --
- ----------------
-
- -- This table keeps track of the units and the corresponding starting and
- -- ending indexes (From, To) in the Scope table.
-
- type File_Index is new Nat;
- -- Used to index values in this table. Values start at 1 and are assigned
- -- sequentially as entries are constructed; value 0 indicates that no
- -- entries have been constructed.
-
- type SPARK_File_Record is record
- File_Num : Nat;
- -- Dependency number in ALI file
-
- From_Scope : Scope_Index;
- -- Starting index in Scope table for this unit
-
- To_Scope : Scope_Index;
- -- Ending index in Scope table for this unit
- end record;
-
- package SPARK_File_Table is new Table.Table (
- Table_Component_Type => SPARK_File_Record,
- Table_Index_Type => File_Index,
- Table_Low_Bound => 1,
- Table_Initial => 20,
- Table_Increment => 200,
- Table_Name => "File_Table");
+ -- This type holds a subset of the frontend xref entry that is needed by
+ -- the SPARK backend.
---------------
-- Constants --
-- Subprograms --
-----------------
- procedure Initialize_SPARK_Tables;
- -- Reset tables for a new compilation
-
procedure dspark;
-- Debug routine to dump internal SPARK cross-reference tables. This is a
-- raw format dump showing exactly what the tables contain.
when 'C' =>
Ptr := Ptr + 1;
-
- if not CodePeer_Mode then
- CodePeer_Mode := True;
-
- -- Suppress compiler warnings by default, since what we are
- -- interested in here is what CodePeer can find out. Note
- -- that if -gnatwxxx is specified after -gnatC on the
- -- command line, we do not want to override this setting in
- -- Adjust_Global_Switches, and assume that the user wants to
- -- get both warnings from GNAT and CodePeer messages.
-
- Warning_Mode := Suppress;
- end if;
+ CodePeer_Mode := True;
-- -gnatd (compiler debug options)
+2017-11-09 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * gnat.dg/elab3.adb, gnat.dg/elab3.ads, gnat.dg/elab3_pkg.adb,
+ gnat.dg/elab3_pkg.ads: New testcase.
+
+2017-11-09 Pierre-Marie de Rodat <derodat@adacore.com>
+
+ * gnat.dg/controlled2.adb, gnat.dg/controlled4.adb, gnat.dg/finalized.adb:
+ Disable the new warning from GNAT.
+
2017-11-09 Jakub Jelinek <jakub@redhat.com>
PR debug/82837
-- { dg-do compile }
+pragma Warnings
+ (Off, "anonymous access-to-controlled object will be finalized when its enclosing unit goes out of scope");
+
with controlled1; use controlled1;
package body controlled2 is
procedure Test_Suite is
-- { dg-do compile }
+pragma Warnings
+ (Off, "anonymous access-to-controlled object will be finalized when its enclosing unit goes out of scope");
+
package body controlled4 is
procedure Test_Suite is
begin
--- /dev/null
+-- { dg-do compile }
+
+with Elab3_Pkg;
+
+package body Elab3 is
+ package Inst is new Elab3_Pkg (False, ABE);
+
+ procedure ABE is begin null; end ABE;
+end Elab3;
--- /dev/null
+package Elab3 is
+ procedure ABE;
+end Elab3;
--- /dev/null
+package body Elab3_Pkg is
+ procedure Elaborator is
+ begin
+ Proc;
+ end Elaborator;
+
+begin
+ if Elaborate then
+ Elaborator;
+ end if;
+end Elab3_Pkg;
--- /dev/null
+generic
+ Elaborate : Boolean := True;
+ with procedure Proc;
+
+package Elab3_Pkg is
+ procedure Elaborator;
+end Elab3_Pkg;
-- { dg-do compile }
+pragma Warnings
+ (Off, "anonymous access-to-controlled object will be finalized when its enclosing unit goes out of scope");
+
with Ada.Finalization; use Ada.Finalization;
procedure finalized is
type Rec is new Controlled with null record;
git://gcc.gnu.org / gcc.git / commitdiff