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]

[Ada] Deconstruct 'F' as a prefix for an ALI data


In GNATprove we used to store a variant of cross-reference information in
the ALI file in lines that started with an 'F' letter. This is no longer
the case, so the letter can be returned to the pool of unused prefixes.

Tested on x86_64-pc-linux-gnu, committed on trunk

2018-07-31  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* ali.adb (Known_ALI_Lines): Remove 'F' as a prefix for lines
	related to the FORMAL analysis done by GNATprove.
--- gcc/ada/ali.adb
+++ gcc/ada/ali.adb
@@ -39,7 +39,7 @@ package body ALI is
    --  line type markers in the ALI file. This is used in Scan_ALI to detect
    --  (or skip) invalid lines. The following letters are still available:
    --
-   --    B G H J K O Q Z
+   --    B F G H J K O Q Z
 
    Known_ALI_Lines : constant array (Character range 'A' .. 'Z') of Boolean :=
      ('V'    => True,   -- version
@@ -59,7 +59,6 @@ package body ALI is
       'Y'    => True,   -- limited_with
       'Z'    => True,   -- implicit with from instantiation
       'C'    => True,   -- SCO information
-      'F'    => True,   -- SPARK cross-reference information
       'T'    => True,   -- task stack information
       others => False);
 


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]