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
This commit is contained in:
Yannick Moy 2015-10-20 12:42:53 +00:00 committed by Arnaud Charlet
parent c83075965b
commit 704228bdcc
18 changed files with 96 additions and 40 deletions

View File

@ -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,

View File

@ -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);

View File

@ -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);

View File

@ -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

View File

@ -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

View File

@ -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;

View File

@ -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));

View File

@ -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 =>

View File

@ -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);

View File

@ -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;

View File

@ -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;

View File

@ -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));

View File

@ -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;

View File

@ -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

View File

@ -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);

View File

@ -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

View File

@ -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

View File

@ -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