+2017-11-08 Javier Miranda <miranda@adacore.com>
+
+ * sem_disp.adb (Is_Inherited_Public_Operation): Extend the
+ functionality of this routine to handle multiple levels of derivations.
+
+2017-11-08 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * einfo.adb: Elist36 is now used as Nested_Scenarios.
+ (Nested_Scenarios): New routine.
+ (Set_Nested_Scenarios): New routine.
+ (Write_Field36_Name): New routine.
+ * einfo.ads: Add new attribute Nested_Scenarios along with occurrences
+ in entities.
+ (Nested_Scenarios): New routine along with pragma Inline.
+ (Set_Nested_Scenarios): New routine along with pragma Inline.
+ * sem_elab.adb (Find_And_Process_Nested_Scenarios): New routine.
+ (Process_Nested_Scenarios): New routine.
+ (Traverse_Body): When a subprogram body is traversed for the first
+ time, find, save, and process all suitable scenarios found within.
+ Subsequent traversals of the same subprogram body utilize the saved
+ scenarios.
+
+2017-11-08 Piotr Trojanek <trojanek@adacore.com>
+
+ * lib-xref-spark_specific.adb (Add_SPARK_Scope): Remove detection of
+ protected operations.
+ (Add_SPARK_Xrefs): Simplify detection of empty entities.
+ * get_spark_xrefs.ads, get_spark_xrefs.adb, put_spark_xrefs.ads,
+ put_spark_xrefs.adb, spark_xrefs_test.adb: Remove code for writing,
+ reading and testing SPARK cross-references stored in the ALI files.
+ * lib-xref.ads (Output_SPARK_Xrefs): Remove.
+ * lib-writ.adb (Write_ALI): Do not write SPARK cross-references to the
+ ALI file.
+ * spark_xrefs.ads, spark_xrefs.adb (pspark): Remove, together
+ with description of the SPARK xrefs ALI format.
+ * gcc-interface/Make-lang.in (GNAT_ADA_OBJS): Remove get_spark_refs.o
+ and put_spark_refs.o.
+
+2017-11-08 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * exp_ch4.adb (Apply_Accessibility_Check): Do not finalize the object
+ when the associated access type is subject to pragma
+ No_Heap_Finalization.
+ * exp_intr.adb (Expand_Unc_Deallocation): Use the available view of the
+ designated type in case it comes from a limited withed unit.
+
2017-11-08 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch3.adb (Expand_N_Object_Declaration): Save and restore relevant
-- Entry_Max_Queue_Lengths_Array Node35
-- Import_Pragma Node35
+ -- Nested_Scenarios Elist36
-- Validated_Object Node36
-- Class_Wide_Clone Node38
return Flag22 (Id);
end Needs_No_Actuals;
+ function Nested_Scenarios (Id : E) return L is
+ begin
+ pragma Assert (Ekind_In (Id, E_Function,
+ E_Procedure,
+ E_Subprogram_Body));
+ return Elist36 (Id);
+ end Nested_Scenarios;
+
function Never_Set_In_Source (Id : E) return B is
begin
return Flag115 (Id);
Set_Flag22 (Id, V);
end Set_Needs_No_Actuals;
+ procedure Set_Nested_Scenarios (Id : E; V : L) is
+ begin
+ pragma Assert (Ekind_In (Id, E_Function,
+ E_Procedure,
+ E_Subprogram_Body));
+ Set_Elist36 (Id, V);
+ end Set_Nested_Scenarios;
+
procedure Set_Never_Set_In_Source (Id : E; V : B := True) is
begin
Set_Flag115 (Id, V);
procedure Write_Field36_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
+ when E_Function
+ | E_Procedure
+ | E_Subprogram_Body
+ =>
+ Write_Str ("Nested_Scenarios");
+
when E_Variable =>
Write_Str ("Validated_Object");
-- interpreted as an indexing of the result of the call. It is also
-- used to resolve various cases of entry calls.
+-- Nested_Scenarios (Elist36)
+-- Present in [stand alone] subprogram bodies. The list contains all
+-- nested scenarios (see the terminology in Sem_Elab) which appear within
+-- the declarations, statements, and exception handlers of the subprogram
+-- body. The list improves the performance of the ABE Processing phase by
+-- avoiding a full tree traversal when the same subprogram body is part
+-- of several distinct paths in the elaboration graph.
+
-- Never_Set_In_Source (Flag115)
-- Defined in all entities, but can be set only for variables and
-- parameters. This flag is set if the object is never assigned a value
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
-- Import_Pragma (Node35) (non-generic case only)
+ -- Nested_Scenarios (Elist36)
-- Class_Wide_Clone (Node38)
-- Protected_Subprogram (Node39) (non-generic case only)
-- SPARK_Pragma (Node40)
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
-- Import_Pragma (Node35) (non-generic case only)
+ -- Nested_Scenarios (Elist36)
-- Class_Wide_Clone (Node38)
-- Protected_Subprogram (Node39) (non-generic case only)
-- SPARK_Pragma (Node40)
-- Extra_Formals (Node28)
-- Anonymous_Masters (Elist29)
-- Contract (Node34)
+ -- Nested_Scenarios (Elist36)
-- SPARK_Pragma (Node40)
-- Contains_Ignored_Ghost_Code (Flag279)
-- SPARK_Pragma_Inherited (Flag265)
function Must_Have_Preelab_Init (Id : E) return B;
function Needs_Debug_Info (Id : E) return B;
function Needs_No_Actuals (Id : E) return B;
+ function Nested_Scenarios (Id : E) return L;
function Never_Set_In_Source (Id : E) return B;
function Next_Inlined_Subprogram (Id : E) return E;
function No_Dynamic_Predicate_On_Actual (Id : E) return B;
procedure Set_Must_Have_Preelab_Init (Id : E; V : B := True);
procedure Set_Needs_Debug_Info (Id : E; V : B := True);
procedure Set_Needs_No_Actuals (Id : E; V : B := True);
+ procedure Set_Nested_Scenarios (Id : E; V : L);
procedure Set_Never_Set_In_Source (Id : E; V : B := True);
procedure Set_Next_Inlined_Subprogram (Id : E; V : E);
procedure Set_No_Dynamic_Predicate_On_Actual (Id : E; V : B := True);
pragma Inline (Must_Have_Preelab_Init);
pragma Inline (Needs_Debug_Info);
pragma Inline (Needs_No_Actuals);
+ pragma Inline (Nested_Scenarios);
pragma Inline (Never_Set_In_Source);
pragma Inline (Next_Index);
pragma Inline (Next_Inlined_Subprogram);
pragma Inline (Set_Must_Have_Preelab_Init);
pragma Inline (Set_Needs_Debug_Info);
pragma Inline (Set_Needs_No_Actuals);
+ pragma Inline (Set_Nested_Scenarios);
pragma Inline (Set_Never_Set_In_Source);
pragma Inline (Set_Next_Inlined_Subprogram);
pragma Inline (Set_No_Dynamic_Predicate_On_Actual);
-- [Deep_]Finalize (Obj_Ref.all);
- if Needs_Finalization (DesigT) then
+ if Needs_Finalization (DesigT)
+ and then not No_Heap_Finalization (PtrT)
+ then
Fin_Call :=
Make_Final_Call
(Obj_Ref =>
Arg : constant Node_Id := First_Actual (N);
Loc : constant Source_Ptr := Sloc (N);
Typ : constant Entity_Id := Etype (Arg);
- Desig_Typ : constant Entity_Id := Designated_Type (Typ);
+ Desig_Typ : constant Entity_Id :=
+ Available_View (Designated_Type (Typ));
Needs_Fin : constant Boolean := Needs_Finalization (Desig_Typ);
Root_Typ : constant Entity_Id := Underlying_Type (Root_Type (Typ));
Pool : constant Entity_Id := Associated_Storage_Pool (Root_Typ);
ada/libgnat/g-spchge.o \
ada/libgnat/g-speche.o \
ada/libgnat/g-u3spch.o \
- ada/get_spark_xrefs.o \
ada/get_targ.o \
ada/ghost.o \
ada/libgnat/gnat.o \
ada/par_sco.o \
ada/prep.o \
ada/prepcomp.o \
- ada/put_spark_xrefs.o \
ada/put_scos.o \
ada/repinfo.o \
ada/restrict.o \
+++ /dev/null
-------------------------------------------------------------------------------
--- --
--- GNAT COMPILER COMPONENTS --
--- --
--- G E T _ S P A R K _ X R E F S --
--- --
--- B o d y --
--- --
--- Copyright (C) 2011-2016, Free Software Foundation, Inc. --
--- --
--- GNAT is free software; you can redistribute it and/or modify it under --
--- terms of the GNU General Public License as published by the Free Soft- --
--- ware Foundation; either version 3, or (at your option) any later ver- --
--- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
--- for more details. You should have received a copy of the GNU General --
--- Public License distributed with GNAT; see file COPYING3. If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license. --
--- --
--- GNAT was originally developed by the GNAT team at New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc. --
--- --
-------------------------------------------------------------------------------
-
-with SPARK_Xrefs; use SPARK_Xrefs;
-with Types; use Types;
-
-with Ada.IO_Exceptions; use Ada.IO_Exceptions;
-
-procedure Get_SPARK_Xrefs is
- C : Character;
-
- use ASCII;
- -- For CR/LF
-
- Cur_File : Nat;
- -- Dependency number for the current file
-
- Cur_Scope : Nat;
- -- Scope number for the current scope entity
-
- Cur_File_Idx : File_Index;
- -- Index in SPARK_File_Table of the current file
-
- Cur_Scope_Idx : Scope_Index;
- -- Index in SPARK_Scope_Table of the current scope
-
- Name_Str : String (1 .. 32768);
- Name_Len : Natural := 0;
- -- Local string used to store name of File/entity scanned as
- -- Name_Str (1 .. Name_Len).
-
- File_Name : String_Ptr;
- Unit_File_Name : String_Ptr;
-
- -----------------------
- -- Local Subprograms --
- -----------------------
-
- function At_EOL return Boolean;
- -- Skips any spaces, then checks if at the end of a line. If so, returns
- -- True (but does not skip the EOL sequence). If not, then returns False.
-
- procedure Check (C : Character);
- -- Checks that file is positioned at given character, and if so skips past
- -- it, If not, raises Data_Error.
-
- function Get_Nat return Nat;
- -- On entry the file is positioned to a digit. On return, the file is
- -- positioned past the last digit, and the returned result is the decimal
- -- value read. Data_Error is raised for overflow (value greater than
- -- Int'Last), or if the initial character is not a digit.
-
- procedure Get_Name;
- -- On entry the file is positioned to a name. On return, the file is
- -- positioned past the last character, and the name scanned is returned
- -- in Name_Str (1 .. Name_Len).
-
- procedure Skip_EOL;
- -- Called with the current character about to be read being LF or CR. Skips
- -- past CR/LF characters until either a non-CR/LF character is found, or
- -- the end of file is encountered.
-
- procedure Skip_Spaces;
- -- Skips zero or more spaces at the current position, leaving the file
- -- positioned at the first non-blank character (or Types.EOF).
-
- ------------
- -- At_EOL --
- ------------
-
- function At_EOL return Boolean is
- begin
- Skip_Spaces;
- return Nextc = CR or else Nextc = LF;
- end At_EOL;
-
- -----------
- -- Check --
- -----------
-
- procedure Check (C : Character) is
- begin
- if Nextc = C then
- Skipc;
- else
- raise Data_Error;
- end if;
- end Check;
-
- -------------
- -- Get_Nat --
- -------------
-
- function Get_Nat return Nat is
- C : Character := Nextc;
- Val : Nat := 0;
-
- begin
- if C not in '0' .. '9' then
- raise Data_Error;
- end if;
-
- -- Loop to read digits of integer value
-
- loop
- declare
- pragma Unsuppress (Overflow_Check);
- begin
- Val := Val * 10 + (Character'Pos (C) - Character'Pos ('0'));
- end;
-
- Skipc;
- C := Nextc;
-
- exit when C not in '0' .. '9';
- end loop;
-
- return Val;
-
- exception
- when Constraint_Error =>
- raise Data_Error;
- end Get_Nat;
-
- --------------
- -- Get_Name --
- --------------
-
- procedure Get_Name is
- N : Natural := 0;
-
- begin
- while Nextc > ' ' loop
- N := N + 1;
- Name_Str (N) := Getc;
- end loop;
-
- Name_Len := N;
- end Get_Name;
-
- --------------
- -- Skip_EOL --
- --------------
-
- procedure Skip_EOL is
- C : Character;
-
- begin
- loop
- Skipc;
- C := Nextc;
- exit when C /= LF and then C /= CR;
-
- if C = ' ' then
- Skip_Spaces;
- C := Nextc;
- exit when C /= LF and then C /= CR;
- end if;
- end loop;
- end Skip_EOL;
-
- -----------------
- -- Skip_Spaces --
- -----------------
-
- procedure Skip_Spaces is
- begin
- while Nextc = ' ' loop
- Skipc;
- end loop;
- end Skip_Spaces;
-
--- Start of processing for Get_SPARK_Xrefs
-
-begin
- Initialize_SPARK_Tables;
-
- Cur_File := 0;
- Cur_Scope := 0;
- Cur_File_Idx := 1;
- Cur_Scope_Idx := 0;
-
- -- Loop through lines of SPARK cross-reference information
-
- while Nextc = 'F' loop
- Skipc;
-
- C := Getc;
-
- -- Make sure first line is a File line
-
- if SPARK_File_Table.Last = 0 and then C /= 'D' then
- raise Data_Error;
- end if;
-
- -- Otherwise dispatch on type of line
-
- case C is
-
- -- Header entry for scope section
-
- when 'D' =>
-
- -- Complete previous entry if any
-
- if SPARK_File_Table.Last /= 0 then
- SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope :=
- SPARK_Scope_Table.Last;
- end if;
-
- -- Scan out dependency number and file name
-
- Skip_Spaces;
- Cur_File := Get_Nat;
- Skip_Spaces;
-
- Get_Name;
- File_Name := new String'(Name_Str (1 .. Name_Len));
- Skip_Spaces;
-
- -- Scan out unit file name when present (for subunits)
-
- if Nextc = '-' then
- Skipc;
- Check ('>');
- Skip_Spaces;
- Get_Name;
- Unit_File_Name := new String'(Name_Str (1 .. Name_Len));
-
- else
- Unit_File_Name := null;
- end if;
-
- -- Make new File table entry (will fill in To_Scope later)
-
- SPARK_File_Table.Append (
- (File_Name => File_Name,
- Unit_File_Name => Unit_File_Name,
- File_Num => Cur_File,
- From_Scope => SPARK_Scope_Table.Last + 1,
- To_Scope => 0));
-
- -- Initialize counter for scopes
-
- Cur_Scope := 1;
-
- -- Scope entry
-
- when 'S' =>
- declare
- Spec_File : Nat;
- Spec_Scope : Nat;
- Scope : Nat;
- Line : Nat;
- Col : Nat;
- Typ : Character;
-
- begin
- -- Scan out location
-
- Skip_Spaces;
- Check ('.');
- Scope := Get_Nat;
- Check (' ');
- Line := Get_Nat;
- Typ := Getc;
- Col := Get_Nat;
-
- pragma Assert (Scope = Cur_Scope);
-
- -- Scan out scope entity name
-
- Skip_Spaces;
- Get_Name;
- Skip_Spaces;
-
- if Nextc = '-' then
- Skipc;
- Check ('>');
- Skip_Spaces;
- Spec_File := Get_Nat;
- Check ('.');
- Spec_Scope := Get_Nat;
-
- else
- Spec_File := 0;
- Spec_Scope := 0;
- end if;
-
- -- Make new scope table entry (will fill in From_Xref and
- -- To_Xref later). Initial range (From_Xref .. To_Xref) is
- -- empty for scopes without entities.
-
- SPARK_Scope_Table.Append (
- (Scope_Entity => Empty,
- Scope_Name => new String'(Name_Str (1 .. Name_Len)),
- File_Num => Cur_File,
- Scope_Num => Cur_Scope,
- Spec_File_Num => Spec_File,
- Spec_Scope_Num => Spec_Scope,
- Line => Line,
- Stype => Typ,
- Col => Col,
- From_Xref => 1,
- To_Xref => 0));
- end;
-
- -- Update counter for scopes
-
- Cur_Scope := Cur_Scope + 1;
-
- -- Header entry for cross-ref section
-
- when 'X' =>
-
- -- Scan out dependency number and file name (ignored)
-
- Skip_Spaces;
- Cur_File := Get_Nat;
- Skip_Spaces;
- Get_Name;
-
- -- Update component From_Xref of current file if first reference
- -- in this file.
-
- while SPARK_File_Table.Table (Cur_File_Idx).File_Num /= Cur_File
- loop
- Cur_File_Idx := Cur_File_Idx + 1;
- end loop;
-
- -- Scan out scope entity number and entity name (ignored)
-
- Skip_Spaces;
- Check ('.');
- Cur_Scope := Get_Nat;
- Skip_Spaces;
- Get_Name;
-
- -- Update component To_Xref of previous scope
-
- if Cur_Scope_Idx /= 0 then
- SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref :=
- SPARK_Xref_Table.Last;
- end if;
-
- -- Update component From_Xref of current scope
-
- Cur_Scope_Idx := SPARK_File_Table.Table (Cur_File_Idx).From_Scope;
-
- while SPARK_Scope_Table.Table (Cur_Scope_Idx).Scope_Num /=
- Cur_Scope
- loop
- Cur_Scope_Idx := Cur_Scope_Idx + 1;
- end loop;
-
- SPARK_Scope_Table.Table (Cur_Scope_Idx).From_Xref :=
- SPARK_Xref_Table.Last + 1;
-
- -- Cross reference entry
-
- when ' ' =>
- declare
- XR_Entity : String_Ptr;
- XR_Entity_Line : Nat;
- XR_Entity_Col : Nat;
- XR_Entity_Typ : Character;
-
- XR_File : Nat;
- -- Keeps track of the current file (changed by nn|)
-
- XR_Scope : Nat;
- -- Keeps track of the current scope (changed by nn:)
-
- begin
- XR_File := Cur_File;
- XR_Scope := Cur_Scope;
-
- XR_Entity_Line := Get_Nat;
- XR_Entity_Typ := Getc;
- XR_Entity_Col := Get_Nat;
-
- Skip_Spaces;
- Get_Name;
- XR_Entity := new String'(Name_Str (1 .. Name_Len));
-
- -- Initialize to scan items on one line
-
- Skip_Spaces;
-
- -- Loop through cross-references for this entity
-
- loop
- declare
- Line : Nat;
- Col : Nat;
- N : Nat;
- Rtype : Character;
-
- begin
- Skip_Spaces;
-
- if At_EOL then
- Skip_EOL;
- exit when Nextc /= '.';
- Skipc;
- Skip_Spaces;
- end if;
-
- if Nextc = '.' then
- Skipc;
- XR_Scope := Get_Nat;
- Check (':');
-
- else
- N := Get_Nat;
-
- if Nextc = '|' then
- XR_File := N;
- Skipc;
-
- else
- Line := N;
- Rtype := Getc;
- Col := Get_Nat;
-
- pragma Assert
- (Rtype = 'r' or else
- Rtype = 'c' or else
- Rtype = 'm' or else
- Rtype = 's');
-
- SPARK_Xref_Table.Append (
- (Entity_Name => XR_Entity,
- Entity_Line => XR_Entity_Line,
- Etype => XR_Entity_Typ,
- Entity_Col => XR_Entity_Col,
- File_Num => XR_File,
- Scope_Num => XR_Scope,
- Line => Line,
- Rtype => Rtype,
- Col => Col));
- end if;
- end if;
- end;
- end loop;
- end;
-
- -- No other SPARK lines are possible
-
- when others =>
- raise Data_Error;
- end case;
-
- -- For cross reference lines, the EOL character has been skipped already
-
- if C /= ' ' then
- Skip_EOL;
- end if;
- end loop;
-
- -- Here with all Xrefs stored, complete last entries in File/Scope tables
-
- if SPARK_File_Table.Last /= 0 then
- SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope :=
- SPARK_Scope_Table.Last;
- end if;
-
- if Cur_Scope_Idx /= 0 then
- SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref := SPARK_Xref_Table.Last;
- end if;
-end Get_SPARK_Xrefs;
+++ /dev/null
-------------------------------------------------------------------------------
--- --
--- GNAT COMPILER COMPONENTS --
--- --
--- G E T _ S P A R K _ X R E F S --
--- --
--- S p e c --
--- --
--- Copyright (C) 2011-2013, Free Software Foundation, Inc. --
--- --
--- GNAT is free software; you can redistribute it and/or modify it under --
--- terms of the GNU General Public License as published by the Free Soft- --
--- ware Foundation; either version 3, or (at your option) any later ver- --
--- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
--- for more details. You should have received a copy of the GNU General --
--- Public License distributed with GNAT; see file COPYING3. If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license. --
--- --
--- GNAT was originally developed by the GNAT team at New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc. --
--- --
-------------------------------------------------------------------------------
-
--- This package contains the function used to read SPARK cross-reference
--- information from an ALI file and populate the tables defined in package
--- SPARK_Xrefs with the result.
-
-generic
- -- These subprograms provide access to the ALI file. Locating, opening and
- -- providing access to the ALI file is the callers' responsibility.
-
- with function Getc return Character is <>;
- -- Get next character, positioning the ALI file ready to read the following
- -- character (equivalent to calling Nextc, then Skipc). If the end of file
- -- is encountered, the value Types.EOF is returned.
-
- with function Nextc return Character is <>;
- -- Look at the next character, and return it, leaving the position of the
- -- file unchanged, so that a subsequent call to Getc or Nextc will return
- -- this same character. If the file is positioned at the end of file, then
- -- Types.EOF is returned.
-
- with procedure Skipc is <>;
- -- Skip past the current character (which typically was read with Nextc),
- -- and position to the next character, which will be returned by the next
- -- call to Getc or Nextc.
-
-procedure Get_SPARK_Xrefs;
--- Load SPARK cross-reference information from ALI file text format into
--- internal SPARK tables (SPARK_Xrefs.SPARK_Xref_Table,
--- SPARK_Xrefs.SPARK_Scope_Table and SPARK_Xrefs.SPARK_File_Table). On entry
--- the input file is positioned to the initial 'F' of the first SPARK specific
--- line in the ALI file. On return, the file is positioned either to the end
--- of file, or to the first character of the line following the SPARK specific
--- information (which will never start with an 'F').
---
--- If a format error is detected in the input, then an exception is raised
--- (Ada.IO_Exceptions.Data_Error), with the file positioned to the error.
if Opt.Xref_Active and then GNATprove_Mode then
SPARK_Specific.Collect_SPARK_Xrefs (Sdep_Table => Sdep_Table,
Num_Sdep => Num_Sdep);
- SPARK_Specific.Output_SPARK_Xrefs;
end if;
-- Output final blank line and we are done. This final blank line is
case Ekind (E) is
when E_Entry
| E_Entry_Family
+ | E_Function
| E_Generic_Function
| E_Generic_Package
| E_Generic_Procedure
| E_Package
+ | E_Procedure
| E_Protected_Type
| E_Task_Type
=>
Typ := Xref_Entity_Letters (Ekind (E));
- when E_Function
- | E_Procedure
- =>
- -- In SPARK we need to distinguish protected functions and
- -- procedures from ordinary subprograms, but there are no
- -- special Xref letters for them. Since this distiction is
- -- only needed to detect protected calls, we pretend that
- -- such calls are entry calls.
-
- if Ekind (Scope (E)) = E_Protected_Type then
- Typ := Xref_Entity_Letters (E_Entry);
- else
- Typ := Xref_Entity_Letters (Ekind (E));
- end if;
-
when E_Package_Body
| E_Protected_Body
| E_Subprogram_Body
Prev_Loc : Source_Ptr;
Prev_Typ : Character;
Ref_Count : Nat;
- Ref_Id : Entity_Id;
Ref_Name : String_Ptr;
Scope_Id : Scope_Index;
return;
end if;
- Ref_Id := Empty;
Scope_Id := 1;
From_Index := 1;
pragma Assert (Scope_Id <= SPARK_Scope_Table.Last);
end loop;
- if Ref.Ent /= Ref_Id then
+ if Present (Ref.Ent) then
Ref_Name := new String'(Unique_Name (Ref.Ent));
end if;
with Csets; use Csets;
with Elists; use Elists;
with Errout; use Errout;
+with Lib.Util; use Lib.Util;
with Nlists; use Nlists;
with Opt; use Opt;
with Restrict; use Restrict;
-- This package contains for collecting and outputting cross-reference
-- information.
-with Einfo; use Einfo;
-with Lib.Util; use Lib.Util;
-with Put_SPARK_Xrefs;
+with Einfo; use Einfo;
package Lib.Xref is
-- files and scopes) and from shared cross-references. Fill in the
-- tables in library package called SPARK_Xrefs.
- procedure Output_SPARK_Xrefs is new Put_SPARK_Xrefs;
- -- Output SPARK cross-reference information to the ALI files, based on
- -- the information collected in the tables in library package called
- -- SPARK_Xrefs, and using routines in Lib.Util.
-
generic
with procedure Process (N : Node_Id) is <>;
procedure Traverse_Compilation_Unit
+++ /dev/null
-------------------------------------------------------------------------------
--- --
--- GNAT COMPILER COMPONENTS --
--- --
--- P U T _ S P A R K _ X R E F S --
--- --
--- B o d y --
--- --
--- Copyright (C) 2011-2016, Free Software Foundation, Inc. --
--- --
--- GNAT is free software; you can redistribute it and/or modify it under --
--- terms of the GNU General Public License as published by the Free Soft- --
--- ware Foundation; either version 3, or (at your option) any later ver- --
--- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
--- for more details. You should have received a copy of the GNU General --
--- Public License distributed with GNAT; see file COPYING3. If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license. --
--- --
--- GNAT was originally developed by the GNAT team at New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc. --
--- --
-------------------------------------------------------------------------------
-
-with SPARK_Xrefs; use SPARK_Xrefs;
-
-procedure Put_SPARK_Xrefs is
-begin
- -- Loop through entries in SPARK_File_Table
-
- for J in 1 .. SPARK_File_Table.Last loop
- declare
- F : SPARK_File_Record renames SPARK_File_Table.Table (J);
-
- begin
- Write_Info_Initiate ('F');
- Write_Info_Char ('D');
- Write_Info_Char (' ');
- Write_Info_Nat (F.File_Num);
- Write_Info_Char (' ');
-
- Write_Info_Str (F.File_Name.all);
-
- -- If file is a subunit, print the file name for the unit
-
- if F.Unit_File_Name /= null then
- Write_Info_Str (" -> " & F.Unit_File_Name.all);
- end if;
-
- Write_Info_Terminate;
-
- -- Loop through scope entries for this file
-
- for J in F.From_Scope .. F.To_Scope loop
- declare
- S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (J);
-
- begin
- Write_Info_Initiate ('F');
- Write_Info_Char ('S');
- Write_Info_Char (' ');
- Write_Info_Char ('.');
- Write_Info_Nat (S.Scope_Num);
- Write_Info_Char (' ');
- Write_Info_Nat (S.Line);
- Write_Info_Char (S.Stype);
- Write_Info_Nat (S.Col);
- Write_Info_Char (' ');
-
- pragma Assert (S.Scope_Name.all /= "");
-
- Write_Info_Str (S.Scope_Name.all);
-
- if S.Spec_File_Num /= 0 then
- Write_Info_Str (" -> ");
- Write_Info_Nat (S.Spec_File_Num);
- Write_Info_Char ('.');
- Write_Info_Nat (S.Spec_Scope_Num);
- end if;
-
- Write_Info_Terminate;
- end;
- end loop;
- end;
- end loop;
-
- -- Loop through entries in SPARK_File_Table
-
- for J in 1 .. SPARK_File_Table.Last loop
- declare
- F : SPARK_File_Record renames SPARK_File_Table.Table (J);
- File : Nat;
- Scope : Nat;
- Entity_Line : Nat;
- Entity_Col : Nat;
-
- begin
- -- Loop through scope entries for this file
-
- for K in F.From_Scope .. F.To_Scope loop
- Output_One_Scope : declare
- S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (K);
-
- begin
- -- Write only non-empty tables
-
- if S.From_Xref <= S.To_Xref then
-
- Write_Info_Initiate ('F');
- Write_Info_Char ('X');
- Write_Info_Char (' ');
- Write_Info_Nat (F.File_Num);
- Write_Info_Char (' ');
-
- Write_Info_Str (F.File_Name.all);
-
- Write_Info_Char (' ');
- Write_Info_Char ('.');
- Write_Info_Nat (S.Scope_Num);
- Write_Info_Char (' ');
-
- Write_Info_Str (S.Scope_Name.all);
-
- -- Default value of (0,0) is used for the special __HEAP
- -- variable so use another default value.
-
- Entity_Line := 0;
- Entity_Col := 1;
-
- -- Loop through cross reference entries for this scope
-
- for X in S.From_Xref .. S.To_Xref loop
-
- Output_One_Xref : declare
- R : SPARK_Xref_Record renames
- SPARK_Xref_Table.Table (X);
-
- begin
- if R.Entity_Line /= Entity_Line
- or else R.Entity_Col /= Entity_Col
- then
- Write_Info_Terminate;
-
- Write_Info_Initiate ('F');
- Write_Info_Char (' ');
- Write_Info_Nat (R.Entity_Line);
- Write_Info_Char (R.Etype);
- Write_Info_Nat (R.Entity_Col);
- Write_Info_Char (' ');
-
- Write_Info_Str (R.Entity_Name.all);
-
- Entity_Line := R.Entity_Line;
- Entity_Col := R.Entity_Col;
- File := F.File_Num;
- Scope := S.Scope_Num;
- end if;
-
- if Write_Info_Col > 72 then
- Write_Info_Terminate;
- Write_Info_Initiate ('.');
- end if;
-
- Write_Info_Char (' ');
-
- if R.File_Num /= File then
- Write_Info_Nat (R.File_Num);
- Write_Info_Char ('|');
- File := R.File_Num;
- Scope := 0;
- end if;
-
- if R.Scope_Num /= Scope then
- Write_Info_Char ('.');
- Write_Info_Nat (R.Scope_Num);
- Write_Info_Char (':');
- Scope := R.Scope_Num;
- end if;
-
- Write_Info_Nat (R.Line);
- Write_Info_Char (R.Rtype);
- Write_Info_Nat (R.Col);
- end Output_One_Xref;
-
- end loop;
-
- Write_Info_Terminate;
- end if;
- end Output_One_Scope;
- end loop;
- end;
- end loop;
-end Put_SPARK_Xrefs;
+++ /dev/null
-------------------------------------------------------------------------------
--- --
--- GNAT COMPILER COMPONENTS --
--- --
--- P U T _ S P A R K _ X R E F S --
--- --
--- S p e c --
--- --
--- Copyright (C) 2011-2016, Free Software Foundation, Inc. --
--- --
--- GNAT is free software; you can redistribute it and/or modify it under --
--- terms of the GNU General Public License as published by the Free Soft- --
--- ware Foundation; either version 3, or (at your option) any later ver- --
--- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
--- for more details. You should have received a copy of the GNU General --
--- Public License distributed with GNAT; see file COPYING3. If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license. --
--- --
--- GNAT was originally developed by the GNAT team at New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc. --
--- --
-------------------------------------------------------------------------------
-
--- This package contains the function used to read SPARK cross-reference
--- information from the internal tables defined in package SPARK_Xrefs, and
--- output text information for the ALI file. The interface allows control over
--- the destination of the output, so that this routine can also be used for
--- debugging purposes.
-
-with Types; use Types;
-
-generic
- -- The following procedures are used to output text information. The
- -- destination of the text information is thus under control of the
- -- particular instantiation. In particular, this procedure is used to
- -- write output to the ALI file, and also for debugging output.
-
- with function Write_Info_Col return Positive is <>;
- -- Return the column in which the next character will be written
-
- with procedure Write_Info_Char (C : Character) is <>;
- -- Output one character
-
- with procedure Write_Info_Str (Val : String) is <>;
- -- Output string stored in string pointer
-
- with procedure Write_Info_Initiate (Key : Character) is <>;
- -- Initiate write of new line to output file, the parameter is the
- -- keyword character for the line.
-
- with procedure Write_Info_Nat (N : Nat) is <>;
- -- Write image of N to output file with no leading or trailing blanks
-
- with procedure Write_Info_Terminate is <>;
- -- Terminate current info line and output lines built in Info_Buffer
-
-procedure Put_SPARK_Xrefs;
--- Read information from SPARK tables (SPARK_Xrefs.SPARK_Xref_Table,
--- SPARK_Xrefs.SPARK_Scope_Table and SPARK_Xrefs.SPARK_File_Table) and output
--- corresponding information in ALI format using the Write_Info procedures.
-----------------------------------
function Is_Inherited_Public_Operation (Op : Entity_Id) return Boolean is
- Prim : constant Entity_Id := Alias (Op);
- Scop : constant Entity_Id := Scope (Prim);
+ Prim : Entity_Id := Op;
+ Scop : Entity_Id := Prim;
Pack_Decl : Node_Id;
begin
+ -- Locate the ultimate non-hidden alias entity
+
+ while Present (Alias (Prim)) and then not Is_Hidden (Alias (Prim)) loop
+ pragma Assert (Alias (Prim) /= Prim);
+ Prim := Alias (Prim);
+ Scop := Scope (Prim);
+ end loop;
+
if Comes_From_Source (Prim) and then Ekind (Scop) = E_Package then
Pack_Decl := Unit_Declaration_Node (Scop);
return Nkind (Pack_Decl) = N_Package_Declaration
with Atree; use Atree;
with Debug; use Debug;
with Einfo; use Einfo;
+with Elists; use Elists;
with Errout; use Errout;
with Exp_Ch11; use Exp_Ch11;
with Exp_Tss; use Exp_Tss;
In_Partial_Fin : Boolean;
In_Task_Body : Boolean)
is
- function Is_Potential_Scenario (Nod : Node_Id) return Traverse_Result;
- -- Determine whether arbitrary node Nod denotes a suitable scenario and
- -- if so, process it.
+ procedure Find_And_Process_Nested_Scenarios;
+ pragma Inline (Find_And_Process_Nested_Scenarios);
+ -- Examine the declarations and statements of subprogram body N for
+ -- suitable scenarios. Save each discovered scenario and process it
+ -- accordingly.
+
+ procedure Process_Nested_Scenarios (Nested : Elist_Id);
+ pragma Inline (Process_Nested_Scenarios);
+ -- Invoke Process_Scenario on each individual scenario whith appears in
+ -- list Nested.
+
+ ---------------------------------------
+ -- Find_And_Process_Nested_Scenarios --
+ ---------------------------------------
+
+ procedure Find_And_Process_Nested_Scenarios is
+ Body_Id : constant Entity_Id := Defining_Entity (N);
+
+ function Is_Potential_Scenario
+ (Nod : Node_Id) return Traverse_Result;
+ -- Determine whether arbitrary node Nod denotes a suitable scenario.
+ -- If it does, save it in the Nested_Scenarios list of the subprogram
+ -- body, and process it.
+
+ procedure Save_Scenario (Nod : Node_Id);
+ pragma Inline (Save_Scenario);
+ -- Save scenario Nod in the Nested_Scenarios list of the subprogram
+ -- body.
- procedure Traverse_Potential_Scenarios is
- new Traverse_Proc (Is_Potential_Scenario);
+ procedure Traverse_List (List : List_Id);
+ pragma Inline (Traverse_List);
+ -- Invoke Traverse_Potential_Scenarios on each node in list List
- procedure Traverse_List (List : List_Id);
- -- Inspect list List for suitable elaboration scenarios and process them
+ procedure Traverse_Potential_Scenarios is
+ new Traverse_Proc (Is_Potential_Scenario);
- ---------------------------
- -- Is_Potential_Scenario --
- ---------------------------
+ ---------------------------
+ -- Is_Potential_Scenario --
+ ---------------------------
- function Is_Potential_Scenario (Nod : Node_Id) return Traverse_Result is
- begin
- -- Special cases
+ function Is_Potential_Scenario
+ (Nod : Node_Id) return Traverse_Result
+ is
+ begin
+ -- Special cases
- -- Skip constructs which do not have elaboration of their own and
- -- need to be elaborated by other means such as invocation, task
- -- activation, etc.
+ -- Skip constructs which do not have elaboration of their own and
+ -- need to be elaborated by other means such as invocation, task
+ -- activation, etc.
- if Is_Non_Library_Level_Encapsulator (Nod) then
- return Skip;
+ if Is_Non_Library_Level_Encapsulator (Nod) then
+ return Skip;
- -- Terminate the traversal of a task body with an accept statement
- -- when no entry calls in elaboration are allowed because the task
- -- will block at run-time and none of the remaining statements will
- -- be executed.
+ -- Terminate the traversal of a task body with an accept statement
+ -- when no entry calls in elaboration are allowed because the task
+ -- will block at run-time and the remaining statements will not be
+ -- executed.
- elsif Nkind_In (Original_Node (Nod), N_Accept_Statement,
- N_Selective_Accept)
- and then Restriction_Active (No_Entry_Calls_In_Elaboration_Code)
- then
- return Abandon;
+ elsif Nkind_In (Original_Node (Nod), N_Accept_Statement,
+ N_Selective_Accept)
+ and then Restriction_Active (No_Entry_Calls_In_Elaboration_Code)
+ then
+ return Abandon;
- -- Certain nodes carry semantic lists which act as repositories until
- -- expansion transforms the node and relocates the contents. Examine
- -- these lists in case expansion is disabled.
+ -- Certain nodes carry semantic lists which act as repositories
+ -- until expansion transforms the node and relocates the contents.
+ -- Examine these lists in case expansion is disabled.
- elsif Nkind_In (Nod, N_And_Then, N_Or_Else) then
- Traverse_List (Actions (Nod));
+ elsif Nkind_In (Nod, N_And_Then, N_Or_Else) then
+ Traverse_List (Actions (Nod));
- elsif Nkind_In (Nod, N_Elsif_Part, N_Iteration_Scheme) then
- Traverse_List (Condition_Actions (Nod));
+ elsif Nkind_In (Nod, N_Elsif_Part, N_Iteration_Scheme) then
+ Traverse_List (Condition_Actions (Nod));
- elsif Nkind (Nod) = N_If_Expression then
- Traverse_List (Then_Actions (Nod));
- Traverse_List (Else_Actions (Nod));
+ elsif Nkind (Nod) = N_If_Expression then
+ Traverse_List (Then_Actions (Nod));
+ Traverse_List (Else_Actions (Nod));
- elsif Nkind_In (Nod, N_Component_Association,
- N_Iterated_Component_Association)
- then
- Traverse_List (Loop_Actions (Nod));
+ elsif Nkind_In (Nod, N_Component_Association,
+ N_Iterated_Component_Association)
+ then
+ Traverse_List (Loop_Actions (Nod));
- -- General case
+ -- General case
- elsif Is_Suitable_Scenario (Nod) then
- Process_Scenario (Nod, In_Partial_Fin, In_Task_Body);
- end if;
+ -- 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
+ -- longer need to reexamine the tree.
+
+ elsif Is_Suitable_Scenario (Nod) then
+ Save_Scenario (Nod);
+ Process_Scenario (Nod, In_Partial_Fin, In_Task_Body);
+ end if;
- return OK;
- end Is_Potential_Scenario;
+ return OK;
+ end Is_Potential_Scenario;
- -------------------
- -- Traverse_List --
- -------------------
+ -------------------
+ -- Save_Scenario --
+ -------------------
- procedure Traverse_List (List : List_Id) is
- Item : Node_Id;
+ procedure Save_Scenario (Nod : Node_Id) is
+ Nested : Elist_Id;
+
+ begin
+ Nested := Nested_Scenarios (Body_Id);
+
+ if No (Nested) then
+ Nested := New_Elmt_List;
+ Set_Nested_Scenarios (Body_Id, Nested);
+ end if;
+
+ Append_Elmt (Nod, Nested);
+ end Save_Scenario;
+
+ -------------------
+ -- Traverse_List --
+ -------------------
+
+ procedure Traverse_List (List : List_Id) is
+ Item : Node_Id;
+
+ begin
+ Item := First (List);
+ while Present (Item) loop
+ Traverse_Potential_Scenarios (Item);
+ Next (Item);
+ end loop;
+ end Traverse_List;
+
+ -- Start of processing for Find_And_Process_Nested_Scenarios
begin
- Item := First (List);
- while Present (Item) loop
- Traverse_Potential_Scenarios (Item);
- Next (Item);
+ -- Examine the declarations for suitable scenarios
+
+ Traverse_List (Declarations (N));
+
+ -- Examine the handled sequence of statements. This also includes any
+ -- exceptions handlers.
+
+ Traverse_Potential_Scenarios (Handled_Statement_Sequence (N));
+ end Find_And_Process_Nested_Scenarios;
+
+ ------------------------------
+ -- Process_Nested_Scenarios --
+ ------------------------------
+
+ procedure Process_Nested_Scenarios (Nested : Elist_Id) is
+ Nested_Elmt : Elmt_Id;
+
+ begin
+ Nested_Elmt := First_Elmt (Nested);
+ while Present (Nested_Elmt) loop
+ Process_Scenario
+ (N => Node (Nested_Elmt),
+ In_Partial_Fin => In_Partial_Fin,
+ In_Task_Body => In_Task_Body);
+
+ Next_Elmt (Nested_Elmt);
end loop;
- end Traverse_List;
+ end Process_Nested_Scenarios;
+
+ -- Local variables
+
+ Nested : Elist_Id;
-- Start of processing for Traverse_Body
Visited_Bodies.Set (N, True);
end if;
- -- Examine the declarations for suitable scenarios
+ Nested := Nested_Scenarios (Defining_Entity (N));
- Traverse_List (Declarations (N));
+ -- The subprogram body was already examined as part of the elaboration
+ -- 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.
- -- Examine the handled sequence of statements. This also includes any
- -- exceptions handlers.
+ if Present (Nested) then
+ Process_Nested_Scenarios (Nested);
- Traverse_Potential_Scenarios (Handled_Statement_Sequence (N));
+ -- Otherwise examine the declarations and statements of the subprogram
+ -- body for suitable scenarios, save and process them accordingly.
+
+ else
+ Find_And_Process_Nested_Scenarios;
+ end if;
end Traverse_Body;
---------------------------------
-- --
-- B o d y --
-- --
--- Copyright (C) 2011-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 2011-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- --
------------------------------------------------------------------------------
-with Output; use Output;
-with Put_SPARK_Xrefs;
+with Output; use Output;
package body SPARK_Xrefs is
SPARK_Xref_Table.Init;
end Initialize_SPARK_Tables;
- ------------
- -- pspark --
- ------------
-
- procedure pspark is
-
- procedure Write_Info_Char (C : Character) renames Write_Char;
- -- Write one character
-
- procedure Write_Info_Str (Val : String) renames Write_Str;
- -- Write string
-
- function Write_Info_Col return Positive;
- -- Return next column for writing
-
- procedure Write_Info_Initiate (Key : Character) renames Write_Char;
- -- Start new one and write one character;
-
- procedure Write_Info_Nat (N : Nat);
- -- Write value of N
-
- procedure Write_Info_Terminate renames Write_Eol;
- -- Terminate current line
-
- --------------------
- -- Write_Info_Col --
- --------------------
-
- function Write_Info_Col return Positive is
- begin
- return Positive (Column);
- end Write_Info_Col;
-
- --------------------
- -- Write_Info_Nat --
- --------------------
-
- procedure Write_Info_Nat (N : Nat) is
- begin
- Write_Int (N);
- end Write_Info_Nat;
-
- procedure Debug_Put_SPARK_Xrefs is new Put_SPARK_Xrefs;
-
- -- Start of processing for pspark
-
- begin
- Debug_Put_SPARK_Xrefs;
- end pspark;
-
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 before writing it to the ALI
--- file, and by Get_SPARK_Xrefs/Put_SPARK_Xrefs to read/write the textual
--- representation that is stored in the ALI file.
+-- SPARK-specific cross-reference information.
with Table;
-with Types; use Types;
+with Types; use Types;
package SPARK_Xrefs is
- -- SPARK cross-reference information can exist in one of two forms. In
- -- the ALI file, it is represented using a text format that is described
- -- in this specification. Internally it is stored using three tables:
- -- SPARK_Xref_Table, SPARK_Scope_Table and SPARK_File_Table, which are
- -- also defined in this unit.
+ -- 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.
- -- Get_SPARK_Xrefs reads the text lines in ALI format and populates the
- -- internal tables with corresponding information.
-
- -- Put_SPARK_Xrefs reads the internal tables and generates text lines in
- -- the ALI format.
-
- ----------------------------
- -- SPARK Xrefs ALI Format --
- ----------------------------
-
- -- SPARK cross-reference information is generated on a unit-by-unit basis
- -- in the ALI file, using lines that start with the identifying character F
- -- ("Formal"). These lines are generated if GNATprove_Mode is True.
-
- -- The SPARK cross-reference information comes after the shared
- -- cross-reference information, so it can be ignored by tools like
- -- gnatbind, gnatmake, etc.
-
- -- -------------------
- -- -- Scope Section --
- -- -------------------
-
- -- A first section defines the scopes in which entities are defined and
- -- referenced. A scope is a package/subprogram/protected_type/task_type
- -- declaration/body. Note that a package declaration and body define two
- -- different scopes. Similarly, a subprogram, protected type and task type
- -- declaration and body, when both present, define two different scopes.
-
- -- FD dependency-number filename (-> unit-filename)?
-
- -- This header precedes scope information for the unit identified by
- -- dependency number and file name. The dependency number is the index
- -- into the generated D lines and is ones-origin (e.g. 2 = reference to
- -- second generated D line).
-
- -- The list of FD lines should match the list of D lines defined in the
- -- ALI file, in the same order.
-
- -- Note that the filename here will reflect the original name if a
- -- Source_Reference pragma was encountered (since all line number
- -- references will be with respect to the original file).
-
- -- Note: the filename is redundant in that it could be deduced from the
- -- corresponding D line, but it is convenient at least for human
- -- reading of the SPARK cross-reference information, and means that
- -- the SPARK cross-reference information can stand on its own without
- -- needing other parts of the ALI file.
-
- -- The optional unit filename is given only for subunits.
-
- -- FS . scope line type col entity (-> spec-file . spec-scope)?
-
- -- (The ? mark stands for an optional entry in the syntax)
-
- -- scope is the ones-origin scope number for the current file (e.g. 2 =
- -- reference to the second FS line in this FD block).
-
- -- line is the line number of the scope entity. The name of the entity
- -- starts in column col. Columns are numbered from one, and if
- -- horizontal tab characters are present, the column number is computed
- -- assuming standard 1,9,17,.. tab stops. For example, if the entity is
- -- the first token on the line, and is preceded by space-HT-space, then
- -- the column would be column 10.
-
- -- type is a single letter identifying the type of the entity, using
- -- the same code as in cross-references:
-
- -- K = package (k = generic package)
- -- V = function (v = generic function)
- -- U = procedure (u = generic procedure)
- -- Y = entry
-
- -- col is the column number of the scope entity
-
- -- entity is the name of the scope entity, with casing in the canonical
- -- casing for the source file where it is defined.
-
- -- spec-file and spec-scope are respectively the file and scope for the
- -- spec corresponding to the current body scope, when they differ.
-
- -- ------------------
- -- -- Xref Section --
- -- ------------------
-
- -- A second section defines cross-references useful for computing global
- -- variables read/written in each subprogram/package/protected_type/
- -- task_type.
-
- -- FX dependency-number filename . entity-number entity
-
- -- dependency-number and filename identify a file in FD lines
-
- -- entity-number and entity identify a scope in FS lines
- -- for the previously identified file.
-
- -- (filename and entity are just a textual representations of
- -- dependency-number and entity-number)
-
- -- F line typ col entity ref*
-
- -- line is the line number of the referenced entity
-
- -- typ is the type of the referenced entity, using a code similar to
- -- the one used for cross-references:
-
- -- > = IN parameter
- -- < = OUT parameter
- -- = = IN OUT parameter
- -- * = all other cases
-
- -- col is the column number of the referenced entity
-
- -- entity is the name of the referenced entity as written in the source
- -- file where it is defined.
-
- -- There may be zero or more ref entries on each line
-
- -- (file |)? ((. scope :)? line type col)*
-
- -- file is the dependency number of the file with the reference. It and
- -- the following vertical bar are omitted if the file is the same as
- -- the previous ref, and the refs for the current file are first (and
- -- do not need a bar).
-
- -- scope is the scope number of the scope with the reference. It and
- -- the following colon are omitted if the scope is the same as the
- -- previous ref, and the refs for the current scope are first (and do
- -- not need a colon).
-
- -- line is the line number of the reference
-
- -- col is the column number of the reference
-
- -- type is one of the following, using the same code as in
- -- cross-references:
-
- -- m = modification
- -- r = reference
- -- c = reference to constant object
- -- s = subprogram reference in a static call
-
- -- Special entries for reads and writes to memory reference a special
- -- variable called "__HEAP". These special entries are present in every
- -- scope where reads and writes to memory are present. Line and column for
- -- this special variable are always 0.
-
- -- Examples: ??? add examples here
-
-- -------------------------------
-- -- Generated Globals Section --
-- -------------------------------
-- Debug routine to dump internal SPARK cross-reference tables. This is a
-- raw format dump showing exactly what the tables contain.
- procedure pspark;
- -- Debugging procedure to output contents of SPARK cross-reference binary
- -- tables in the format in which they appear in an ALI file.
-
end SPARK_Xrefs;
+++ /dev/null
-------------------------------------------------------------------------------
--- --
--- GNAT SYSTEM UTILITIES --
--- --
--- S P A R K _ X R E F S _ T E S T --
--- --
--- B o d y --
--- --
--- Copyright (C) 2011-2013, Free Software Foundation, Inc. --
--- --
--- GNAT is free software; you can redistribute it and/or modify it under --
--- terms of the GNU General Public License as published by the Free Soft- --
--- ware Foundation; either version 3, or (at your option) any later ver- --
--- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
--- for more details. You should have received a copy of the GNU General --
--- Public License distributed with GNAT; see file COPYING3. If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license. --
--- --
--- GNAT was originally developed by the GNAT team at New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc. --
--- --
-------------------------------------------------------------------------------
-
--- This utility program is used to test proper operation of the
--- Get_SPARK_Xrefs and Put_SPARK_Xrefs units. To run it, compile any source
--- file with switch -gnatd.E or -gnatd.F to get an ALI file file.ALI
--- containing SPARK information. Then run this utility using:
-
--- spark_xrefs_test file.ali
-
--- This test will read the SPARK cross-reference information from the ALI
--- file, and use Get_SPARK_Xrefs to store this in binary form in the internal
--- tables in SPARK_Xrefs. Then Put_SPARK_Xrefs is used to write the
--- information from these tables back into text form. This output is compared
--- with the original SPARK cross-reference information in the ALI file and the
--- two should be identical. If not an error message is output.
-
-with Get_SPARK_Xrefs;
-with Put_SPARK_Xrefs;
-
-with SPARK_Xrefs; use SPARK_Xrefs;
-with Types; use Types;
-
-with Ada.Command_Line; use Ada.Command_Line;
-with Ada.Streams; use Ada.Streams;
-with Ada.Streams.Stream_IO; use Ada.Streams.Stream_IO;
-with Ada.Text_IO;
-
-with GNAT.OS_Lib; use GNAT.OS_Lib;
-
-procedure SPARK_Xrefs_Test is
- Infile : File_Type;
- Name1 : String_Access;
- Outfile_1 : File_Type;
- Name2 : String_Access;
- Outfile_2 : File_Type;
- C : Character;
-
- Stop : exception;
- -- Terminate execution
-
- Diff_Exec : constant String_Access := Locate_Exec_On_Path ("diff");
- Diff_Result : Integer;
-
- use ASCII;
-
-begin
- if Argument_Count /= 1 then
- Ada.Text_IO.Put_Line ("Usage: spark_xrefs_test FILE.ali");
- raise Stop;
- end if;
-
- Name1 := new String'(Argument (1) & ".1");
- Name2 := new String'(Argument (1) & ".2");
-
- Open (Infile, In_File, Argument (1));
- Create (Outfile_1, Out_File, Name1.all);
- Create (Outfile_2, Out_File, Name2.all);
-
- -- Read input file till we get to first 'F' line
-
- Process : declare
- Output_Col : Positive := 1;
-
- function Get_Char (F : File_Type) return Character;
- -- Read one character from specified file
-
- procedure Put_Char (F : File_Type; C : Character);
- -- Write one character to specified file
-
- function Get_Output_Col return Positive;
- -- Return current column in output file, where each line starts at
- -- column 1 and terminate with LF, and HT is at columns 1, 9, etc.
- -- All output is supposed to be carried through Put_Char.
-
- --------------
- -- Get_Char --
- --------------
-
- function Get_Char (F : File_Type) return Character is
- Item : Stream_Element_Array (1 .. 1);
- Last : Stream_Element_Offset;
-
- begin
- Read (F, Item, Last);
-
- if Last /= 1 then
- return Types.EOF;
- else
- return Character'Val (Item (1));
- end if;
- end Get_Char;
-
- --------------------
- -- Get_Output_Col --
- --------------------
-
- function Get_Output_Col return Positive is
- begin
- return Output_Col;
- end Get_Output_Col;
-
- --------------
- -- Put_Char --
- --------------
-
- procedure Put_Char (F : File_Type; C : Character) is
- Item : Stream_Element_Array (1 .. 1);
-
- begin
- if C /= CR and then C /= EOF then
- if C = LF then
- Output_Col := 1;
- elsif C = HT then
- Output_Col := ((Output_Col + 6) / 8) * 8 + 1;
- else
- Output_Col := Output_Col + 1;
- end if;
-
- Item (1) := Character'Pos (C);
- Write (F, Item);
- end if;
- end Put_Char;
-
- -- Subprograms used by Get_SPARK_Xrefs (these also copy the output to
- -- Outfile_1 for later comparison with the output generated by
- -- Put_SPARK_Xrefs).
-
- function Getc return Character;
- function Nextc return Character;
- procedure Skipc;
-
- ----------
- -- Getc --
- ----------
-
- function Getc return Character is
- C : Character;
- begin
- C := Get_Char (Infile);
- Put_Char (Outfile_1, C);
- return C;
- end Getc;
-
- -----------
- -- Nextc --
- -----------
-
- function Nextc return Character is
- C : Character;
-
- begin
- C := Get_Char (Infile);
-
- if C /= EOF then
- Set_Index (Infile, Index (Infile) - 1);
- end if;
-
- return C;
- end Nextc;
-
- -----------
- -- Skipc --
- -----------
-
- procedure Skipc is
- C : Character;
- pragma Unreferenced (C);
- begin
- C := Getc;
- end Skipc;
-
- -- Subprograms used by Put_SPARK_Xrefs, which write information to
- -- Outfile_2.
-
- function Write_Info_Col return Positive;
- procedure Write_Info_Char (C : Character);
- procedure Write_Info_Initiate (Key : Character);
- procedure Write_Info_Nat (N : Nat);
- procedure Write_Info_Terminate;
-
- --------------------
- -- Write_Info_Col --
- --------------------
-
- function Write_Info_Col return Positive is
- begin
- return Get_Output_Col;
- end Write_Info_Col;
-
- ---------------------
- -- Write_Info_Char --
- ---------------------
-
- procedure Write_Info_Char (C : Character) is
- begin
- Put_Char (Outfile_2, C);
- end Write_Info_Char;
-
- -------------------------
- -- Write_Info_Initiate --
- -------------------------
-
- procedure Write_Info_Initiate (Key : Character) is
- begin
- Write_Info_Char (Key);
- end Write_Info_Initiate;
-
- --------------------
- -- Write_Info_Nat --
- --------------------
-
- procedure Write_Info_Nat (N : Nat) is
- begin
- if N > 9 then
- Write_Info_Nat (N / 10);
- end if;
-
- Write_Info_Char (Character'Val (48 + N mod 10));
- end Write_Info_Nat;
-
- --------------------------
- -- Write_Info_Terminate --
- --------------------------
-
- procedure Write_Info_Terminate is
- begin
- Write_Info_Char (LF);
- end Write_Info_Terminate;
-
- -- Local instantiations of Put_SPARK_Xrefs and Get_SPARK_Xrefs
-
- procedure Get_SPARK_Xrefs_Info is new Get_SPARK_Xrefs;
- procedure Put_SPARK_Xrefs_Info is new Put_SPARK_Xrefs;
-
- -- Start of processing for Process
-
- begin
- -- Loop to skip till first 'F' line
-
- loop
- C := Get_Char (Infile);
-
- if C = EOF then
- raise Stop;
-
- elsif C = LF or else C = CR then
- loop
- C := Get_Char (Infile);
- exit when C /= LF and then C /= CR;
- end loop;
-
- exit when C = 'F';
- end if;
- end loop;
-
- -- Position back to initial 'F' of first 'F' line
-
- Set_Index (Infile, Index (Infile) - 1);
-
- -- Read SPARK cross-reference information to internal SPARK tables, also
- -- copying SPARK xrefs info to Outfile_1.
-
- Initialize_SPARK_Tables;
- Get_SPARK_Xrefs_Info;
-
- -- Write SPARK cross-reference information from internal SPARK tables to
- -- Outfile_2.
-
- Put_SPARK_Xrefs_Info;
-
- -- Junk blank line (see comment at end of Lib.Writ)
-
- Write_Info_Terminate;
-
- -- Flush to disk
-
- Close (Outfile_1);
- Close (Outfile_2);
-
- -- Now Outfile_1 and Outfile_2 should be identical
-
- Diff_Result :=
- Spawn (Diff_Exec.all,
- Argument_String_To_List
- ("-u " & Name1.all & " " & Name2.all).all);
-
- if Diff_Result /= 0 then
- Ada.Text_IO.Put_Line ("diff(1) exit status" & Diff_Result'Img);
- end if;
-
- OS_Exit (Diff_Result);
-
- end Process;
-
-exception
- when Stop =>
- null;
-end SPARK_Xrefs_Test;
+2017-11-08 Javier Miranda <miranda@adacore.com>
+
+ * gnat.dg/overriding_ops2.adb, gnat.dg/overriding_ops2.ads,
+ gnat.dg/overriding_ops2_pkg.ads, gnat.dg/overriding_ops2_pkg-high.ads:
+ New testcase.
+
2017-11-08 Andreas Schwab <schwab@suse.de>
* c-c++-common/torture/aarch64-vect-lane-2.c (search_line_fast):
--- /dev/null
+-- { dg-do compile }
+
+package body Overriding_Ops2 is
+ overriding procedure Finalize (Self : in out Consumer) is
+ begin
+ null;
+ end Finalize;
+end Overriding_Ops2;
--- /dev/null
+with Overriding_Ops2_Pkg.High;
+
+package Overriding_Ops2 is
+ type Consumer is tagged limited private;
+private
+ type Consumer is
+ limited
+ new Overriding_Ops2_Pkg.High.High_Level_Session
+ with null record;
+
+ overriding procedure Finalize (Self : in out Consumer);
+end Overriding_Ops2;
--- /dev/null
+package Overriding_Ops2_Pkg.High is
+ type High_Level_Session is new Session_Type with private;
+private
+ type High_Level_Session is new Session_Type with null record;
+end Overriding_Ops2_Pkg.High;
--- /dev/null
+with Ada.Finalization;
+
+package Overriding_Ops2_Pkg is
+ type Session_Type is abstract tagged limited private;
+ procedure Finalize (Session : in out Session_Type);
+private
+ type Session_Type is
+ abstract new Ada.Finalization.Limited_Controlled with null record;
+end Overriding_Ops2_Pkg;
projects / gcc.git / commitdiff