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.
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
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;
-- 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);