mirror of git://gcc.gnu.org/git/gcc.git
[multiple changes]
2011-09-02 Robert Dewar <dewar@adacore.com> * prj-dect.adb, prj-env.adb, prj-nmsc.adb, prj-proc.adb, prj-tree.adb, prj.adb, prj.ads, sem_ch5.adb: Minor reformatting. 2011-09-02 Thomas Quinot <quinot@adacore.com> * sem_attr.adb (Analyze_Attribute, case Unrestriced_Access): Guard against a prefix that is an N_Has_Entity but has no associated entity. 2011-09-02 Yannick Moy <moy@adacore.com> * lib-xref-alfa.adb (Is_Alfa_Reference): Ignore IN parameters in Alfa references. 2011-09-02 Yannick Moy <moy@adacore.com> * opt.ads (Warn_On_Suspicious_Contract): New warning flag. * sem_ch3.adb (Analyze_Declarations): Call checker for suspicious contracts. * sem_ch6.adb, sem_ch6.ads (Check_Subprogram_Contract): New procedure looking for suspicious postconditions. * usage.adb (Usage): New options -gnatw.t and -gnatw.T. * warnsw.adb (Set_Dot_Warning_Switch): Take into account new options -gnatw.t and -gnatw.T. From-SVN: r178448
This commit is contained in:
parent
5415acbd64
commit
67c861780f
|
|
@ -1,3 +1,30 @@
|
|||
2011-09-02 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* prj-dect.adb, prj-env.adb, prj-nmsc.adb, prj-proc.adb, prj-tree.adb,
|
||||
prj.adb, prj.ads, sem_ch5.adb: Minor reformatting.
|
||||
|
||||
2011-09-02 Thomas Quinot <quinot@adacore.com>
|
||||
|
||||
* sem_attr.adb (Analyze_Attribute, case Unrestriced_Access):
|
||||
Guard against a prefix that is an N_Has_Entity but has no
|
||||
associated entity.
|
||||
|
||||
2011-09-02 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* lib-xref-alfa.adb (Is_Alfa_Reference): Ignore IN parameters in Alfa
|
||||
references.
|
||||
|
||||
2011-09-02 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* opt.ads (Warn_On_Suspicious_Contract): New warning flag.
|
||||
* sem_ch3.adb (Analyze_Declarations): Call checker for suspicious
|
||||
contracts.
|
||||
* sem_ch6.adb, sem_ch6.ads (Check_Subprogram_Contract): New
|
||||
procedure looking for suspicious postconditions.
|
||||
* usage.adb (Usage): New options -gnatw.t and -gnatw.T.
|
||||
* warnsw.adb (Set_Dot_Warning_Switch): Take into account new
|
||||
options -gnatw.t and -gnatw.T.
|
||||
|
||||
2011-09-02 Pascal Obry <obry@adacore.com>
|
||||
|
||||
* prj.adb: Minor code refactoring. Move check for null project in
|
||||
|
|
|
|||
|
|
@ -608,11 +608,20 @@ package body Alfa is
|
|||
-- On non-callable entities, the only references of interest are
|
||||
-- reads and writes.
|
||||
|
||||
if Ekind (E) in Overloadable_Kind then
|
||||
return Typ = 's';
|
||||
else
|
||||
return Typ = 'r' or else Typ = 'm';
|
||||
end if;
|
||||
case Ekind (E) is
|
||||
when Overloadable_Kind =>
|
||||
return Typ = 's';
|
||||
|
||||
-- References to IN parameters are not considered in Alfa
|
||||
-- section, as these will be translated as constants in the
|
||||
-- intermediate language for formal verification.
|
||||
|
||||
when E_In_Parameter =>
|
||||
return False;
|
||||
|
||||
when others =>
|
||||
return Typ = 'r' or else Typ = 'm';
|
||||
end case;
|
||||
end Is_Alfa_Reference;
|
||||
|
||||
-------------------
|
||||
|
|
|
|||
|
|
@ -1550,6 +1550,12 @@ package Opt is
|
|||
-- clauses that are affected by non-standard bit-order. The default is
|
||||
-- that this warning is enabled.
|
||||
|
||||
Warn_On_Suspicious_Contract : Boolean := True;
|
||||
-- GNAT
|
||||
-- Set to True to generate warnings for suspicious contracts expressed as
|
||||
-- pragmas or aspects precondition and postcondition. The default is that
|
||||
-- this warning is enabled.
|
||||
|
||||
Warn_On_Suspicious_Modulus_Value : Boolean := True;
|
||||
-- GNAT
|
||||
-- Set to True to generate warnings for suspicious modulus values. The
|
||||
|
|
|
|||
|
|
@ -23,10 +23,6 @@
|
|||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
with GNAT.Case_Util; use GNAT.Case_Util;
|
||||
with GNAT.Spelling_Checker; use GNAT.Spelling_Checker;
|
||||
with GNAT.Strings;
|
||||
|
||||
with Err_Vars; use Err_Vars;
|
||||
with Opt; use Opt;
|
||||
with Prj.Attr; use Prj.Attr;
|
||||
|
|
@ -37,32 +33,34 @@ with Prj.Tree; use Prj.Tree;
|
|||
with Snames;
|
||||
with Uintp; use Uintp;
|
||||
|
||||
with GNAT; use GNAT;
|
||||
with GNAT.Case_Util; use GNAT.Case_Util;
|
||||
with GNAT.Spelling_Checker; use GNAT.Spelling_Checker;
|
||||
with GNAT.Strings;
|
||||
|
||||
package body Prj.Dect is
|
||||
|
||||
use GNAT;
|
||||
|
||||
type Zone is (In_Project, In_Package, In_Case_Construction);
|
||||
-- Used to indicate if we are parsing a package (In_Package),
|
||||
-- a case construction (In_Case_Construction) or none of those two
|
||||
-- (In_Project).
|
||||
-- Used to indicate if we are parsing a package (In_Package), a case
|
||||
-- construction (In_Case_Construction) or none of those two (In_Project).
|
||||
|
||||
procedure Rename_Obsolescent_Attributes
|
||||
(In_Tree : Project_Node_Tree_Ref;
|
||||
Attribute : Project_Node_Id;
|
||||
Current_Package : Project_Node_Id);
|
||||
-- Rename obsolescent attributes in the tree.
|
||||
-- When the attribute has been renamed since its initial introduction in
|
||||
-- the design of projects, we replace the old name in the tree with the
|
||||
-- new name, so that the code does not have to check both names forever.
|
||||
-- Rename obsolescent attributes in the tree. When the attribute has been
|
||||
-- renamed since its initial introduction in the design of projects, we
|
||||
-- replace the old name in the tree with the new name, so that the code
|
||||
-- does not have to check both names forever.
|
||||
|
||||
procedure Check_Attribute_Allowed
|
||||
(In_Tree : Project_Node_Tree_Ref;
|
||||
Project : Project_Node_Id;
|
||||
Attribute : Project_Node_Id;
|
||||
Flags : Processing_Flags);
|
||||
-- Check whether the attribute is valid in this project.
|
||||
-- In particular, depending on the type of project (qualifier), some
|
||||
-- attributes might be disabled.
|
||||
-- Check whether the attribute is valid in this project. In particular,
|
||||
-- depending on the type of project (qualifier), some attributes might
|
||||
-- be disabled.
|
||||
|
||||
procedure Check_Package_Allowed
|
||||
(In_Tree : Project_Node_Tree_Ref;
|
||||
|
|
@ -244,7 +242,7 @@ package body Prj.Dect is
|
|||
begin
|
||||
case Qualif is
|
||||
when Aggregate | Aggregate_Library =>
|
||||
if Name = Snames.Name_Languages
|
||||
if Name = Snames.Name_Languages
|
||||
or else Name = Snames.Name_Source_Files
|
||||
or else Name = Snames.Name_Source_List_File
|
||||
or else Name = Snames.Name_Locally_Removed_Files
|
||||
|
|
|
|||
|
|
@ -778,10 +778,9 @@ package body Prj.Env is
|
|||
In_Tree : Project_Tree_Ref;
|
||||
Name : out Path_Name_Type)
|
||||
is
|
||||
File : File_Descriptor := Invalid_FD;
|
||||
|
||||
Buffer : String_Access := new String (1 .. Buffer_Initial);
|
||||
Buffer_Last : Natural := 0;
|
||||
File : File_Descriptor := Invalid_FD;
|
||||
Buffer : String_Access := new String (1 .. Buffer_Initial);
|
||||
Buffer_Last : Natural := 0;
|
||||
|
||||
procedure Put_Name_Buffer;
|
||||
-- Put the line contained in the Name_Buffer in the global buffer
|
||||
|
|
@ -833,7 +832,7 @@ package body Prj.Env is
|
|||
if Source.Replaced_By = No_Source
|
||||
and then Source.Path.Name /= No_Path
|
||||
and then (Source.Language.Config.Kind = File_Based
|
||||
or else Source.Unit /= No_Unit_Index)
|
||||
or else Source.Unit /= No_Unit_Index)
|
||||
then
|
||||
if Source.Unit /= No_Unit_Index then
|
||||
|
||||
|
|
@ -1141,7 +1140,7 @@ package body Prj.Env is
|
|||
|
||||
if not Main_Project_Only
|
||||
or else (Unit.File_Names (Spec) /= null
|
||||
and then Unit.File_Names (Spec).Project = The_Project)
|
||||
and then Unit.File_Names (Spec).Project = The_Project)
|
||||
then
|
||||
declare
|
||||
Current_Name : File_Name_Type;
|
||||
|
|
@ -1668,7 +1667,7 @@ package body Prj.Env is
|
|||
-- For the object path, we make a distinction depending on
|
||||
-- Including_Libraries.
|
||||
|
||||
if Objects_Path and then Including_Libraries then
|
||||
if Objects_Path and Including_Libraries then
|
||||
if Project.Objects_Path_File_With_Libs = No_Path then
|
||||
Object_Path_Table.Init (Object_Paths);
|
||||
Process_Object_Dirs := True;
|
||||
|
|
@ -1688,7 +1687,7 @@ package body Prj.Env is
|
|||
-- If there is something to do, set Seen to False for all projects,
|
||||
-- then call the recursive procedure Add for Project.
|
||||
|
||||
if Process_Source_Dirs or else Process_Object_Dirs then
|
||||
if Process_Source_Dirs or Process_Object_Dirs then
|
||||
For_All_Projects (Project, In_Tree, Dummy);
|
||||
end if;
|
||||
|
||||
|
|
|
|||
|
|
@ -36,8 +36,9 @@ with Sinput.P;
|
|||
with Snames; use Snames;
|
||||
with Targparm; use Targparm;
|
||||
|
||||
with Ada; use Ada;
|
||||
with Ada.Characters.Handling; use Ada.Characters.Handling;
|
||||
with Ada.Directories; use Ada, Ada.Directories;
|
||||
with Ada.Directories; use Ada.Directories;
|
||||
with Ada.Strings; use Ada.Strings;
|
||||
with Ada.Strings.Fixed; use Ada.Strings.Fixed;
|
||||
with Ada.Strings.Maps.Constants; use Ada.Strings.Maps.Constants;
|
||||
|
|
@ -5194,13 +5195,13 @@ package body Prj.Nmsc is
|
|||
|
||||
No_Sources : constant Boolean :=
|
||||
((not Source_Files.Default
|
||||
and then Source_Files.Values = Nil_String)
|
||||
and then Source_Files.Values = Nil_String)
|
||||
or else
|
||||
(not Source_Dirs.Default
|
||||
and then Source_Dirs.Values = Nil_String)
|
||||
and then Source_Dirs.Values = Nil_String)
|
||||
or else
|
||||
(not Languages.Default
|
||||
and then Languages.Values = Nil_String))
|
||||
and then Languages.Values = Nil_String))
|
||||
and then Project.Extends = No_Project;
|
||||
|
||||
-- Start of processing for Get_Directories
|
||||
|
|
@ -5248,6 +5249,7 @@ package body Prj.Nmsc is
|
|||
Externally_Built => Project.Externally_Built);
|
||||
|
||||
if not Dir_Exists and then not Project.Externally_Built then
|
||||
|
||||
-- The object directory does not exist, report an error if the
|
||||
-- project is not externally built.
|
||||
|
||||
|
|
@ -7270,9 +7272,9 @@ package body Prj.Nmsc is
|
|||
|
||||
-- Loop through subdirectories
|
||||
|
||||
Source_Dir := Project.Project.Source_Dirs;
|
||||
Src_Dir_Rank := Project.Project.Source_Dir_Ranks;
|
||||
|
||||
Source_Dir := Project.Project.Source_Dirs;
|
||||
while Source_Dir /= Nil_String loop
|
||||
begin
|
||||
Num_Nod := Shared.Number_Lists.Table (Src_Dir_Rank);
|
||||
|
|
@ -7322,7 +7324,7 @@ package body Prj.Nmsc is
|
|||
|
||||
if not Opt.Follow_Links_For_Files
|
||||
or else Is_Regular_File
|
||||
(Display_Source_Directory & Name (1 .. Last))
|
||||
(Display_Source_Directory & Name (1 .. Last))
|
||||
then
|
||||
Name_Len := Last;
|
||||
Name_Buffer (1 .. Name_Len) := Name (1 .. Last);
|
||||
|
|
|
|||
|
|
@ -1364,7 +1364,7 @@ package body Prj.Proc is
|
|||
Reset_Tree => Reset_Tree);
|
||||
|
||||
if Project_Qualifier_Of
|
||||
(From_Project_Node, From_Project_Node_Tree) /= Configuration
|
||||
(From_Project_Node, From_Project_Node_Tree) /= Configuration
|
||||
then
|
||||
Process_Project_Tree_Phase_2
|
||||
(In_Tree => In_Tree,
|
||||
|
|
@ -1566,8 +1566,8 @@ package body Prj.Proc is
|
|||
-- declaration.
|
||||
|
||||
Copy_Package_Declarations
|
||||
(From =>
|
||||
Shared.Packages.Table (Renamed_Package).Decl,
|
||||
(From => Shared.Packages.Table
|
||||
(Renamed_Package).Decl,
|
||||
To => Shared.Packages.Table (New_Pkg).Decl,
|
||||
New_Loc => Location_Of (Current_Item, Node_Tree),
|
||||
Restricted => False,
|
||||
|
|
@ -2577,6 +2577,7 @@ package body Prj.Proc is
|
|||
Loaded_Project : Prj.Tree.Project_Node_Id;
|
||||
Success : Boolean := True;
|
||||
Tree : Project_Tree_Ref;
|
||||
|
||||
begin
|
||||
if Project.Qualifier not in Aggregate_Project then
|
||||
return;
|
||||
|
|
@ -2711,6 +2712,7 @@ package body Prj.Proc is
|
|||
end loop;
|
||||
|
||||
if Attribute1 = No_Variable or else Attr_Value1.Value.Default then
|
||||
|
||||
-- Attribute Languages is not declared in the extending project.
|
||||
-- Check if it is declared in the project being extended.
|
||||
|
||||
|
|
@ -2754,8 +2756,8 @@ package body Prj.Proc is
|
|||
Imported : Project_List;
|
||||
Declaration_Node : Project_Node_Id := Empty_Node;
|
||||
|
||||
Name : constant Name_Id :=
|
||||
Name_Of (From_Project_Node, From_Project_Node_Tree);
|
||||
Name : constant Name_Id :=
|
||||
Name_Of (From_Project_Node, From_Project_Node_Tree);
|
||||
|
||||
Name_Node : constant Tree_Private_Part.Project_Name_And_Node :=
|
||||
Tree_Private_Part.Projects_Htable.Get
|
||||
|
|
@ -2837,7 +2839,9 @@ package body Prj.Proc is
|
|||
Initialize_And_Copy (Child_Env, Copy_From => Env);
|
||||
|
||||
elsif Project.Qualifier = Aggregate_Library then
|
||||
|
||||
-- The child environment is the same as the current one
|
||||
|
||||
Child_Env := Env;
|
||||
|
||||
else
|
||||
|
|
@ -2888,9 +2892,9 @@ package body Prj.Proc is
|
|||
|
||||
if Project.Qualifier = Aggregate_Library then
|
||||
declare
|
||||
L : Aggregated_Project_List :=
|
||||
Project.Aggregated_Projects;
|
||||
L : Aggregated_Project_List;
|
||||
begin
|
||||
L := Project.Aggregated_Projects;
|
||||
while L /= null loop
|
||||
Project.Imported_Projects :=
|
||||
new Project_List_Element'
|
||||
|
|
|
|||
|
|
@ -104,6 +104,7 @@ package body Prj.Tree is
|
|||
Zone := In_Tree.Project_Nodes.Table (To).Comments;
|
||||
|
||||
if No (Zone) then
|
||||
|
||||
-- Create new N_Comment_Zones node
|
||||
|
||||
Project_Node_Table.Increment_Last (In_Tree.Project_Nodes);
|
||||
|
|
|
|||
|
|
@ -393,9 +393,7 @@ package body Prj is
|
|||
if Iter.Language = No_Language_Index then
|
||||
if Iter.All_Projects then
|
||||
Iter.Project := Iter.Project.Next;
|
||||
|
||||
Project_Changed (Iter);
|
||||
|
||||
else
|
||||
Iter.Project := null;
|
||||
end if;
|
||||
|
|
@ -582,7 +580,6 @@ package body Prj is
|
|||
|
||||
begin
|
||||
Iterator := For_Each_Source (In_Tree => Tree, Project => Proj);
|
||||
|
||||
while Element (Iterator) /= No_Source loop
|
||||
if Element (Iterator).File = Base_Name
|
||||
and then (Index = 0 or else Element (Iterator).Index = Index)
|
||||
|
|
@ -1662,6 +1659,7 @@ package body Prj is
|
|||
Root_Tree : Project_Tree_Ref)
|
||||
is
|
||||
Agg : Aggregated_Project_List;
|
||||
|
||||
begin
|
||||
Action (Root_Project, Root_Tree);
|
||||
|
||||
|
|
@ -1674,6 +1672,8 @@ package body Prj is
|
|||
end if;
|
||||
end For_Project_And_Aggregated;
|
||||
|
||||
-- Package initialization for Prj
|
||||
|
||||
begin
|
||||
-- Make sure that the standard config and user project file extensions are
|
||||
-- compatible with canonical case file naming.
|
||||
|
|
|
|||
|
|
@ -77,8 +77,8 @@ package Prj is
|
|||
-- Aggregate_Library: aggregate library project is ...
|
||||
-- Configuration: configuration project is ...
|
||||
|
||||
subtype Aggregate_Project
|
||||
is Project_Qualifier range Aggregate .. Aggregate_Library;
|
||||
subtype Aggregate_Project is
|
||||
Project_Qualifier range Aggregate .. Aggregate_Library;
|
||||
|
||||
All_Packages : constant String_List_Access;
|
||||
-- Default value of parameter Packages of procedures Parse, in Prj.Pars and
|
||||
|
|
|
|||
|
|
@ -4942,7 +4942,10 @@ package body Sem_Attr is
|
|||
if Comes_From_Source (N) then
|
||||
Check_Restriction (No_Unchecked_Access, N);
|
||||
|
||||
if Nkind (P) in N_Has_Entity and then Is_Object (Entity (P)) then
|
||||
if Nkind (P) in N_Has_Entity
|
||||
and then Present (Entity (P))
|
||||
and then Is_Object (Entity (P))
|
||||
then
|
||||
Check_Restriction (No_Implicit_Aliasing, N);
|
||||
end if;
|
||||
end if;
|
||||
|
|
|
|||
|
|
@ -2192,6 +2192,8 @@ package body Sem_Ch3 is
|
|||
Prag := Next_Pragma (Prag);
|
||||
end loop;
|
||||
|
||||
Check_Subprogram_Contract (Sent);
|
||||
|
||||
Prag := Spec_TC_List (Contract (Sent));
|
||||
while Present (Prag) loop
|
||||
Analyze_TC_In_Decl_Part (Prag, Sent);
|
||||
|
|
|
|||
|
|
@ -2261,9 +2261,9 @@ package body Sem_Ch5 is
|
|||
Analyze (Subt);
|
||||
end if;
|
||||
|
||||
-- If domain of iteration is an expression, create a declaration for it,
|
||||
-- so that finalization actions are introduced outside of the loop.
|
||||
-- The declaration must be a renaming because the body of the loop may
|
||||
-- If domain of iteration is an expression, create a declaration for
|
||||
-- it, so that finalization actions are introduced outside of the loop.
|
||||
-- The declaration must be a renaming because the body of the loop may
|
||||
-- assign to elements.
|
||||
|
||||
if not Is_Entity_Name (Iter_Name) then
|
||||
|
|
|
|||
|
|
@ -5454,6 +5454,207 @@ package body Sem_Ch6 is
|
|||
end if;
|
||||
end Check_Returns;
|
||||
|
||||
-------------------------------
|
||||
-- Check_Subprogram_Contract --
|
||||
-------------------------------
|
||||
|
||||
procedure Check_Subprogram_Contract (Spec_Id : Entity_Id) is
|
||||
|
||||
-- Inherited : constant Subprogram_List :=
|
||||
-- Inherited_Subprograms (Spec_Id);
|
||||
-- List of subprograms inherited by this subprogram
|
||||
|
||||
Last_Postcondition : Node_Id := Empty;
|
||||
-- Last postcondition on the subprogram, or else Empty if either no
|
||||
-- postcondition or only inherited postconditions.
|
||||
|
||||
Attribute_Result_Mentioned : Boolean := False;
|
||||
-- Whether attribute 'Result is mentioned in a postcondition
|
||||
|
||||
Post_State_Mentioned : Boolean := False;
|
||||
-- Whether some expression mentioned in a postcondition can have a
|
||||
-- different value in the post-state than in the pre-state.
|
||||
|
||||
function Check_Attr_Result (N : Node_Id) return Traverse_Result;
|
||||
-- Check whether N is a reference to the attribute 'Result, and if so
|
||||
-- set Attribute_Result_Mentioned and return Abandon. Otherwise return
|
||||
-- OK.
|
||||
|
||||
function Check_Post_State (N : Node_Id) return Traverse_Result;
|
||||
-- Check whether the value of evaluating N can be different in the
|
||||
-- post-state, compared to the same evaluation in the pre-state, and
|
||||
-- if so set Post_State_Mentioned and return Abandon. Return Skip on
|
||||
-- reference to attribute 'Old, in order to ignore its prefix, which
|
||||
-- is precisely evaluated in the pre-state. Otherwise return OK.
|
||||
|
||||
procedure Process_Post_Conditions
|
||||
(Spec : Node_Id;
|
||||
Class : Boolean);
|
||||
-- This processes the Spec_PPC_List from Spec, processing any
|
||||
-- postconditions from the list. If Class is True, then only
|
||||
-- postconditions marked with Class_Present are considered. The
|
||||
-- caller has checked that Spec_PPC_List is non-Empty.
|
||||
|
||||
function Find_Attribute_Result is new Traverse_Func (Check_Attr_Result);
|
||||
|
||||
function Find_Post_State is new Traverse_Func (Check_Post_State);
|
||||
|
||||
-----------------------
|
||||
-- Check_Attr_Result --
|
||||
-----------------------
|
||||
|
||||
function Check_Attr_Result (N : Node_Id) return Traverse_Result is
|
||||
begin
|
||||
if Nkind (N) = N_Attribute_Reference
|
||||
and then
|
||||
Get_Attribute_Id (Attribute_Name (N)) = Attribute_Result
|
||||
then
|
||||
Attribute_Result_Mentioned := True;
|
||||
return Abandon;
|
||||
else
|
||||
return OK;
|
||||
end if;
|
||||
end Check_Attr_Result;
|
||||
|
||||
----------------------
|
||||
-- Check_Post_State --
|
||||
----------------------
|
||||
|
||||
function Check_Post_State (N : Node_Id) return Traverse_Result is
|
||||
Found : Boolean := False;
|
||||
|
||||
begin
|
||||
case Nkind (N) is
|
||||
when N_Function_Call |
|
||||
N_Explicit_Dereference =>
|
||||
Found := True;
|
||||
|
||||
when N_Identifier |
|
||||
N_Expanded_Name =>
|
||||
declare
|
||||
E : constant Entity_Id := Entity (N);
|
||||
begin
|
||||
if Is_Entity_Name (N)
|
||||
and then Present (E)
|
||||
and then Ekind (E) in Assignable_Kind
|
||||
then
|
||||
Found := True;
|
||||
end if;
|
||||
end;
|
||||
|
||||
when N_Attribute_Reference =>
|
||||
case Get_Attribute_Id (Attribute_Name (N)) is
|
||||
when Attribute_Old =>
|
||||
return Skip;
|
||||
when Attribute_Result =>
|
||||
Found := True;
|
||||
when others =>
|
||||
null;
|
||||
end case;
|
||||
|
||||
when others =>
|
||||
null;
|
||||
end case;
|
||||
|
||||
if Found then
|
||||
Post_State_Mentioned := True;
|
||||
return Abandon;
|
||||
else
|
||||
return OK;
|
||||
end if;
|
||||
end Check_Post_State;
|
||||
|
||||
-----------------------------
|
||||
-- Process_Post_Conditions --
|
||||
-----------------------------
|
||||
|
||||
procedure Process_Post_Conditions
|
||||
(Spec : Node_Id;
|
||||
Class : Boolean)
|
||||
is
|
||||
Prag : Node_Id;
|
||||
Arg : Node_Id;
|
||||
Ignored : Traverse_Final_Result;
|
||||
pragma Unreferenced (Ignored);
|
||||
|
||||
begin
|
||||
Prag := Spec_PPC_List (Contract (Spec));
|
||||
|
||||
loop
|
||||
Arg := First (Pragma_Argument_Associations (Prag));
|
||||
|
||||
-- Since pre- and postconditions are listed in reverse order, the
|
||||
-- first postcondition in the list is the last in the source.
|
||||
|
||||
if Pragma_Name (Prag) = Name_Postcondition
|
||||
and then not Class
|
||||
and then No (Last_Postcondition)
|
||||
then
|
||||
Last_Postcondition := Prag;
|
||||
end if;
|
||||
|
||||
-- For functions, look for presence of 'Result in postcondition
|
||||
|
||||
if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
|
||||
Ignored := Find_Attribute_Result (Arg);
|
||||
end if;
|
||||
|
||||
-- For each individual non-inherited postcondition, look for
|
||||
-- presence of an expression that could be evaluated differently
|
||||
-- in post-state.
|
||||
|
||||
if Pragma_Name (Prag) = Name_Postcondition
|
||||
and then not Class
|
||||
then
|
||||
Post_State_Mentioned := False;
|
||||
Ignored := Find_Post_State (Arg);
|
||||
|
||||
if not Post_State_Mentioned then
|
||||
Error_Msg_N ("?postcondition only refers to pre-state",
|
||||
Prag);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
Prag := Next_Pragma (Prag);
|
||||
exit when No (Prag);
|
||||
end loop;
|
||||
end Process_Post_Conditions;
|
||||
|
||||
-- Start of processing for Check_Subprogram_Contract
|
||||
|
||||
begin
|
||||
if not Warn_On_Suspicious_Contract then
|
||||
return;
|
||||
end if;
|
||||
|
||||
if Present (Spec_PPC_List (Contract (Spec_Id))) then
|
||||
Process_Post_Conditions (Spec_Id, Class => False);
|
||||
end if;
|
||||
|
||||
-- Process inherited postconditions
|
||||
|
||||
-- Code is currently commented out as, in some cases, it causes crashes
|
||||
-- because Direct_Primitive_Operations is not available for a private
|
||||
-- type. This may cause more warnings to be issued than necessary.
|
||||
|
||||
-- for J in Inherited'Range loop
|
||||
-- if Present (Spec_PPC_List (Contract (Inherited (J)))) then
|
||||
-- Process_Post_Conditions (Inherited (J), Class => True);
|
||||
-- end if;
|
||||
-- end loop;
|
||||
|
||||
-- Issue warning for functions whose postcondition does not mention
|
||||
-- 'Result after all postconditions have been processed.
|
||||
|
||||
if Ekind_In (Spec_Id, E_Function, E_Generic_Function)
|
||||
and then Present (Last_Postcondition)
|
||||
and then not Attribute_Result_Mentioned
|
||||
then
|
||||
Error_Msg_N ("?function postcondition does not mention result",
|
||||
Last_Postcondition);
|
||||
end if;
|
||||
end Check_Subprogram_Contract;
|
||||
|
||||
----------------------------
|
||||
-- Check_Subprogram_Order --
|
||||
----------------------------
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- S p e c --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2011, 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- --
|
||||
|
|
@ -113,6 +113,10 @@ package Sem_Ch6 is
|
|||
-- type-conformant subprogram that becomes hidden by the new subprogram.
|
||||
-- Is_Primitive indicates whether the subprogram is primitive.
|
||||
|
||||
procedure Check_Subprogram_Contract (Spec_Id : Entity_Id);
|
||||
-- Spec_Id is the spec entity for a subprogram. This routine issues
|
||||
-- warnings on suspicious contracts if Warn_On_Suspicious_Contract is set.
|
||||
|
||||
procedure Check_Subtype_Conformant
|
||||
(New_Id : Entity_Id;
|
||||
Old_Id : Entity_Id;
|
||||
|
|
|
|||
|
|
@ -484,6 +484,8 @@ begin
|
|||
Write_Line (" .S* turn off warnings for overridden size clause");
|
||||
Write_Line (" t turn on warnings for tracking deleted code");
|
||||
Write_Line (" T* turn off warnings for tracking deleted code");
|
||||
Write_Line (" .t* turn on warnings for suspicious contract");
|
||||
Write_Line (" .T turn off warnings for suspicious contract");
|
||||
Write_Line (" u+ turn on warnings for unused entity");
|
||||
Write_Line (" U* turn off warnings for unused entity");
|
||||
Write_Line (" .u turn on warnings for unordered enumeration");
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1999-2010, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1999-2011, 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- --
|
||||
|
|
@ -143,6 +143,12 @@ package body Warnsw is
|
|||
when 'S' =>
|
||||
Warn_On_Overridden_Size := False;
|
||||
|
||||
when 't' =>
|
||||
Warn_On_Suspicious_Contract := True;
|
||||
|
||||
when 'T' =>
|
||||
Warn_On_Suspicious_Contract := False;
|
||||
|
||||
when 'u' =>
|
||||
Warn_On_Unordered_Enumeration_Type := True;
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue