git
/
gcc
mirror of git://gcc.gnu.org/git/gcc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

[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
This commit is contained in:
Piotr Trojanek 2018-07-31 09:55:32 +00:00 committed by Pierre-Marie de Rodat
parent b09a237ab8
commit e8723e7441
2 changed files with 6 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
gcc/ada/ChangeLog
View File

@ -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> 2018-07-31 Javier Miranda <miranda@adacore.com>
* sem.ads (Inside_Preanalysis_Without_Freezing): New global * sem.ads (Inside_Preanalysis_Without_Freezing): New global

3
gcc/ada/ali.adb
View File

@ -39,7 +39,7 @@ package body ALI is
-- line type markers in the ALI file. This is used in Scan_ALI to detect -- 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: -- (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 := Known_ALI_Lines : constant array (Character range 'A' .. 'Z') of Boolean :=
('V' => True, -- version ('V' => True, -- version
@ -59,7 +59,6 @@ package body ALI is
'Y' => True, -- limited_with 'Y' => True, -- limited_with
'Z' => True, -- implicit with from instantiation 'Z' => True, -- implicit with from instantiation
'C' => True, -- SCO information 'C' => True, -- SCO information
'F' => True, -- SPARK cross-reference information
'T' => True, -- task stack information 'T' => True, -- task stack information
others => False); others => False);