+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
-- 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;
-------------------
-- 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
-- --
------------------------------------------------------------------------------
-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;
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;
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
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
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
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;
-- 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;
-- 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;
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;
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
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.
-- 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);
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);
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,
-- 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,
Loaded_Project : Prj.Tree.Project_Node_Id;
Success : Boolean := True;
Tree : Project_Tree_Ref;
+
begin
if Project.Qualifier not in Aggregate_Project then
return;
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.
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
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
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'
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);
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;
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)
Root_Tree : Project_Tree_Ref)
is
Agg : Aggregated_Project_List;
+
begin
Action (Root_Project, Root_Tree);
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.
-- 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
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;
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);
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
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 --
----------------------------
-- --
-- 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- --
-- 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;
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");
-- --
-- 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- --
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;
projects / gcc.git / commitdiff