aboutsummaryrefslogtreecommitdiff
path: root/gcc
diff options
context:
space:
mode:
Diffstat (limited to 'gcc')
-rw-r--r--gcc/ada/ChangeLog18
-rw-r--r--gcc/ada/a-cfhase.adb2
-rw-r--r--gcc/ada/a-cihama.adb2
-rw-r--r--gcc/ada/a-clrefi.adb6
-rw-r--r--gcc/ada/fmap.adb4
-rw-r--r--gcc/ada/freeze.adb2
-rw-r--r--gcc/ada/inline.adb2
-rw-r--r--gcc/ada/lib-xref-spark_specific.adb70
-rw-r--r--gcc/ada/lib-xref.ads4
-rw-r--r--gcc/ada/make.adb2
-rw-r--r--gcc/ada/restrict.adb2
-rw-r--r--gcc/ada/s-regexp.adb4
-rw-r--r--gcc/ada/scng.adb2
-rw-r--r--gcc/ada/sem_ch12.adb2
-rw-r--r--gcc/ada/sem_ch5.adb4
-rw-r--r--gcc/ada/sem_res.adb2
-rw-r--r--gcc/ada/sem_util.adb4
-rw-r--r--gcc/ada/tempdir.adb4
18 files changed, 96 insertions, 40 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 3e0d760..3407bd3 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 ac2ea61..d25705b 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 2cea318..1183100 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 4708bf8..5afde3b 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 f543209..77fa6c0 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 36822ec..ee8a23e 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 bb26c46..0d16aff 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 b38d65b..a396714 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 c463fe9..9d1037c 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 f3ac043..90eb0ed 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 1dbd3d5..fb0e968 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 68cef65..6a44534 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 7bf8ea2..0216ddf 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 41e9007..53f1cad 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 13d447e..24e641e 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 a96f1d1..4de4549 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 152be028..384221e 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 4936c26..d783863 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
generated by cgit v1.1 at 2025-05-01 09:37:01 +0000