Abandon_Instantiation (Actual);
end if;
- -- In accordance with AI05-288 (which is an Ada 2012 AI that is a
- -- binding intepretation to be applied to previous versions of Ada
- -- as well as Ada 2012), actuals for access_to_subprograms must be
+ -- According to AI05-288, actuals for access_to_subprograms must be
-- subtype conformant with the generic formal. Previous to AI05-288
-- only mode conformance was required.
- Check_Subtype_Conformant
- (Designated_Type (Act_T),
- Designated_Type (A_Gen_T),
- Actual,
- Get_Inst => True);
+ -- This is a binding interpretation that applies to previous versions
+ -- of the language, but for now we retain the milder check in order
+ -- to preserve ACATS tests.
+ -- These will be protested eventually ???
+
+ if Ada_Version < Ada_2012 then
+ Check_Mode_Conformant
+ (Designated_Type (Act_T),
+ Designated_Type (A_Gen_T),
+ Actual,
+ Get_Inst => True);
+
+ else
+ Check_Subtype_Conformant
+ (Designated_Type (Act_T),
+ Designated_Type (A_Gen_T),
+ Actual,
+ Get_Inst => True);
+ end if;
if Ekind (Base_Type (Act_T)) = E_Access_Protected_Subprogram_Type then
if Ekind (A_Gen_T) = E_Access_Subprogram_Type then
-- 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
-- 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.
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 --
-----------------------------
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;
return;
end if;
+ -- Process spec postconditions
+
if Present (Spec_PPC_List (Contract (Spec_Id))) then
Process_Post_Conditions (Spec_Id, Class => False);
end if;
-- 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;
projects / gcc.git / commitdiff