aboutsummaryrefslogtreecommitdiff
path: root/gcc
diff options
context:
space:
mode:
authorPiotr Trojanek <trojanek@adacore.com>2018-07-31 09:55:32 +0000
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>2018-07-31 09:55:32 +0000
commite8723e74410de463cdba50e31489f7803387c9bd (patch)
tree8c7c573bcaa93398857918ab93df3abc24d36d80 /gcc
parentb09a237ab879a169416c3be1af8a773e982fd53a (diff)
downloadgcc-e8723e74410de463cdba50e31489f7803387c9bd.zip
gcc-e8723e74410de463cdba50e31489f7803387c9bd.tar.gz
gcc-e8723e74410de463cdba50e31489f7803387c9bd.tar.bz2
[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
Diffstat (limited to 'gcc')
-rw-r--r--gcc/ada/ChangeLog5
-rw-r--r--gcc/ada/ali.adb3
2 files changed, 6 insertions, 2 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 33ff75b..ed00e54 100644
--- 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 1cb454c..48b5715 100644
--- 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);