[multiple changes]

2012-03-19  Yannick Moy  <moy@adacore.com>

	* 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  <dewar@adacore.com>

	* gnat_ugn.texi: Fix index entry for -gnatei (now we have
	ug_words entry).

From-SVN: r185527

gcc/ada/ChangeLog

+2012-03-19  Yannick Moy  <moy@adacore.com>
+
+	* 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  <dewar@adacore.com>
+
+	* gnat_ugn.texi: Fix index entry for -gnatei (now we have
+	ug_words entry).
+
 2012-03-19  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* sem_ch3.adb (Get_Discriminant_Value): Instead of looking

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

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.
 

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