In formal verification mode, in order to properly detect which parameters may
be read/written by a subprogram, a new information is added to ALFA cross
references.
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-08-04 Yannick Moy <m...@adacore.com>
* alfa.ads (ALFA_Xref_Record): add component for type of entity
* get_alfa.adb, put_alfa.adb: Read and write new component of
cross-reference.
* lib-xref-alfa.adb (Collect_ALFA): generate new component.
Index: alfa.ads
===================================================================
--- alfa.ads (revision 177361)
+++ alfa.ads (working copy)
@@ -133,10 +133,18 @@
-- entity-number and identity identify a scope entity in FS lines for
-- the file previously identified.
- -- line col entity ref*
+ -- 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
@@ -186,6 +194,13 @@
Entity_Line : Nat;
-- Line number for the entity referenced
+ Etype : Character;
+ -- Indicates type of entity, using code used in ALI file:
+ -- > = IN parameter
+ -- < = OUT parameter
+ -- = = IN OUT parameter
+ -- * = all other cases
+
Entity_Col : Nat;
-- Column number for the entity referenced
Index: put_alfa.adb
===================================================================
--- put_alfa.adb (revision 177274)
+++ put_alfa.adb (working copy)
@@ -173,7 +173,7 @@
Write_Info_Initiate ('F');
Write_Info_Char (' ');
Write_Info_Nat (R.Entity_Line);
- Write_Info_Char (' ');
+ Write_Info_Char (R.Etype);
Write_Info_Nat (R.Entity_Col);
Write_Info_Char (' ');
Index: lib-xref-alfa.adb
===================================================================
--- lib-xref-alfa.adb (revision 177324)
+++ lib-xref-alfa.adb (working copy)
@@ -635,6 +635,9 @@
-- Return scope entity which corresponds to index Cur_Scope_Idx in
-- table ALFA_Scope_Table.
+ function Get_Entity_Type (E : Entity_Id) return Character;
+ -- Return a character representing the type of entity
+
function Is_Future_Scope_Entity (E : Entity_Id) return Boolean;
-- Check whether entity E is in ALFA_Scope_Table at index
-- Cur_Scope_Idx or higher.
@@ -652,6 +655,22 @@
return ALFA_Scope_Table.Table (Cur_Scope_Idx).Scope_Entity;
end Cur_Scope;
+ ---------------------
+ -- Get_Entity_Type --
+ ---------------------
+
+ function Get_Entity_Type (E : Entity_Id) return Character is
+ C : Character;
+ begin
+ case Ekind (E) is
+ when E_Out_Parameter => C := '<';
+ when E_In_Out_Parameter => C := '=';
+ when E_In_Parameter => C := '>';
+ when others => C := '*';
+ end case;
+ return C;
+ end Get_Entity_Type;
+
----------------------------
-- Is_Future_Scope_Entity --
----------------------------
@@ -729,6 +748,7 @@
ALFA_Xref_Table.Append (
(Entity_Name => Cur_Entity_Name,
Entity_Line => Int (Get_Logical_Line_Number (XE.Def)),
+ Etype => Get_Entity_Type (XE.Ent),
Entity_Col => Int (Get_Column_Number (XE.Def)),
File_Num => Dependency_Num (XE.Lun),
Scope_Num => Get_Scope_Num (XE.Ref_Scope),
Index: get_alfa.adb
===================================================================
--- get_alfa.adb (revision 177274)
+++ get_alfa.adb (working copy)
@@ -371,6 +371,7 @@
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|)
@@ -383,7 +384,7 @@
XR_Scope := Cur_Scope;
XR_Entity_Line := Get_Nat;
- Check (' ');
+ XR_Entity_Typ := Getc;
XR_Entity_Col := Get_Nat;
Skip_Spaces;
@@ -439,6 +440,7 @@
ALFA_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,
