From e8723e74410de463cdba50e31489f7803387c9bd Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Tue, 31 Jul 2018 09:55:32 +0000 Subject: [PATCH] [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 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 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/ali.adb | 3 +-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 33ff75bf2a6..ed00e5450cf 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2018-07-31 Piotr Trojanek + + * 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 * sem.ads (Inside_Preanalysis_Without_Freezing): New global diff --git a/gcc/ada/ali.adb b/gcc/ada/ali.adb index 1cb454cce1e..48b5715c786 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); -- 2.30.2