+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,
end loop;
end Find_Equivalent_Key;
- -- Start of processing of Equivalent_Sets
+ -- Start of processing for Equivalent_Sets
begin
return Is_Equivalent (Left, Right);
Busy : With_Busy (Container.HT.TC'Unrestricted_Access);
- -- Start of processing Iterate
+ -- Start of processing for Iterate
begin
Local_Iterate (Container.HT);
-- --
-- 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- --
end loop;
end Get_Line;
- -- Start or Recurse
+ -- Start of processing for Recurse
begin
Last_Arg := 0;
raise;
end Recurse;
- -- Start of Arguments_From
+ -- Start of processing for Arguments_From
begin
-- The job is done by procedure Recurse
-- --
-- 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- --
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
end if;
end Process_Flist;
- -- Start or processing for Freeze_All_Ent
+ -- Start of processing for Freeze_All_Ent
begin
E := From;
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));
-- --
-- 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- --
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
Traverse_Compilation_Unit
(CU => Cunit (Uspec),
Process => Detect_And_Add_SPARK_Scope'Access,
- Inside_Stubs => False);
+ Inside_Stubs => True);
end if;
end if;
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 --
-------------------------------
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 =>
-- 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);
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;
-- Just checking, SPARK does not allow restrictions to be set ???
- if CodePeer_Mode or GNATprove_Mode then
+ if CodePeer_Mode then
return;
end if;
-- --
-- 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- --
return J;
end Next_Sub_Expression;
- -- Start of Create_Primary_Table
+ -- Start of processing for Create_Primary_Table
begin
Table.all := (others => (others => 0));
end loop;
end Scan_Integer;
- -- Start of Processing for Nlit
+ -- Start of processing for Nlit
begin
Base := 10;
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
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,
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);
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
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);
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
-- --
-- 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- --
end if;
end Directory;
- -- Start of processing Tempdir
+ -- Start of processing for Create_Temp_File
begin
if Temp_Dir'Length /= 0 then
projects / gcc.git / commitdiff