diff mbox

[Ada] Enrich ALFA cross references with the type of entity for parameters

Message ID 20110804131613.GA29760@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Aug. 4, 2011, 1:16 p.m. UTC
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  <moy@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.
diff mbox

Patch

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,