===================================================================
@@ -2196,19 +2196,26 @@
Spec := Specification (Original_Node (Decl));
Sent := Defining_Unit_Name (Spec);
+ -- Analyze preconditions and postconditions
+
Prag := Spec_PPC_List (Contract (Sent));
while Present (Prag) loop
Analyze_PPC_In_Decl_Part (Prag, Sent);
Prag := Next_Pragma (Prag);
end loop;
- Check_Subprogram_Contract (Sent);
+ -- Analyze contract-cases and test-cases
Prag := Spec_CTC_List (Contract (Sent));
while Present (Prag) loop
Analyze_CTC_In_Decl_Part (Prag, Sent);
Prag := Next_Pragma (Prag);
end loop;
+
+ -- At this point, entities have been attached to identifiers.
+ -- This is required to be able to detect suspicious contracts.
+
+ Check_Subprogram_Contract (Sent);
end if;
Next (Decl);
===================================================================
@@ -5696,9 +5696,11 @@
@emph{Activate warnings on suspicious contracts.}
@cindex @option{-gnatw.t} (@command{gcc})
This switch activates warnings on suspicious postconditions (whether a
-pragma @code{Postcondition} or a @code{Post} aspect in Ada 2012). A
-function postcondition is suspicious when it does not mention the result
-of the function. A procedure postcondition is suspicious when it only
+pragma @code{Postcondition} or a @code{Post} aspect in Ada 2012)
+and suspicious contract cases (pragma @code{Contract_Case}). A
+function postcondition or contract case is suspicious when no postcondition
+or contract case for this function mentions the result of the function.
+A procedure postcondition or contract case is suspicious when it only
refers to the pre-state of the procedure, because in that case it should
rather be expressed as a precondition. The default is that such warnings
are not generated. This warning can also be turned on using @option{-gnatwa}.
===================================================================
@@ -6953,6 +6953,9 @@
-- Last postcondition on the subprogram, or else Empty if either no
-- postcondition or only inherited postconditions.
+ Last_Contract_Case : Node_Id := Empty;
+ -- Last contract-case on the subprogram, or else Empty
+
Attribute_Result_Mentioned : Boolean := False;
-- Whether attribute 'Result is mentioned in a postcondition
@@ -6971,9 +6974,14 @@
-- reference to attribute 'Old, in order to ignore its prefix, which
-- is precisely evaluated in the pre-state. Otherwise return OK.
+ procedure Process_Contract_Cases (Spec : Node_Id);
+ -- This processes the Spec_CTC_List from Spec, processing any contract
+ -- case from the list. The caller has checked that Spec_CTC_List is
+ -- non-Empty.
+
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
+ -- postcondition 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.
@@ -7056,6 +7064,57 @@
end if;
end Check_Post_State;
+ ----------------------------
+ -- Process_Contract_Cases --
+ ----------------------------
+
+ procedure Process_Contract_Cases (Spec : Node_Id) is
+ Prag : Node_Id;
+ Arg : Node_Id;
+ Ignored : Traverse_Final_Result;
+ pragma Unreferenced (Ignored);
+
+ begin
+ Prag := Spec_CTC_List (Contract (Spec));
+
+ loop
+ -- Retrieve the Ensures component of the contract-case, if any
+
+ Arg := Get_Ensures_From_Case_Pragma (Prag);
+
+ if Pragma_Name (Prag) = Name_Contract_Case then
+
+ -- Since contract-cases are listed in reverse order, the first
+ -- contract-case in the list is the last in the source.
+
+ if No (Last_Contract_Case) then
+ Last_Contract_Case := Prag;
+ end if;
+
+ -- For functions, look for presence of 'Result in Ensures
+
+ if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
+ Ignored := Find_Attribute_Result (Arg);
+ end if;
+
+ -- For each individual contract-case, look for presence
+ -- of an expression that could be evaluated differently
+ -- in post-state.
+
+ Post_State_Mentioned := False;
+ Ignored := Find_Post_State (Arg);
+
+ if not Post_State_Mentioned then
+ Error_Msg_N ("?`Ensures` component refers only to pre-state",
+ Prag);
+ end if;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ exit when No (Prag);
+ end loop;
+ end Process_Contract_Cases;
+
-----------------------------
-- Process_Post_Conditions --
-----------------------------
@@ -7075,35 +7134,36 @@
loop
Arg := First (Pragma_Argument_Associations (Prag));
- -- Since pre- and post-conditions are listed in reverse order, the
- -- first postcondition in the list is the last in the source.
+ if Pragma_Name (Prag) = Name_Postcondition then
- if Pragma_Name (Prag) = Name_Postcondition
- and then not Class
- and then No (Last_Postcondition)
- then
- Last_Postcondition := Prag;
- end if;
+ -- Since pre- and post-conditions are listed in reverse order,
+ -- the first postcondition in the list is the last in the
+ -- source.
- -- For functions, look for presence of 'Result in postcondition
+ if not Class
+ and then No (Last_Postcondition)
+ then
+ Last_Postcondition := Prag;
+ end if;
- if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
- Ignored := Find_Attribute_Result (Arg);
- end if;
+ -- For functions, look for presence of 'Result in postcondition
- -- For each individual non-inherited postcondition, look for
- -- presence of an expression that could be evaluated differently
- -- in post-state.
+ if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
+ Ignored := Find_Attribute_Result (Arg);
+ end if;
- if Pragma_Name (Prag) = Name_Postcondition
- and then not Class
- then
- Post_State_Mentioned := False;
- Ignored := Find_Post_State (Arg);
+ -- For each individual non-inherited postcondition, look
+ -- for presence of an expression that could be evaluated
+ -- differently in post-state.
- if not Post_State_Mentioned then
- Error_Msg_N ("?postcondition refers only to pre-state",
- Prag);
+ if not Class then
+ Post_State_Mentioned := False;
+ Ignored := Find_Post_State (Arg);
+
+ if not Post_State_Mentioned then
+ Error_Msg_N ("?postcondition refers only to pre-state",
+ Prag);
+ end if;
end if;
end if;
@@ -7119,6 +7179,8 @@
return;
end if;
+ -- Process spec postconditions
+
if Present (Spec_PPC_List (Contract (Spec_Id))) then
Process_Post_Conditions (Spec_Id, Class => False);
end if;
@@ -7135,15 +7197,34 @@
-- end if;
-- end loop;
+ -- Process contract cases
+
+ if Present (Spec_CTC_List (Contract (Spec_Id))) then
+ Process_Contract_Cases (Spec_Id);
+ end if;
+
-- 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 (Present (Last_Postcondition)
+ or else Present (Last_Contract_Case))
and then not Attribute_Result_Mentioned
then
- Error_Msg_N ("?function postcondition does not mention result",
- Last_Postcondition);
+ if Present (Last_Postcondition) then
+ if Present (Last_Contract_Case) then
+ Error_Msg_N ("?neither function postcondition nor " &
+ "contract cases do mention result",
+ Last_Postcondition);
+
+ else
+ Error_Msg_N ("?function postcondition does not mention result",
+ Last_Postcondition);
+ end if;
+ else
+ Error_Msg_N ("?contract cases do not mention result",
+ Last_Contract_Case);
+ end if;
end if;
end Check_Subprogram_Contract;
The warning option -gnatw.t already issued warnings on suspicious postconditions. This extends it to contract cases, which is a GNAT pragma/aspect allowing to express fine-grain contracts. GNAT now detects these cases on the following code: $ gcc -c -gnatc -gnatw.t -gnat12 p.ads 1. package P is 2. function A_Is_Positive (X : Integer) return Boolean with 3. Contract_Case => (Name => "normal case", | >>> warning: "Ensures" component refers only to pre-state >>> warning: contract cases do not mention result 4. Mode => Nominal, 5. Ensures => X >= 0); 6. procedure A_Incr (X : in Integer; Y : out Integer) with 7. Contract_Case => (Name => "normal case", | >>> warning: "Ensures" component refers only to pre-state 8. Mode => Nominal, 9. Ensures => X = X + 1); 10. end P; Tested on x86_64-pc-linux-gnu, committed on trunk 2012-03-15 Yannick Moy <moy@adacore.com> * gnat_ugn.texi Document the extension of option -gnatw.t. * sem_ch3.adb (Analyze_Declaration): Check for suspicious contracts only after contract cases have been semantically analyzed. * sem_ch6.adb (Check_Subprogram_Contract): Consider also Ensures components of contract cases for detecting suspicious contracts.