From 22f46473c7f98a4f414db8728ba64a60a6e23a16 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 15 Mar 2012 10:05:07 +0100 Subject: [PATCH] [multiple changes] 2012-03-15 Hristian Kirtchev * exp_util.adb (Initialized_By_Ctrl_Function): Do not loop over selector names as the function call always appears at the top selected component. 2012-03-15 Ed Schonberg * sem_ch12.adb (Validate_Access_Subprogram_Instance): keep Mode_Conformance check for older versions of the language. 2012-03-15 Yannick Moy * 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. From-SVN: r185417 --- gcc/ada/ChangeLog | 20 +++++++ gcc/ada/exp_util.adb | 13 ++-- gcc/ada/gnat_ugn.texi | 8 ++- gcc/ada/sem_ch12.adb | 28 ++++++--- gcc/ada/sem_ch3.adb | 9 ++- gcc/ada/sem_ch6.adb | 135 +++++++++++++++++++++++++++++++++--------- 6 files changed, 165 insertions(+), 48 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f5b141e1864..e8d4a5b2ad1 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,23 @@ +2012-03-15 Hristian Kirtchev + + * exp_util.adb (Initialized_By_Ctrl_Function): Do not loop over + selector names as the function call always appears at the top selected + component. + +2012-03-15 Ed Schonberg + + * sem_ch12.adb (Validate_Access_Subprogram_Instance): keep + Mode_Conformance check for older versions of the language. + +2012-03-15 Yannick Moy + + * 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. + 2012-03-15 Yannick Moy * aspects.adb, aspects.ads (Aspect_Id): New GNAT aspect diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 8ccf21634ec..ae7f2b95467 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -3967,16 +3967,11 @@ package body Exp_Util is Expr := Name (Expr); end if; - -- The function call may appear in object.operation format. Strip - -- all prefixes and retrieve the function name. + -- The function call may appear in object.operation format - loop - if Nkind (Expr) = N_Selected_Component then - Expr := Selector_Name (Expr); - else - exit; - end if; - end loop; + if Nkind (Expr) = N_Selected_Component then + Expr := Selector_Name (Expr); + end if; return Nkind_In (Expr, N_Expanded_Name, N_Identifier) diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi index 08e064966ce..365a4478a1d 100644 --- a/gcc/ada/gnat_ugn.texi +++ b/gcc/ada/gnat_ugn.texi @@ -5696,9 +5696,11 @@ This switch suppresses warnings for tracking of deleted conditional code. @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}. diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index b411b3bd64c..5ab842d3673 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -10433,17 +10433,29 @@ package body Sem_Ch12 is 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 diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 9d6688490a4..71b1fb44f3f 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2196,19 +2196,26 @@ package body Sem_Ch3 is 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); diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 6adcaa37665..13fc5aba172 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -6953,6 +6953,9 @@ package body Sem_Ch6 is -- 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 @@ package body Sem_Ch6 is -- 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 @@ package body Sem_Ch6 is 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 @@ package body Sem_Ch6 is 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 @@ package body Sem_Ch6 is 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 @@ package body Sem_Ch6 is -- 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; -- 2.30.2