A contract, either in GNAT syntax (pragma precondition and postcondition) or
Ada 2012 aspect syntax, is suspicious when: for a function, it does not mention
the result; for a function or procedure, it only refers to the pre-state. GNAT
now detects these cases on the following code:
$ gcc -c -gnatc -gnat12 p.ads
p.ads:3:06: warning: postcondition only refers to pre-state
p.ads:3:06: warning: function postcondition does not mention result
p.ads:5:06: warning: postcondition only refers to pre-state
---
1 package P is
2 function A_Is_Positive (X : Integer) return Boolean with
3 Post => X >= 0;
4 procedure A_Incr (X : in Integer; Y : out Integer) with
5 Post => X = X + 1;
6 end P;
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-09-02 Yannick Moy <m...@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.
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 178440)
+++ sem_ch3.adb (working copy)
@@ -2192,6 +2192,8 @@
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);
Index: usage.adb
===================================================================
--- usage.adb (revision 178381)
+++ usage.adb (working copy)
@@ -484,6 +484,8 @@
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");
Index: warnsw.adb
===================================================================
--- warnsw.adb (revision 178381)
+++ warnsw.adb (working copy)
@@ -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 @@
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;
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 178411)
+++ sem_ch6.adb (working copy)
@@ -5454,6 +5454,207 @@
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 --
----------------------------
Index: sem_ch6.ads
===================================================================
--- sem_ch6.ads (revision 178381)
+++ sem_ch6.ads (working copy)
@@ -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 @@
-- 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;
Index: opt.ads
===================================================================
--- opt.ads (revision 178381)
+++ opt.ads (working copy)
@@ -1550,6 +1550,12 @@
-- 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
