diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 3e0d760a65978d700b0cf5fe67220aee791d7090..3407bd3b4a99b5db72f587a1a9dd7e92877d6155 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 ac2ea61adb42c23a9239d7c71c31703749dea956..d25705bfc71f31bb81198911ab08b5a883d9cfca 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 2cea31895111955a6a6841c40e5e4adc93d7a242..11831004deac8c5cfa2f91e1de23f7c18514ed23 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 4708bf8f34c53f0cb9e7384ded39b9d9b5ebd05d..5afde3b616cb3942c080179f2a4751f30b3af46c 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 f5432096e28f92508f95071facd21d924259226a..77fa6c0d78d160a629993f52c819a52388c7c173 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 36822ec05b6b7a19b8c7d2834b9132c6eaa61647..ee8a23e5f1c948ee37f8f2d56a4d479376dad413 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 bb26c4639d84d46f5f5afee078b53cfb2b241a1e..0d16affb06e0c7948d56c7573a4013008dc3229c 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 b38d65b23dd4894a75161c16c276413bde236940..a39671494fa2c87f40e7c12726eeac5f01a74c31 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 c463fe937370144c29da782a29f13b804e33ea09..9d1037ca05326bd49a6147d0ab901caab9e945d4 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 f3ac043a7ac76145a7dbf14d8b0cc18ec3d1c81c..90eb0ed1c9c9cfb84a8b3bc00197143043973bdf 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 1dbd3d551add9fe2b90c46ef361a76362d4accc2..fb0e9682a41e16e4f8335cd0b335a07906adb97a 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 68cef650aacc2b12c21b7628e1444506e728d962..6a445340b14c1ef1ec9ee5e8c23586b83bfa4c44 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 7bf8ea2eacc25885d61586093fa9fbcd980dd5fe..0216ddf71a997920c78e181a930b6b3956dd59fe 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 41e90071a4d528cc02054d690f8cc0c4659796f6..53f1cad6110389733ae4a066c4fd481485e4b0bb 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 13d447e33935a5c83466f441fff4da7f651d2481..24e641ebfea19e1ca40a4b883e37d487d0d6f393 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 a96f1d1657a599ba16a1dee8cc6607308b3bf755..4de4549f2b2bddac4f5df217cf6e7d3223a9c56e 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 152be0282b525b52c31cecb146065d0fee8d4040..384221e32dba18975072d2daacae726ece033004 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 4936c26c5aaea80ecc5fd7fea0c7bc442386e2b5..d7838630385798deefe79b2f1e9acd5d0f86f339 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