From 704228bdcc8e23d3ffd65748acbb6ee9ecba0083 Mon Sep 17 00:00:00 2001
From: Yannick Moy <moy@adacore.com>
Date: Tue, 20 Oct 2015 12:42:53 +0000
Subject: [PATCH] fmap.adb, [...]: Fix coding style for marking start of
processing of subprograms.
2015-10-20 Yannick Moy <moy@adacore.com>
* fmap.adb, a-cihama.adb, sem_ch5.adb, make.adb, inline.adb,
a-cfhase.adb, scng.adb, sem_ch12.adb, freeze.adb, tempdir.adb,
sem_util.adb, sem_res.adb, s-regexp.adb, a-clrefi.adb: Fix coding
style for marking start of processing of subprograms.
2015-10-20 Yannick Moy <moy@adacore.com>
* lib-xref-spark_specific.adb (Add_SPARK_File): Start traversal
by requesting info from stubs. (Traverse_All_Compilation_Units):
Remove unused procedure.
(Traverse_Declarations_Or_Statements): Handle protected and task units.
* lib-xref.ads (Traverse_All_Compilation_Units): Remove unused
procedure.
* restrict.adb (Check_Restriction): Do not ignore
restrictions in GNATprove_Mode.
From-SVN: r229078
---
gcc/ada/ChangeLog | 18 ++++++++
gcc/ada/a-cfhase.adb | 2 +-
gcc/ada/a-cihama.adb | 2 +-
gcc/ada/a-clrefi.adb | 6 +--
gcc/ada/fmap.adb | 4 +-
gcc/ada/freeze.adb | 2 +-
gcc/ada/inline.adb | 2 +-
gcc/ada/lib-xref-spark_specific.adb | 70 +++++++++++++++++++++++------
gcc/ada/lib-xref.ads | 4 --
gcc/ada/make.adb | 2 +-
gcc/ada/restrict.adb | 2 +-
gcc/ada/s-regexp.adb | 4 +-
gcc/ada/scng.adb | 2 +-
gcc/ada/sem_ch12.adb | 2 +-
gcc/ada/sem_ch5.adb | 4 +-
gcc/ada/sem_res.adb | 2 +-
gcc/ada/sem_util.adb | 4 +-
gcc/ada/tempdir.adb | 4 +-
18 files changed, 96 insertions(+), 40 deletions(-)
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 3e0d760a6597..3407bd3b4a99 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,21 @@
+2015-10-20 Yannick Moy <moy@adacore.com>
+
+ * fmap.adb, a-cihama.adb, sem_ch5.adb, make.adb, inline.adb,
+ a-cfhase.adb, scng.adb, sem_ch12.adb, freeze.adb, tempdir.adb,
+ sem_util.adb, sem_res.adb, s-regexp.adb, a-clrefi.adb: Fix coding
+ style for marking start of processing of subprograms.
+
+2015-10-20 Yannick Moy <moy@adacore.com>
+
+ * lib-xref-spark_specific.adb (Add_SPARK_File): Start traversal
+ by requesting info from stubs. (Traverse_All_Compilation_Units):
+ Remove unused procedure.
+ (Traverse_Declarations_Or_Statements): Handle protected and task units.
+ * lib-xref.ads (Traverse_All_Compilation_Units): Remove unused
+ procedure.
+ * restrict.adb (Check_Restriction): Do not ignore
+ restrictions in GNATprove_Mode.
+
2015-10-20 Arnaud Charlet <charlet@adacore.com>
* s-valllu.adb, sem_ch3.adb, layout.adb, a-crbtgo.adb, exp_ch9.adb,
diff --git a/gcc/ada/a-cfhase.adb b/gcc/ada/a-cfhase.adb
index ac2ea61adb42..d25705bfc71f 100644
--- a/gcc/ada/a-cfhase.adb
+++ b/gcc/ada/a-cfhase.adb
@@ -516,7 +516,7 @@ is
end loop;
end Find_Equivalent_Key;
- -- Start of processing of Equivalent_Sets
+ -- Start of processing for Equivalent_Sets
begin
return Is_Equivalent (Left, Right);
diff --git a/gcc/ada/a-cihama.adb b/gcc/ada/a-cihama.adb
index 2cea31895111..11831004deac 100644
--- a/gcc/ada/a-cihama.adb
+++ b/gcc/ada/a-cihama.adb
@@ -788,7 +788,7 @@ package body Ada.Containers.Indefinite_Hashed_Maps is
Busy : With_Busy (Container.HT.TC'Unrestricted_Access);
- -- Start of processing Iterate
+ -- Start of processing for Iterate
begin
Local_Iterate (Container.HT);
diff --git a/gcc/ada/a-clrefi.adb b/gcc/ada/a-clrefi.adb
index 4708bf8f34c5..5afde3b616cb 100644
--- a/gcc/ada/a-clrefi.adb
+++ b/gcc/ada/a-clrefi.adb
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 2007-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 2007-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -217,7 +217,7 @@ package body Ada.Command_Line.Response_File is
end loop;
end Get_Line;
- -- Start or Recurse
+ -- Start of processing for Recurse
begin
Last_Arg := 0;
@@ -491,7 +491,7 @@ package body Ada.Command_Line.Response_File is
raise;
end Recurse;
- -- Start of Arguments_From
+ -- Start of processing for Arguments_From
begin
-- The job is done by procedure Recurse
diff --git a/gcc/ada/fmap.adb b/gcc/ada/fmap.adb
index f5432096e28f..77fa6c0d78d1 100644
--- a/gcc/ada/fmap.adb
+++ b/gcc/ada/fmap.adb
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 2001-2012, Free Software Foundation, Inc. --
+-- Copyright (C) 2001-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -478,7 +478,7 @@ package body Fmap is
Buffer (Buffer_Last) := ASCII.LF;
end Put_Line;
- -- Start of Update_Mapping_File
+ -- Start of processing for Update_Mapping_File
begin
-- If the mapping file could not be read, then it will not be possible
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 36822ec05b6b..ee8a23e5f1c9 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -1592,7 +1592,7 @@ package body Freeze is
end if;
end Process_Flist;
- -- Start or processing for Freeze_All_Ent
+ -- Start of processing for Freeze_All_Ent
begin
E := From;
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index bb26c4639d84..0d16affb06e0 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -1504,7 +1504,7 @@ package body Inline is
Id : Entity_Id; -- Procedure or function entity for the subprogram
- -- Start of Can_Be_Inlined_In_GNATprove_Mode
+ -- Start of processing for Can_Be_Inlined_In_GNATprove_Mode
begin
pragma Assert (Present (Spec_Id) or else Present (Body_Id));
diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb
index b38d65b23dd4..a39671494fa2 100644
--- a/gcc/ada/lib-xref-spark_specific.adb
+++ b/gcc/ada/lib-xref-spark_specific.adb
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 2011-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 2011-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -154,7 +154,7 @@ package body SPARK_Specific is
Traverse_Compilation_Unit
(CU => Cunit (Ubody),
Process => Detect_And_Add_SPARK_Scope'Access,
- Inside_Stubs => False);
+ Inside_Stubs => True);
end if;
-- When two units are present for the same compilation unit, as it
@@ -166,7 +166,7 @@ package body SPARK_Specific is
Traverse_Compilation_Unit
(CU => Cunit (Uspec),
Process => Detect_And_Add_SPARK_Scope'Access,
- Inside_Stubs => False);
+ Inside_Stubs => True);
end if;
end if;
@@ -1151,17 +1151,6 @@ package body SPARK_Specific is
end if;
end Generate_Dereference;
- ------------------------------------
- -- Traverse_All_Compilation_Units --
- ------------------------------------
-
- procedure Traverse_All_Compilation_Units (Process : Node_Processing) is
- begin
- for U in Units.First .. Last_Unit loop
- Traverse_Compilation_Unit (Cunit (U), Process, Inside_Stubs => False);
- end loop;
- end Traverse_All_Compilation_Units;
-
-------------------------------
-- Traverse_Compilation_Unit --
-------------------------------
@@ -1300,6 +1289,59 @@ package body SPARK_Specific is
end;
end if;
+ -- Protected unit
+
+ when N_Protected_Definition =>
+ Traverse_Declarations_Or_Statements
+ (Visible_Declarations (N), Process, Inside_Stubs);
+ Traverse_Declarations_Or_Statements
+ (Private_Declarations (N), Process, Inside_Stubs);
+
+ when N_Protected_Body =>
+ Traverse_Declarations_Or_Statements
+ (Declarations (N), Process, Inside_Stubs);
+
+ when N_Protected_Body_Stub =>
+ if Present (Library_Unit (N)) then
+ declare
+ Body_N : constant Node_Id := Get_Body_From_Stub (N);
+ begin
+ if Inside_Stubs then
+ Traverse_Declarations_Or_Statements
+ (Declarations (Body_N), Process, Inside_Stubs);
+ end if;
+ end;
+ end if;
+
+ -- Task unit
+
+ when N_Task_Definition =>
+ Traverse_Declarations_Or_Statements
+ (Visible_Declarations (N), Process, Inside_Stubs);
+ Traverse_Declarations_Or_Statements
+ (Private_Declarations (N), Process, Inside_Stubs);
+
+ when N_Task_Body =>
+ Traverse_Declarations_Or_Statements
+ (Declarations (N), Process, Inside_Stubs);
+ Traverse_Handled_Statement_Sequence
+ (Handled_Statement_Sequence (N), Process, Inside_Stubs);
+
+ when N_Task_Body_Stub =>
+ if Present (Library_Unit (N)) then
+ declare
+ Body_N : constant Node_Id := Get_Body_From_Stub (N);
+ begin
+ if Inside_Stubs then
+ Traverse_Declarations_Or_Statements
+ (Declarations (Body_N), Process, Inside_Stubs);
+ Traverse_Handled_Statement_Sequence
+ (Handled_Statement_Sequence (Body_N), Process,
+ Inside_Stubs);
+ end if;
+ end;
+ end if;
+
-- Block statement
when N_Block_Statement =>
diff --git a/gcc/ada/lib-xref.ads b/gcc/ada/lib-xref.ads
index c463fe937370..9d1037ca0532 100644
--- a/gcc/ada/lib-xref.ads
+++ b/gcc/ada/lib-xref.ads
@@ -645,10 +645,6 @@ package Lib.Xref is
-- Inside_Stubs is True, then the body of stubs is also traversed.
-- Generic declarations are ignored.
- procedure Traverse_All_Compilation_Units (Process : Node_Processing);
- -- Call Process on all declarations through all compilation units.
- -- Generic declarations are ignored.
-
procedure Collect_SPARK_Xrefs
(Sdep_Table : Unit_Ref_Table;
Num_Sdep : Nat);
diff --git a/gcc/ada/make.adb b/gcc/ada/make.adb
index f3ac043a7ac7..90eb0ed1c9c9 100644
--- a/gcc/ada/make.adb
+++ b/gcc/ada/make.adb
@@ -4119,7 +4119,7 @@ package body Make is
procedure Globalize_Dirs is new
Prj.Env.For_All_Object_Dirs (Globalize_Dir);
- -- Start of procedure Globalize
+ -- Start of processing for Globalize
begin
Success := True;
diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb
index 1dbd3d551add..fb0e9682a41e 100644
--- a/gcc/ada/restrict.adb
+++ b/gcc/ada/restrict.adb
@@ -505,7 +505,7 @@ package body Restrict is
-- Just checking, SPARK does not allow restrictions to be set ???
- if CodePeer_Mode or GNATprove_Mode then
+ if CodePeer_Mode then
return;
end if;
diff --git a/gcc/ada/s-regexp.adb b/gcc/ada/s-regexp.adb
index 68cef650aacc..6a445340b14c 100644
--- a/gcc/ada/s-regexp.adb
+++ b/gcc/ada/s-regexp.adb
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 1999-2013, AdaCore --
+-- Copyright (C) 1999-2015, AdaCore --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -1084,7 +1084,7 @@ package body System.Regexp is
return J;
end Next_Sub_Expression;
- -- Start of Create_Primary_Table
+ -- Start of processing for Create_Primary_Table
begin
Table.all := (others => (others => 0));
diff --git a/gcc/ada/scng.adb b/gcc/ada/scng.adb
index 7bf8ea2eacc2..0216ddf71a99 100644
--- a/gcc/ada/scng.adb
+++ b/gcc/ada/scng.adb
@@ -641,7 +641,7 @@ package body Scng is
end loop;
end Scan_Integer;
- -- Start of Processing for Nlit
+ -- Start of processing for Nlit
begin
Base := 10;
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 41e90071a4d5..53f1cad61103 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -8126,7 +8126,7 @@ package body Sem_Ch12 is
return Freeze_Node (Id);
end Package_Freeze_Node;
- -- Start of processing of Freeze_Subprogram_Body
+ -- Start of processing for Freeze_Subprogram_Body
begin
-- If the instance and the generic body appear within the same unit, and
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 13d447e33935..24e641ebfea1 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -1571,7 +1571,7 @@ package body Sem_Ch5 is
end if;
end Analyze_Cond_Then;
- -- Start of Analyze_If_Statement
+ -- Start of processing for Analyze_If_Statement
begin
-- Initialize exit count for else statements. If there is no else part,
@@ -1788,7 +1788,7 @@ package body Sem_Ch5 is
return Etype (Ent);
end Get_Cursor_Type;
- -- Start of processing for Analyze_iterator_Specification
+ -- Start of processing for Analyze_iterator_Specification
begin
Enter_Name (Def_Id);
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index a96f1d1657a5..4de4549f2b2b 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7319,7 +7319,7 @@ package body Sem_Res is
end if;
end Actual_Index_Type;
- -- Start of processing of Resolve_Entry
+ -- Start of processing for Resolve_Entry
begin
-- Find name of entry being called, and resolve prefix of name with its
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 152be0282b52..384221e32dba 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -3021,7 +3021,7 @@ package body Sem_Util is
end if;
end Is_Later_Declarative_Item;
- -- Start of Check_Later_Vs_Basic_Declarations
+ -- Start of processing for Check_Later_Vs_Basic_Declarations
begin
Decl := First (Decls);
@@ -14385,7 +14385,7 @@ package body Sem_Util is
procedure Mark_Allocators is new Traverse_Proc (Mark_Allocator);
- -- Start of processing Mark_Coextensions
+ -- Start of processing for Mark_Coextensions
begin
-- An allocator that appears on the right-hand side of an assignment is
diff --git a/gcc/ada/tempdir.adb b/gcc/ada/tempdir.adb
index 4936c26c5aae..d78386303857 100644
--- a/gcc/ada/tempdir.adb
+++ b/gcc/ada/tempdir.adb
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 2003-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 2003-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -62,7 +62,7 @@ package body Tempdir is
end if;
end Directory;
- -- Start of processing Tempdir
+ -- Start of processing for Create_Temp_File
begin
if Temp_Dir'Length /= 0 then
--
GitLab