This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |
Other format: | [Raw text] |
Follow-up for the extraction of relevant cross-references for formal verification. Instead of printing cross-references subprogram by subprogram, which was not very readable for debugging, now print cross-references using a format close to the usual cross-references format. Also, do not print references on-the-fly but store the relevant information in dedicated tables, and define Put and Get packages to communicate between internal tables and ALI format. Most of this is directly inspired from work on SCO. Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-03 Yannick Moy <moy@adacore.com> * alfa.adb, alfa.ads, alfa_test.adb: New files. * ali.adb (Known_ALI_Lines): add 'C' lines (SCO) and 'F' lines (ALFA) (Scan_ALI): do not issue a fatal error if parsing known lines after Xref section (does not happen in compiler, only if code directly calls Scan_ALI). * get_alfa.adb, get_alfa.ads: New files. * lib-writ.adb, lib-writ.ads (Write_ALI): output ALFA information if needed. * lib-xref-alfa.adb: New file. * lib-xref.adb, lib-xref.ads (Xref_Entry): redefine information needed in cross-references for ALFA. Push ALFA treatments in separated local package. (Enclosing_Subpragram_Or_Package): treat specially subprogram identifiers. Return entity of package body instead of spec. Return Empty for a scope with no location. (Generate_Reference): adapt to new components for ALFA information. Remove the need for D references on definitions. (Is_Local_Reference): moved to ALFA local package (Output_References): extract subfunction as Extract_Source_Name (Output_Local_References): remove procedure, replaced by filtering of cross-references in package ALFA and printing in Put_ALFA. (Write_Entity_Name): remove procedure * lib.adb, lib.ads (Extract_Source_Name): extract here function to print exact name of entity as it appears in source file (Unit_Ref_Table): make type public for use in Lib.Xref.ALFA * put_alfa.adb, put_alfa.ads: New files. * xref_lib.adb (Search_Xref): protect read of cross-references against reading other sections of the ALI file, in gnatxref (Search): protect read of cross-references against reading other sections of the ALI file, in gnatfind. * gcc-interface/Make-lang.in: Update dependencies.
Attachment:
difs
Description: Text document
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |