[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.

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.

From-SVN: r263092

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 33ff75bf2a6ca67b09111cf4768875b4f283a6cf..ed00e5450cf1664e4dd68f79c904a7dbe0610672 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2018-07-31  Piotr Trojanek  <trojanek@adacore.com>
+
+       * ali.adb (Known_ALI_Lines): Remove 'F' as a prefix for lines
+       related to the FORMAL analysis done by GNATprove.
+
 2018-07-31  Javier Miranda  <miranda@adacore.com>
 
        * sem.ads (Inside_Preanalysis_Without_Freezing): New global

diff --git a/gcc/ada/ali.adb b/gcc/ada/ali.adb
index 1cb454cce1ef1831953f9beffe5bf0c2d88642aa..48b5715c7865728d116936615fb16f1c90e7db99 100644 (file)
--- a/gcc/ada/ali.adb
+++ b/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);