diff options
Diffstat (limited to 'gcc/ada/lib-xref.adb')
| -rw-r--r-- | gcc/ada/lib-xref.adb | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb index ba9221b..8825f06 100644 --- a/gcc/ada/lib-xref.adb +++ b/gcc/ada/lib-xref.adb @@ -79,7 +79,7 @@ package body Lib.Xref is -- Unit number corresponding to Loc. Value is undefined and not -- referenced if Loc is set to No_Location. - -- The following components are only used for Alfa cross-references + -- The following components are only used for SPARK cross-references Ref_Scope : Entity_Id; -- Entity of the closest subprogram or package enclosing the reference @@ -151,11 +151,11 @@ package body Lib.Xref is Hash => Hash, Equal => Equal); - ---------------------- - -- Alfa Information -- - ---------------------- + ----------------------------- + -- SPARK Xrefs Information -- + ----------------------------- - package body Alfa is separate; + package body SPARK_Specific is separate; ------------------------ -- Local Subprograms -- @@ -632,10 +632,10 @@ package body Lib.Xref is or else (Typ = 'b' and then Is_Generic_Instance (E)) -- Allow the generation of references to reads, writes and calls - -- in Alfa mode when the related context comes from an instance. + -- in SPARK mode when the related context comes from an instance. or else - (Alfa_Mode + (SPARK_Mode and then In_Extended_Main_Code_Unit (N) and then (Typ = 'm' or else Typ = 'r' or else Typ = 's')) then @@ -885,12 +885,12 @@ package body Lib.Xref is -- Ignore references from within an instance. The only exceptions to -- this are default subprograms, for which we generate an implicit - -- reference and compilations in Alfa_Mode. + -- reference and compilations in SPARK mode. and then (Instantiation_Location (Sloc (N)) = No_Location or else Typ = 'i' - or else Alfa_Mode) + or else SPARK_Mode) -- Ignore dummy references @@ -973,11 +973,11 @@ package body Lib.Xref is return; end if; - -- In Alfa mode, consider the underlying entity renamed instead of + -- In SPARK mode, consider the underlying entity renamed instead of -- the renaming, which is needed to compute a valid set of effects -- (reads, writes) for the enclosing subprogram. - if Alfa_Mode then + if SPARK_Mode then Ent := Get_Through_Renamings (Ent); -- If no enclosing object, then it could be a reference to any @@ -987,10 +987,10 @@ package body Lib.Xref is if No (Ent) then if Actual_Typ = 'w' then - Alfa.Generate_Dereference (Nod, 'r'); - Alfa.Generate_Dereference (Nod, 'w'); + SPARK_Specific.Generate_Dereference (Nod, 'r'); + SPARK_Specific.Generate_Dereference (Nod, 'w'); else - Alfa.Generate_Dereference (Nod, 'r'); + SPARK_Specific.Generate_Dereference (Nod, 'r'); end if; return; @@ -1006,14 +1006,14 @@ package body Lib.Xref is Actual_Typ := 'P'; end if; - if Alfa_Mode then + if SPARK_Mode then Ref := Sloc (Nod); Def := Sloc (Ent); - Ref_Scope := Alfa.Enclosing_Subprogram_Or_Package (Nod); - Ent_Scope := Alfa.Enclosing_Subprogram_Or_Package (Ent); + Ref_Scope := SPARK_Specific.Enclosing_Subprogram_Or_Package (Nod); + Ent_Scope := SPARK_Specific.Enclosing_Subprogram_Or_Package (Ent); - -- Since we are reaching through renamings in Alfa mode, we may + -- Since we are reaching through renamings in SPARK mode, we may -- end up with standard constants. Ignore those. if Sloc (Ent_Scope) <= Standard_Location |