From 704228bdcc8e23d3ffd65748acbb6ee9ecba0083 Mon Sep 17 00:00:00 2001 From: Yannick Moy 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 * 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 * 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 3e0d760a659..3407bd3b4a9 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,21 @@ +2015-10-20 Yannick Moy + + * 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 + + * 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 * 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 ac2ea61adb4..d25705bfc71 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 2cea3189511..11831004dea 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 4708bf8f34c..5afde3b616c 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 f5432096e28..77fa6c0d78d 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 36822ec05b6..ee8a23e5f1c 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 bb26c4639d8..0d16affb06e 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 b38d65b23dd..a39671494fa 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 c463fe93737..9d1037ca053 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 f3ac043a7ac..90eb0ed1c9c 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 1dbd3d551ad..fb0e9682a41 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 68cef650aac..6a445340b14 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 7bf8ea2eacc..0216ddf71a9 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 41e90071a4d..53f1cad6110 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 13d447e3393..24e641ebfea 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 a96f1d1657a..4de4549f2b2 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 152be0282b5..384221e32db 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 4936c26c5aa..d7838630385 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 -- 2.30.2