+2013-04-22 Yannick Moy <moy@adacore.com>
+
+ * aspects.ads, aspects.adb, sem_ch13.adb: Removal of references to
+ Contract_Case.
+ * gnat_ugn.texi, gnat_rm.texi Description of Contract_Case replaced by
+ description of Contract_Cases.
+
2013-04-12 Robert Dewar <dewar@adacore.com>
* makeutl.adb, prj-nmsc.adb: Minor reformatting.
Aspect_Compiler_Unit => Aspect_Compiler_Unit,
Aspect_Component_Size => Aspect_Component_Size,
Aspect_Constant_Indexing => Aspect_Constant_Indexing,
- Aspect_Contract_Case => Aspect_Contract_Case,
Aspect_Contract_Cases => Aspect_Contract_Cases,
Aspect_Convention => Aspect_Convention,
Aspect_CPU => Aspect_CPU,
Aspect_Bit_Order,
Aspect_Component_Size,
Aspect_Constant_Indexing,
- Aspect_Contract_Case, -- GNAT
Aspect_Contract_Cases, -- GNAT
Aspect_Convention,
Aspect_CPU,
Aspect_Ada_2005 => True,
Aspect_Ada_2012 => True,
Aspect_Compiler_Unit => True,
- Aspect_Contract_Case => True,
Aspect_Contract_Cases => True,
Aspect_Depends => True,
Aspect_Dimension => True,
-- the same aspect attached to the same declaration are allowed.
No_Duplicates_Allowed : constant array (Aspect_Id) of Boolean :=
- (Aspect_Contract_Case => False,
- Aspect_Test_Case => False,
+ (Aspect_Test_Case => False,
others => True);
-- The following array indicates type aspects that are inherited and apply
Aspect_Bit_Order => Expression,
Aspect_Component_Size => Expression,
Aspect_Constant_Indexing => Name,
- Aspect_Contract_Case => Expression,
Aspect_Contract_Cases => Expression,
Aspect_Convention => Name,
Aspect_CPU => Expression,
Aspect_Compiler_Unit => Name_Compiler_Unit,
Aspect_Component_Size => Name_Component_Size,
Aspect_Constant_Indexing => Name_Constant_Indexing,
- Aspect_Contract_Case => Name_Contract_Case,
Aspect_Contract_Cases => Name_Contract_Cases,
Aspect_Convention => Name_Convention,
Aspect_CPU => Name_CPU,
* Pragma Complete_Representation::
* Pragma Complex_Representation::
* Pragma Component_Alignment::
-* Pragma Contract_Case::
+* Pragma Contract_Cases::
* Pragma Convention_Identifier::
* Pragma CPP_Class::
* Pragma CPP_Constructor::
* Pragma Complete_Representation::
* Pragma Complex_Representation::
* Pragma Component_Alignment::
-* Pragma Contract_Case::
+* Pragma Contract_Cases::
* Pragma Convention_Identifier::
* Pragma CPP_Class::
* Pragma CPP_Constructor::
pragma @code{Pack}, pragma @code{Component_Alignment}, or a record rep
clause), the GNAT uses the default alignment as described previously.
-@node Pragma Contract_Case
-@unnumberedsec Pragma Contract_Case
+@node Pragma Contract_Cases
+@unnumberedsec Pragma Contract_Cases
@cindex Contract cases
-@findex Contract_Case
+@findex Contract_Cases
@noindent
Syntax:
@smallexample @c ada
-pragma Contract_Case (
- [Name =>] static_string_Expression
- ,[Mode =>] (Nominal | Robustness)
- [, Requires => Boolean_Expression]
- [, Ensures => Boolean_Expression]);
+pragma Contract_Cases (
+ Condition => Consequence
+ @{,Condition => Consequence@});
@end smallexample
@noindent
-The @code{Contract_Case} pragma allows defining fine-grain specifications
+The @code{Contract_Cases} pragma allows defining fine-grain specifications
that can complement or replace the contract given by a precondition and a
-postcondition. Additionally, the @code{Contract_Case} pragma can be used
+postcondition. Additionally, the @code{Contract_Cases} pragma can be used
by testing and formal verification tools. The compiler checks its validity and,
depending on the assertion policy at the point of declaration of the pragma,
it may insert a check in the executable. For code generation, the contract
-case
-
-@smallexample @c ada
-pragma Contract_Case (
- Name => ...
- Mode => ...
- Requires => R,
- Ensures => E);
-@end smallexample
-
-@noindent
-is equivalent to
+cases
@smallexample @c ada
-pragma Postcondition (not R'Old or else E);
+pragma Contract_Cases (
+ Cond1 => Pred1,
+ Cond2 => Pred2);
@end smallexample
@noindent
-which is also equivalent to (in Ada 2012)
+are equivalent to
@smallexample @c ada
-pragma Postcondition (if R'Old then E);
+C1 : constant Boolean := Cond1; -- evaluated at subprogram entry
+C2 : constant Boolean := Cond2; -- evaluated at subprogram entry
+pragma Precondition ((C1 and not C2) or (C2 and not C1));
+pragma Postcondition (if C1 then Pred1);
+pragma Postcondition (if C2 then Pred2);
@end smallexample
@noindent
-expressing that, whenever condition @code{R} is satisfied on entry to the
-subprogram, condition @code{E} should be fulfilled on exit to the subprogram.
+The precondition expresses that one and only one of the conditions is
+satisfied on entry to the subprogram.
+The postcondition expresses that, whenever condition @code{Ci} is satisfied
+on entry to the subprogram, consequence @code{Predi} should be fulfilled on
+exit to the subprogram.
A precondition @code{P} and postcondition @code{Q} can also be
expressed as contract cases:
@smallexample @c ada
-pragma Contract_Case (
- Name => "Replace precondition",
- Mode => Nominal,
- Requires => not P,
- Ensures => False);
-pragma Contract_Case (
- Name => "Replace postcondition",
- Mode => Nominal,
- Requires => P,
- Ensures => Q);
+pragma Contract_Cases (P => Q);
@end smallexample
-@code{Contract_Case} pragmas may only appear immediately following the
-(separate) declaration of a subprogram in a package declaration, inside
-a package spec unit. Only other pragmas may intervene (that is appear
-between the subprogram declaration and a contract case).
+The placement and visibility rules for @code{Contract_Cases} pragmas are
+identical to those described for preconditions and postconditions.
-The compiler checks that boolean expressions given in @code{Requires} and
-@code{Ensures} are valid, where the rules for @code{Requires} are the
-same as the rule for an expression in @code{Precondition} and the rules
-for @code{Ensures} are the same as the rule for an expression in
+The compiler checks that boolean expressions given in conditions and
+consequences are valid, where the rules for conditions are the same as
+the rule for an expression in @code{Precondition} and the rules for
+consequences are the same as the rule for an expression in
@code{Postcondition}. In particular, attributes @code{'Old} and
-@code{'Result} can only be used within the @code{Ensures}
-expression. The following is an example of use within a package spec:
+@code{'Result} can only be used within consequence expressions.
+The condition for the last contract case may be @code{others}, to denote
+any case not captured by the previous cases. The
+following is an example of use within a package spec:
@smallexample @c ada
package Math_Functions is
...
function Sqrt (Arg : Float) return Float;
- pragma Contract_Case (Name => "Small argument",
- Mode => Nominal,
- Requires => Arg < 100,
- Ensures => Sqrt'Result < 10);
+ pragma Contract_Cases ((Arg in 0 .. 99) => Sqrt'Result < 10,
+ Arg >= 100 => Sqrt'Result >= 10,
+ others => Sqrt'Result = 0);
...
end Math_Functions;
@end smallexample
@noindent
-The meaning of a contract case is that, whenever the associated subprogram is
-executed in a context where @code{Requires} holds, then @code{Ensures}
-should hold when the subprogram returns. Mode @code{Nominal} indicates
-that the input context should also satisfy the precondition of the
-subprogram, and the output context should also satisfy its
-postcondition. More @code{Robustness} indicates that the precondition and
-postcondition of the subprogram should be ignored for this contract case,
-which is mostly useful when testing such a contract using a testing tool
-that understands contract cases.
+The meaning of contract cases is that only one case should apply at each
+call, as determined by the corresponding condition evaluating to True,
+and that the consequence for this case should hold when the subprogram
+returns.
@node Pragma Convention_Identifier
@unnumberedsec Pragma Convention_Identifier
@noindent
The @code{Test_Case} pragma allows defining fine-grain specifications
-for use by testing tools. Its syntax is similar to the syntax of the
-@code{Contract_Case} pragma, which is used for both testing and
-formal verification.
+for use by testing tools.
The compiler checks the validity of the @code{Test_Case} pragma, but its
presence does not lead to any modification of the code generated by the
-compiler, contrary to the treatment of the @code{Contract_Case} pragma.
+compiler.
@code{Test_Case} pragmas may only appear immediately following the
(separate) declaration of a subprogram in a package declaration, inside
@item @code{Atomic_Components} @tab
@item @code{Bit_Order} @tab
@item @code{Component_Size} @tab
-@item @code{Contract_Case} @tab -- GNAT
+@item @code{Contract_Cases} @tab -- GNAT
@item @code{Discard_Names} @tab
@item @code{External_Tag} @tab
@item @code{Favor_Top_Level} @tab -- GNAT
@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)
-and suspicious contract cases (pragma @code{Contract_Case}). A
+and suspicious contract cases (pragma @code{Contract_Cases}). 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
-- analyzed right now.
-- Note that there is a special handling for Pre, Post, Test_Case,
- -- Contract_Case aspects. In these cases, we do not have to worry
+ -- Contract_Cases aspects. In these cases, we do not have to worry
-- about delay issues, since the pragmas themselves deal with delay
-- of visibility for the expression analysis. Thus, we just insert
-- the pragma after the node N.
-- Case 4: Special handling for aspects
- -- Pre/Post/Test_Case/Contract_Case whose corresponding pragmas
- -- take care of the delay.
+ -- Pre/Post/Test_Case/Contract_Cases whose corresponding
+ -- pragmas take care of the delay.
-- Aspects Pre/Post generate Precondition/Postcondition pragmas
-- with a first argument that is the expression, and a second
goto Continue;
end;
- when Aspect_Contract_Case |
- Aspect_Test_Case =>
+ when Aspect_Test_Case => Test_Case : declare
+ Args : List_Id;
+ Comp_Expr : Node_Id;
+ Comp_Assn : Node_Id;
+ New_Expr : Node_Id;
- declare
- Args : List_Id;
- Comp_Expr : Node_Id;
- Comp_Assn : Node_Id;
- New_Expr : Node_Id;
+ begin
+ Args := New_List;
- begin
- Args := New_List;
+ if Nkind (Parent (N)) = N_Compilation_Unit then
+ Error_Msg_Name_1 := Nam;
+ Error_Msg_N ("incorrect placement of aspect `%`", E);
+ goto Continue;
+ end if;
- if Nkind (Parent (N)) = N_Compilation_Unit then
- Error_Msg_Name_1 := Nam;
- Error_Msg_N ("incorrect placement of aspect `%`", E);
- goto Continue;
- end if;
+ if Nkind (Expr) /= N_Aggregate then
+ Error_Msg_Name_1 := Nam;
+ Error_Msg_NE
+ ("wrong syntax for aspect `%` for &", Id, E);
+ goto Continue;
+ end if;
- if Nkind (Expr) /= N_Aggregate then
+ -- Make pragma expressions refer to the original aspect
+ -- expressions through the Original_Node link. This is
+ -- used in semantic analysis for ASIS mode, so that the
+ -- original expression also gets analyzed.
+
+ Comp_Expr := First (Expressions (Expr));
+ while Present (Comp_Expr) loop
+ New_Expr := Relocate_Node (Comp_Expr);
+ Set_Original_Node (New_Expr, Comp_Expr);
+ Append_To (Args,
+ Make_Pragma_Argument_Association (Sloc (Comp_Expr),
+ Expression => New_Expr));
+ Next (Comp_Expr);
+ end loop;
+
+ Comp_Assn := First (Component_Associations (Expr));
+ while Present (Comp_Assn) loop
+ if List_Length (Choices (Comp_Assn)) /= 1
+ or else
+ Nkind (First (Choices (Comp_Assn))) /= N_Identifier
+ then
Error_Msg_Name_1 := Nam;
Error_Msg_NE
("wrong syntax for aspect `%` for &", Id, E);
goto Continue;
end if;
- -- Make pragma expressions refer to the original aspect
- -- expressions through the Original_Node link. This is
- -- used in semantic analysis for ASIS mode, so that the
- -- original expression also gets analyzed.
-
- Comp_Expr := First (Expressions (Expr));
- while Present (Comp_Expr) loop
- New_Expr := Relocate_Node (Comp_Expr);
- Set_Original_Node (New_Expr, Comp_Expr);
- Append_To (Args,
- Make_Pragma_Argument_Association (Sloc (Comp_Expr),
- Expression => New_Expr));
- Next (Comp_Expr);
- end loop;
-
- Comp_Assn := First (Component_Associations (Expr));
- while Present (Comp_Assn) loop
- if List_Length (Choices (Comp_Assn)) /= 1
- or else
- Nkind (First (Choices (Comp_Assn))) /= N_Identifier
- then
- Error_Msg_Name_1 := Nam;
- Error_Msg_NE
- ("wrong syntax for aspect `%` for &", Id, E);
- goto Continue;
- end if;
-
- New_Expr := Relocate_Node (Expression (Comp_Assn));
- Set_Original_Node (New_Expr, Expression (Comp_Assn));
- Append_To (Args,
- Make_Pragma_Argument_Association (Sloc (Comp_Assn),
- Chars => Chars (First (Choices (Comp_Assn))),
- Expression => New_Expr));
- Next (Comp_Assn);
- end loop;
+ New_Expr := Relocate_Node (Expression (Comp_Assn));
+ Set_Original_Node (New_Expr, Expression (Comp_Assn));
+ Append_To (Args,
+ Make_Pragma_Argument_Association (Sloc (Comp_Assn),
+ Chars => Chars (First (Choices (Comp_Assn))),
+ Expression => New_Expr));
+ Next (Comp_Assn);
+ end loop;
- -- Build the contract-case or test-case pragma
+ -- Build the test-case pragma
- Aitem :=
- Make_Pragma (Loc,
- Pragma_Identifier =>
- Make_Identifier (Sloc (Id), Nam),
- Pragma_Argument_Associations => Args);
+ Aitem :=
+ Make_Pragma (Loc,
+ Pragma_Identifier =>
+ Make_Identifier (Sloc (Id), Nam),
+ Pragma_Argument_Associations => Args);
- Delay_Required := False;
- end;
+ Delay_Required := False;
+ end Test_Case;
when Aspect_Contract_Cases => Contract_Cases : declare
Case_Guard : Node_Id;
-- Here is the list of aspects that don't require delay analysis
when Aspect_Abstract_State |
- Aspect_Contract_Case |
Aspect_Contract_Cases |
Aspect_Dimension |
Aspect_Dimension_System |
begin
GNAT_Pragma;
- S14_Pragma;
Check_Arg_Count (1);
-- Completely ignore if not enabled
projects / thirdparty / gcc.git / commitdiff
