[multiple changes]

2014-02-19  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Check_Refined_Global_Item):
	A state or variable acts as a constituent only it is part of an
	encapsulating state and the state has visible refinement.

2014-02-19  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Contract): Do not warn on a
	postcondition for a function when the expression does not mention
	'Result but the function has in-out parameters.

2014-02-19  Robert Dewar  <dewar@adacore.com>

	* gnat_rm.texi: Add documentation on Value_Size forcing biased
	representation.

From-SVN: r207886

gcc/ada/ChangeLog

 2014-02-19  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* sem_prag.adb (Check_Refined_Global_Item):
+	A state or variable acts as a constituent only it is part of an
+	encapsulating state and the state has visible refinement.
+
+2014-02-19  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch6.adb (Analyze_Subprogram_Contract): Do not warn on a
+	postcondition for a function when the expression does not mention
+	'Result but the function has in-out parameters.
+
+2014-02-19  Robert Dewar  <dewar@adacore.com>
+
+	* gnat_rm.texi: Add documentation on Value_Size forcing biased
+	representation.
+
+2014-02-19  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* lib-xref.ads Remove the small table of letter and symbol usage as we
 	already have one.
 

gcc/ada/gnat_rm.texi

@@ -14262,6 +14262,34 @@ For all other types, the @code{Object_Size}
 and Value_Size are the same (and equivalent to the RM attribute @code{Size}).
 Only @code{Size} may be specified for such types.
 
+Note that @code{Value_Size} can be used to force biased representation
+for a particular subtype. Consider this example:
+
+@smallexample
+   type R is (A, B, C, D, E, F);
+   subtype RAB is R range A .. B;
+   subtype REF is R range E .. F;
+@end smallexample
+
+@noindent
+By default, @code{RAB}
+has a size of 1 (sufficient to accomodate the representation
+of @code{A} and @code{B}, 0 and 1), and @code{REF}
+has a size of 3 (sufficient to accomodate the representation
+of @code{E} and @code{F}, 4 and 5). But if we add the
+following @code{Value_Size} attribute definition clause:
+
+@smallexample
+   for REF'Value_Size use 1;
+@end smallexample
+
+@noindent
+then biased representation is forced for @code{REF},
+and 0 will represent @code{E} and 1 will represent @code{F}.
+A warning is issued when a @code{Value_Size} attribute
+definition clause forces biased representation. This
+warning can be turned off using @code{-gnatw.B}.
+
 @node Component_Size Clauses
 @section Component_Size Clauses
 @cindex Component_Size Clause

gcc/ada/sem_ch6.adb

@@ -3663,7 +3663,25 @@ package body Sem_Ch6 is
             Error_Msg_N
               ("contract cases do not mention result?T?", Case_Prag);
 
+         --  OK if we have at least one IN OUT parameter
+
          elsif Present (Post_Prag) and then not Seen_In_Post then
+            declare
+               F : Entity_Id;
+            begin
+               F := First_Formal (Subp);
+               while Present (F) loop
+                  if Ekind (F) = E_In_Out_Parameter then
+                     return;
+                  else
+                     Next_Formal (F);
+                  end if;
+               end loop;
+            end;
+
+            --  If no in-out parameters and no mention of Result, the contract
+            --  is certainly suspicious.
+
             Error_Msg_N
               ("function postcondition does not mention result?T?", Post_Prag);
          end if;

gcc/ada/sem_prag.adb

@@ -22610,10 +22610,13 @@ package body Sem_Prag is
          --  Start of processing for Check_Refined_Global_Item
 
          begin
-            --  The state or variable acts as a constituent of a state, collect
-            --  it for the state completeness checks performed later on.
+            --  When the state or variable acts as a constituent of another
+            --  state with a visible refinement, collect it for the state
+            --  completeness checks performed later on.
 
-            if Present (Encapsulating_State (Item_Id)) then
+            if Present (Encapsulating_State (Item_Id))
+             and then Has_Visible_Refinement (Encapsulating_State (Item_Id))
+            then
                if Global_Mode = Name_Input then
                   Add_Item (Item_Id, In_Constits);