From a15d8d347f13ffff51c89f06c606b79a1afa2e67 Mon Sep 17 00:00:00 2001 From: charlet Date: Fri, 2 Sep 2011 09:22:16 +0000 Subject: [PATCH] 2011-09-02 Robert Dewar * 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 * 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 * lib-xref-alfa.adb (Is_Alfa_Reference): Ignore IN parameters in Alfa references. 2011-09-02 Yannick Moy * 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. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@178448 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/ChangeLog | 27 +++++++ gcc/ada/lib-xref-alfa.adb | 19 +++-- gcc/ada/opt.ads | 6 ++ gcc/ada/prj-dect.adb | 32 ++++---- gcc/ada/prj-env.adb | 15 ++-- gcc/ada/prj-nmsc.adb | 14 ++-- gcc/ada/prj-proc.adb | 18 +++-- gcc/ada/prj-tree.adb | 1 + gcc/ada/prj.adb | 6 +- gcc/ada/prj.ads | 4 +- gcc/ada/sem_attr.adb | 5 +- gcc/ada/sem_ch3.adb | 2 + gcc/ada/sem_ch5.adb | 6 +- gcc/ada/sem_ch6.adb | 201 ++++++++++++++++++++++++++++++++++++++++++++++ gcc/ada/sem_ch6.ads | 6 +- gcc/ada/usage.adb | 2 + gcc/ada/warnsw.adb | 8 +- 17 files changed, 318 insertions(+), 54 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 9a5fdea93c2..6abbf344980 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,30 @@ +2011-09-02 Robert Dewar + + * 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 + + * 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 + + * lib-xref-alfa.adb (Is_Alfa_Reference): Ignore IN parameters in Alfa + references. + +2011-09-02 Yannick Moy + + * 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 * prj.adb: Minor code refactoring. Move check for null project in diff --git a/gcc/ada/lib-xref-alfa.adb b/gcc/ada/lib-xref-alfa.adb index 74d1421b915..ce9546327f3 100644 --- a/gcc/ada/lib-xref-alfa.adb +++ b/gcc/ada/lib-xref-alfa.adb @@ -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; ------------------- diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index d2874d4ad49..9e4ee4a7f11 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -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 diff --git a/gcc/ada/prj-dect.adb b/gcc/ada/prj-dect.adb index dae54800cf9..b1a1738412c 100644 --- a/gcc/ada/prj-dect.adb +++ b/gcc/ada/prj-dect.adb @@ -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; -package body Prj.Dect is +with GNAT; use GNAT; +with GNAT.Case_Util; use GNAT.Case_Util; +with GNAT.Spelling_Checker; use GNAT.Spelling_Checker; +with GNAT.Strings; - use GNAT; +package body Prj.Dect is 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 diff --git a/gcc/ada/prj-env.adb b/gcc/ada/prj-env.adb index 734ef49b12b..9f29313a0b6 100644 --- a/gcc/ada/prj-env.adb +++ b/gcc/ada/prj-env.adb @@ -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; diff --git a/gcc/ada/prj-nmsc.adb b/gcc/ada/prj-nmsc.adb index 63b434f64d1..2c8d96a171e 100644 --- a/gcc/ada/prj-nmsc.adb +++ b/gcc/ada/prj-nmsc.adb @@ -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); diff --git a/gcc/ada/prj-proc.adb b/gcc/ada/prj-proc.adb index e8ba9912978..269bc4552db 100644 --- a/gcc/ada/prj-proc.adb +++ b/gcc/ada/prj-proc.adb @@ -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' diff --git a/gcc/ada/prj-tree.adb b/gcc/ada/prj-tree.adb index 2b420e1fd63..8072c9daae4 100644 --- a/gcc/ada/prj-tree.adb +++ b/gcc/ada/prj-tree.adb @@ -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); diff --git a/gcc/ada/prj.adb b/gcc/ada/prj.adb index 3a2ef4ed1f9..7795cc9c505 100644 --- a/gcc/ada/prj.adb +++ b/gcc/ada/prj.adb @@ -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. diff --git a/gcc/ada/prj.ads b/gcc/ada/prj.ads index 0b0dee6a935..e88455dec3c 100644 --- a/gcc/ada/prj.ads +++ b/gcc/ada/prj.ads @@ -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 diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index d09e3b5c195..480e9a62c8e 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -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; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 6a55aa93fee..4102bea4378 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -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); diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index b5584e64d6e..5a2d2b37216 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -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 diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 7b4bf913ab6..648cdcb2e50 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -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 -- ---------------------------- diff --git a/gcc/ada/sem_ch6.ads b/gcc/ada/sem_ch6.ads index 96d967b128d..1ca6f3bebdb 100644 --- a/gcc/ada/sem_ch6.ads +++ b/gcc/ada/sem_ch6.ads @@ -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; diff --git a/gcc/ada/usage.adb b/gcc/ada/usage.adb index a4f0948369a..1d79f66a0a7 100644 --- a/gcc/ada/usage.adb +++ b/gcc/ada/usage.adb @@ -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"); diff --git a/gcc/ada/warnsw.adb b/gcc/ada/warnsw.adb index c226f3bf48c..96a8e8f5df6 100644 --- a/gcc/ada/warnsw.adb +++ b/gcc/ada/warnsw.adb @@ -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; -- 2.11.0