From e6ae24fa4f4d7564a42981e3415e3450915a3866 Mon Sep 17 00:00:00 2001 From: charlet Date: Mon, 19 Mar 2012 16:31:20 +0000 Subject: [PATCH] 2012-03-19 Yannick Moy * sem_ch6.adb (Check_Subprogram_Contract): Do not emit warnings on trivially True or False postconditions and Ensures components of contract-cases. 2012-03-19 Robert Dewar * gnat_ugn.texi: Fix index entry for -gnatei (now we have ug_words entry). git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@185527 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/ChangeLog | 11 ++++++++++ gcc/ada/gnat_ugn.texi | 4 ++-- gcc/ada/sem_ch6.adb | 57 ++++++++++++++++++++++++++++++++++++++------------- gcc/ada/ug_words | 1 + 4 files changed, 57 insertions(+), 16 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 5966f5e..28c47b8 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,14 @@ +2012-03-19 Yannick Moy + + * sem_ch6.adb (Check_Subprogram_Contract): Do not emit warnings + on trivially True or False postconditions and Ensures components + of contract-cases. + +2012-03-19 Robert Dewar + + * gnat_ugn.texi: Fix index entry for -gnatei (now we have + ug_words entry). + 2012-03-19 Hristian Kirtchev * sem_ch3.adb (Get_Discriminant_Value): Instead of looking diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi index 9022276..5c313ac 100644 --- a/gcc/ada/gnat_ugn.texi +++ b/gcc/ada/gnat_ugn.texi @@ -4155,13 +4155,13 @@ Display full source path name in brief error messages. @cindex @option{-gnateG} (@command{gcc}) Save result of preprocessing in a text file. -@item ^-gnatei^/MAX_INSTANTIATIONS=^@var{nnn} +@item -gnatei@var{nnn} @cindex @option{-gnatei} (@command{gcc}) Set maximum number of instantiations during compilation of a single unit to @var{nnn}. This may be useful in increasing the default maximum of 8000 for the rare case when a single unit legitimately exceeds this limit. -@item ^-gnateI^/MULTI_UNIT_INDEX=^@var{nnn} +@item -gnateI@var{nnn} @cindex @option{-gnateI} (@command{gcc}) Indicates that the source is a multi-unit source and that the index of the unit to compile is @var{nnn}. @var{nnn} needs to be a positive number and need diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index a2d729c..5464d41 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -6927,23 +6927,29 @@ package body Sem_Ch6 is -- Inherited_Subprograms (Spec_Id); -- -- List of subprograms inherited by this subprogram + -- We ignore postconditions "True" or "False" and contract-cases which + -- have similar Ensures components, which we call "trivial", when + -- issuing warnings, since these postconditions and contract-cases + -- purposedly ignore the post-state. + Last_Postcondition : Node_Id := Empty; - -- Last postcondition on the subprogram, or else Empty if either no - -- postcondition or only inherited postconditions. + -- Last non-trivial postcondition on the subprogram, or else Empty if + -- either no non-trivial postcondition or only inherited postconditions. Last_Contract_Case : Node_Id := Empty; - -- Last contract-case on the subprogram, or else Empty + -- Last non-trivial contract-case on the subprogram, or else Empty Attribute_Result_Mentioned : Boolean := False; - -- Whether attribute 'Result is mentioned in a postcondition + -- Whether attribute 'Result is mentioned in a non-trivial postcondition + -- or contract-case. No_Warning_On_Some_Postcondition : Boolean := False; - -- Whether there exists a postcondition or a contract-case without a - -- corresponding warning. + -- Whether there exists a non-trivial postcondition or contract-case + -- without a corresponding warning. 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. + -- Whether some expression mentioned in a postcondition or contract-case + -- 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 if N is a reference to the attribute 'Result, and if so set @@ -6956,6 +6962,9 @@ 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. + function Is_Trivial_Post_Or_Ensures (N : Node_Id) return Boolean; + -- Return whether node N is trivially "True" or "False" + 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 @@ -7046,13 +7055,26 @@ package body Sem_Ch6 is end if; end Check_Post_State; + -------------------------------- + -- Is_Trivial_Post_Or_Ensures -- + -------------------------------- + + function Is_Trivial_Post_Or_Ensures (N : Node_Id) return Boolean is + begin + return Is_Entity_Name (N) + and then (Entity (N) = Standard_True + or else + Entity (N) = Standard_False); + end Is_Trivial_Post_Or_Ensures; + ---------------------------- -- Process_Contract_Cases -- ---------------------------- procedure Process_Contract_Cases (Spec : Node_Id) is - Prag : Node_Id; - Arg : Node_Id; + Prag : Node_Id; + Arg : Node_Id; + Ignored : Traverse_Final_Result; pragma Unreferenced (Ignored); @@ -7063,8 +7085,12 @@ package body Sem_Ch6 is Arg := Get_Ensures_From_CTC_Pragma (Prag); - if Pragma_Name (Prag) = Name_Contract_Case then + -- Ignore trivial contract-case when Ensures component is "True" + -- or "False". + if Pragma_Name (Prag) = Name_Contract_Case + and then not Is_Trivial_Post_Or_Ensures (Expression (Arg)) + then -- Since contract-cases are listed in reverse order, the first -- contract-case in the list is the last in the source. @@ -7088,8 +7114,8 @@ package body Sem_Ch6 is if Post_State_Mentioned then No_Warning_On_Some_Postcondition := True; else - Error_Msg_N ("?`Ensures` component refers only to pre-state", - Prag); + Error_Msg_N + ("?`Ensures` component refers only to pre-state", Prag); end if; end if; @@ -7116,8 +7142,11 @@ package body Sem_Ch6 is loop Arg := First (Pragma_Argument_Associations (Prag)); - if Pragma_Name (Prag) = Name_Postcondition then + -- Ignore trivial postcondition of "True" or "False" + if Pragma_Name (Prag) = Name_Postcondition + and then not Is_Trivial_Post_Or_Ensures (Expression (Arg)) + then -- Since pre- and post-conditions are listed in reverse order, -- the first postcondition in the list is last in the source. diff --git a/gcc/ada/ug_words b/gcc/ada/ug_words index d92b89c..9901b84 100644 --- a/gcc/ada/ug_words +++ b/gcc/ada/ug_words @@ -63,6 +63,7 @@ gcc -c ^ GNAT COMPILE -gnateD ^ /SYMBOL_PREPROCESSING -gnatef ^ /FULL_PATH_IN_BRIEF_MESSAGES -gnateG ^ /GENERATE_PROCESSED_SOURCE +-gnatei ^ /MAX_INSTANTIATIONS= -gnateI ^ /MULTI_UNIT_INDEX= -gnatem ^ /MAPPING_FILE -gnatep ^ /DATA_PREPROCESSING -- 2.7.4