git
/
gcc
mirror of git://gcc.gnu.org/git/gcc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

aspects.adb, [...] (Aspect_Id): New GNAT aspect Aspect_Contract_Case. 

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

	* aspects.adb, aspects.ads (Aspect_Id): New GNAT aspect
	Aspect_Contract_Case.
	* gnat_rm.texi Document the new pragma/aspect
	Contract_Case. Correct the documentation of the existing
	pragma/aspect Test_Case with the new semantics.
	* sem_attr.adb (Analyze_Attribute): Allow use of 'Result in the
	Ensures component of a Contract_Case pragma.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Check new aspect
	and translate it into a pragma.
	(Check_Aspect_At_Freeze_Point): Take into account the new aspect.
	* sem_ch3.adb, sinfo.adb, sinfo.ads Renaming of TC (for test case)
	into CTC (for contract and test case).
	* sem_ch6.adb (Process_PPCs): Generate Check pragmas from
	Contract_Case pragmas, similarly to what is done already for
	postconditions.
	* sem_prag.adb, sem_prag.ads (Check_Contract_Or_Test_Case):
	Renaming of Check_Test_Case.
	(Analyze_Pragma, Sig_Flags): Take into account the new pragma.
	* sem_util.adb, sem_util.ads Renaming to take into account the
	new pragma, so that functions which applied only to Test_Case
	now apply to both Test_Case and Contract_Case.
	* par-prag.adb, sem_warn.adb, snames.ads-tmpl Take into account
	the new pragma.

From-SVN: r185415
This commit is contained in:
Yannick Moy 2012-03-15 08:48:36 +00:00 committed by Arnaud Charlet
parent 51a1aacf86
commit 90e8523311
17 changed files with 498 additions and 198 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
gcc/ada/ChangeLog
View File

@ -1,3 +1,29 @@
2012-03-15 Yannick Moy <moy@adacore.com>
* aspects.adb, aspects.ads (Aspect_Id): New GNAT aspect
Aspect_Contract_Case.
* gnat_rm.texi Document the new pragma/aspect
Contract_Case. Correct the documentation of the existing
pragma/aspect Test_Case with the new semantics.
* sem_attr.adb (Analyze_Attribute): Allow use of 'Result in the
Ensures component of a Contract_Case pragma.
* sem_ch13.adb (Analyze_Aspect_Specifications): Check new aspect
and translate it into a pragma.
(Check_Aspect_At_Freeze_Point): Take into account the new aspect.
* sem_ch3.adb, sinfo.adb, sinfo.ads Renaming of TC (for test case)
into CTC (for contract and test case).
* sem_ch6.adb (Process_PPCs): Generate Check pragmas from
Contract_Case pragmas, similarly to what is done already for
postconditions.
* sem_prag.adb, sem_prag.ads (Check_Contract_Or_Test_Case):
Renaming of Check_Test_Case.
(Analyze_Pragma, Sig_Flags): Take into account the new pragma.
* sem_util.adb, sem_util.ads Renaming to take into account the
new pragma, so that functions which applied only to Test_Case
now apply to both Test_Case and Contract_Case.
* par-prag.adb, sem_warn.adb, snames.ads-tmpl Take into account
the new pragma.
2012-03-15 Robert Dewar <dewar@adacore.com>
* sem_ch6.ads: Minor comment updates.

1
gcc/ada/aspects.adb
View File

@ -249,6 +249,7 @@ package body Aspects is
Aspect_Bit_Order => Aspect_Bit_Order,
Aspect_Component_Size => Aspect_Component_Size,
Aspect_Constant_Indexing => Aspect_Constant_Indexing,
Aspect_Contract_Case => Aspect_Contract_Case,
Aspect_CPU => Aspect_CPU,
Aspect_Default_Component_Value => Aspect_Default_Component_Value,
Aspect_Default_Iterator => Aspect_Default_Iterator,

9
gcc/ada/aspects.ads
View File

@ -50,6 +50,7 @@ package Aspects is
Aspect_Bit_Order,
Aspect_Component_Size,
Aspect_Constant_Indexing,
Aspect_Contract_Case, -- GNAT
Aspect_CPU,
Aspect_Default_Component_Value,
Aspect_Default_Iterator,
@ -176,6 +177,7 @@ package Aspects is
(Aspect_Ada_2005 => True,
Aspect_Ada_2012 => True,
Aspect_Compiler_Unit => True,
Aspect_Contract_Case => True,
Aspect_Dimension => True,
Aspect_Dimension_System => True,
Aspect_Favor_Top_Level => True,
@ -206,8 +208,9 @@ package Aspects is
-- the same aspect attached to the same declaration are allowed.
No_Duplicates_Allowed : constant array (Aspect_Id) of Boolean :=
(Aspect_Test_Case => False,
others => True);
(Aspect_Contract_Case => False,
Aspect_Test_Case => False,
others => True);
-- The following array indicates type aspects that are inherited and apply
-- to the class-wide type as well.
@ -259,6 +262,7 @@ package Aspects is
Aspect_Bit_Order => Expression,
Aspect_Component_Size => Expression,
Aspect_Constant_Indexing => Name,
Aspect_Contract_Case => Expression,
Aspect_CPU => Expression,
Aspect_Default_Component_Value => Expression,
Aspect_Default_Iterator => Name,
@ -325,6 +329,7 @@ package Aspects is
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_CPU => Name_CPU,
Aspect_Default_Iterator => Name_Default_Iterator,
Aspect_Default_Value => Name_Default_Value,

128
gcc/ada/gnat_rm.texi
View File

@ -120,6 +120,7 @@ Implementation Defined Pragmas
* Pragma Complete_Representation::
* Pragma Complex_Representation::
* Pragma Component_Alignment::
* Pragma Contract_Case::
* Pragma Convention_Identifier::
* Pragma CPP_Class::
* Pragma CPP_Constructor::
@ -855,6 +856,7 @@ consideration, the use of these pragmas should be minimized.
* Pragma Complete_Representation::
* Pragma Complex_Representation::
* Pragma Component_Alignment::
* Pragma Contract_Case::
* Pragma Convention_Identifier::
* Pragma CPP_Class::
* Pragma CPP_Constructor::
@ -1704,6 +1706,108 @@ If the alignment for a record or array type is not specified (using
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
@cindex Contract cases
@findex Contract_Case
@noindent
Syntax:
@smallexample @c ada
pragma Contract_Case (
[Name =>] static_string_Expression
,[Mode =>] (Nominal | Robustness)
[, Requires => Boolean_Expression]
[, Ensures => Boolean_Expression]);
@end smallexample
@noindent
The @code{Contract_Case} 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
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
@smallexample @c ada
pragma Postcondition (not R'Old or else E);
@end smallexample
@noindent
which is also equivalent to (in Ada 2012)
@smallexample @c ada
pragma Postcondition (if R'Old then E);
@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.
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);
@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 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
@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:
@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);
...
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.
@node Pragma Convention_Identifier
@unnumberedsec Pragma Convention_Identifier
@findex Convention_Identifier
@ -5238,9 +5342,12 @@ pragma Test_Case (
@noindent
The @code{Test_Case} pragma allows defining fine-grain specifications
for use by testing and verification tools. The compiler checks its
validity but the presence of pragma @code{Test_Case} does not lead to
any modification of the code generated by the compiler.
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.
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.
@code{Test_Case} pragmas may only appear immediately following the
(separate) declaration of a subprogram in a package declaration, inside
@ -5261,19 +5368,19 @@ package Math_Functions is
function Sqrt (Arg : Float) return Float;
pragma Test_Case (Name => "Test 1",
Mode => Nominal,
Requires => Arg < 100,
Requires => Arg < 10000,
Ensures => Sqrt'Result < 10);
...
end Math_Functions;
@end smallexample
@noindent
The meaning of a test case is that, if 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 satisfy the precondition of the
subprogram, and the output context should then satisfy its
postcondition. More @code{Robustness} indicates that the pre- and
The meaning of a test case is that there is at least one context where
@code{Requires} holds such that, if the associated subprogram is executed in
that context, then @code{Ensures} holds 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 test case.
@node Pragma Thread_Local_Storage
@ -17375,6 +17482,7 @@ A complete description of the AIs may be found in
@item @code{Atomic_Components} @tab
@item @code{Bit_Order} @tab
@item @code{Component_Size} @tab
@item @code{Contract_Case} @tab -- GNAT
@item @code{Discard_Names} @tab
@item @code{External_Tag} @tab
@item @code{Favor_Top_Level} @tab -- GNAT

1
gcc/ada/par-prag.adb
View File

@ -1109,6 +1109,7 @@ begin
Pragma_Compile_Time_Error |
Pragma_Compile_Time_Warning |
Pragma_Compiler_Unit |
Pragma_Contract_Case |
Pragma_Convention_Identifier |
Pragma_CPP_Class |
Pragma_CPP_Constructor |

14
gcc/ada/sem_attr.adb
View File

@ -4256,10 +4256,12 @@ package body Sem_Attr is
("% attribute can only appear in postcondition of function",
P);
elsif Get_Pragma_Id (Prag) = Pragma_Test_Case then
elsif Get_Pragma_Id (Prag) = Pragma_Contract_Case
or else Get_Pragma_Id (Prag) = Pragma_Test_Case
then
declare
Arg_Ens : constant Node_Id :=
Get_Ensures_From_Test_Case_Pragma (Prag);
Get_Ensures_From_Case_Pragma (Prag);
Arg : Node_Id;
begin
@ -4269,7 +4271,13 @@ package body Sem_Attr is
end loop;
if Arg /= Arg_Ens then
Error_Attr ("% attribute misplaced inside Test_Case", P);
if Get_Pragma_Id (Prag) = Pragma_Contract_Case then
Error_Attr
("% attribute misplaced inside contract case", P);
else
Error_Attr
("% attribute misplaced inside test case", P);
end if;
end if;
end;

144
gcc/ada/sem_ch13.adb
View File

@ -1450,83 +1450,87 @@ package body Sem_Ch13 is
Set_Is_Delayed_Aspect (Aspect);
Delay_Required := True;
when Aspect_Test_Case => declare
Args : List_Id;
Comp_Expr : Node_Id;
Comp_Assn : Node_Id;
New_Expr : Node_Id;
when Aspect_Contract_Case |
Aspect_Test_Case =>
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_N
("incorrect placement of aspect `Test_Case`", E);
goto Continue;
end if;
if Nkind (Expr) /= N_Aggregate then
Error_Msg_NE
("wrong syntax for aspect `Test_Case` 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
(Make_Pragma_Argument_Association (Sloc (Comp_Expr),
Expression => New_Expr),
Args);
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_NE
("wrong syntax for aspect `Test_Case` for &", Id, E);
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;
New_Expr := Relocate_Node (Expression (Comp_Assn));
Set_Original_Node (New_Expr, Expression (Comp_Assn));
Append (Make_Pragma_Argument_Association (
Sloc => Sloc (Comp_Assn),
Chars => Chars (First (Choices (Comp_Assn))),
Expression => New_Expr),
Args);
Next (Comp_Assn);
end loop;
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;
-- Build the test-case pragma
-- 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.
Aitem :=
Make_Pragma (Loc,
Pragma_Identifier =>
Make_Identifier (Sloc (Id), Name_Test_Case),
Pragma_Argument_Associations =>
Args);
Comp_Expr := First (Expressions (Expr));
while Present (Comp_Expr) loop
New_Expr := Relocate_Node (Comp_Expr);
Set_Original_Node (New_Expr, Comp_Expr);
Append
(Make_Pragma_Argument_Association (Sloc (Comp_Expr),
Expression => New_Expr),
Args);
Next (Comp_Expr);
end loop;
Set_From_Aspect_Specification (Aitem, True);
Set_Corresponding_Aspect (Aitem, Aspect);
Set_Is_Delayed_Aspect (Aspect);
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;
-- Insert immediately after the entity declaration
New_Expr := Relocate_Node (Expression (Comp_Assn));
Set_Original_Node (New_Expr, Expression (Comp_Assn));
Append (Make_Pragma_Argument_Association (
Sloc => Sloc (Comp_Assn),
Chars => Chars (First (Choices (Comp_Assn))),
Expression => New_Expr),
Args);
Next (Comp_Assn);
end loop;
Insert_After (N, Aitem);
-- Build the contract-case or test-case pragma
goto Continue;
end;
Aitem :=
Make_Pragma (Loc,
Pragma_Identifier =>
Make_Identifier (Sloc (Id), Nam),
Pragma_Argument_Associations =>
Args);
Set_From_Aspect_Specification (Aitem, True);
Set_Corresponding_Aspect (Aitem, Aspect);
Set_Is_Delayed_Aspect (Aspect);
-- Insert immediately after the entity declaration
Insert_After (N, Aitem);
goto Continue;
end;
when Aspect_Dimension =>
Analyze_Aspect_Dimension (N, Id, Expr);
@ -6158,7 +6162,13 @@ package body Sem_Ch13 is
when Boolean_Aspects =>
raise Program_Error;
-- Test_Case aspect applies to entries and subprograms, hence should
-- Contract_Case aspects apply to subprograms, hence should never be
-- delayed.
when Aspect_Contract_Case =>
raise Program_Error;
-- Test_Case aspects apply to entries and subprograms, hence should
-- never be delayed.
when Aspect_Test_Case =>

4
gcc/ada/sem_ch3.adb
View File

@ -2204,9 +2204,9 @@ package body Sem_Ch3 is
Check_Subprogram_Contract (Sent);
Prag := Spec_TC_List (Contract (Sent));
Prag := Spec_CTC_List (Contract (Sent));
while Present (Prag) loop
Analyze_TC_In_Decl_Part (Prag, Sent);
Analyze_CTC_In_Decl_Part (Prag, Sent);
Prag := Next_Pragma (Prag);
end loop;
end if;

130
gcc/ada/sem_ch6.adb
View File

@ -10932,6 +10932,11 @@ package body Sem_Ch6 is
Plist : List_Id := No_List;
-- List of generated postconditions
function Grab_CC return Node_Id;
-- Prag contains an analyzed contract case pragma. This function copies
-- relevant components of the pragma, creates the corresponding Check
-- pragma and returns the Check pragma as the result.
function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id;
-- Prag contains an analyzed precondition or postcondition pragma. This
-- function copies the pragma, changes it to the corresponding Check
@ -10954,6 +10959,87 @@ package body Sem_Ch6 is
-- that an invariant check is required (for an IN OUT parameter, or
-- the returned value of a function.
-------------
-- Grab_CC --
-------------
function Grab_CC return Node_Id is
CP : Node_Id;
Req : Node_Id;
Ens : Node_Id;
Post : Node_Id;
Loc : constant Source_Ptr := Sloc (Prag);
-- Similarly to postcondition, the string is "failed xx from yy"
-- where xx is in all lower case. The reason for this different
-- wording compared to other Check cases is that the failure is not
-- at the point of occurrence of the pragma, unlike the other Check
-- cases.
Msg : constant String :=
"failed contract case from " & Build_Location_String (Loc);
begin
-- Copy the Requires and Ensures expressions
Req := New_Copy_Tree (
Expression (Get_Requires_From_Case_Pragma (Prag)),
New_Scope => Current_Scope);
Ens := New_Copy_Tree (
Expression (Get_Ensures_From_Case_Pragma (Prag)),
New_Scope => Current_Scope);
-- Build the postcondition (not Requires'Old or else Ensures)
Post := Make_Or_Else (Loc,
Left_Opnd => Make_Op_Not (Loc,
Make_Attribute_Reference (Loc,
Prefix => Req,
Attribute_Name => Name_Old)),
Right_Opnd => Ens);
-- For a contract case pragma within a generic, generate a
-- postcondition pragma for later expansion. This is also used
-- when an error was detected, thus setting Expander_Active to False.
if not Expander_Active then
CP := Make_Pragma (Loc,
Chars => Name_Postcondition,
Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Loc,
Chars => Name_Check,
Expression => Post),
Make_Pragma_Argument_Association (Loc,
Chars => Name_Message,
Expression => Make_String_Literal (Loc, Msg))));
-- Otherwise, create the Check pragma
else
CP := Make_Pragma (Loc,
Chars => Name_Check,
Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Loc,
Chars => Name_Name,
Expression =>
Make_Identifier (Loc, Name_Postcondition)),
Make_Pragma_Argument_Association (Loc,
Chars => Name_Check,
Expression => Post),
Make_Pragma_Argument_Association (Loc,
Chars => Name_Message,
Expression => Make_String_Literal (Loc, Msg))));
end if;
-- Return the Postcondition or Check pragma
return CP;
end Grab_CC;
--------------
-- Grab_PPC --
--------------
@ -11005,7 +11091,8 @@ package body Sem_Ch6 is
Set_Comes_From_Source (CP, False);
-- For a postcondition pragma within a generic, preserve the pragma
-- for later expansion.
-- for later expansion. This is also used when an error was detected,
-- thus setting Expander_Active to False.
if Nam = Name_Postcondition
and then not Expander_Active
@ -11328,6 +11415,11 @@ package body Sem_Ch6 is
if Present (Spec_Id) then
Spec_Postconditions : declare
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 non-Empty.
procedure Process_Post_Conditions
(Spec : Node_Id;
Class : Boolean);
@ -11336,6 +11428,34 @@ package body Sem_Ch6 is
-- postconditions marked with Class_Present are considered.
-- The caller has checked that Spec_PPC_List is non-Empty.
----------------------------
-- Process_Contract_Cases --
----------------------------
procedure Process_Contract_Cases (Spec : Node_Id) is
begin
-- Loop through Contract_Case pragmas from spec
Prag := Spec_CTC_List (Contract (Spec));
loop
if Pragma_Name (Prag) = Name_Contract_Case then
if Plist = No_List then
Plist := Empty_List;
end if;
if not Expander_Active then
Prepend (Grab_CC, Declarations (N));
else
Append (Grab_CC, Plist);
end if;
end if;
Prag := Next_Pragma (Prag);
exit when No (Prag);
end loop;
end Process_Contract_Cases;
-----------------------------
-- Process_Post_Conditions --
-----------------------------
@ -11380,6 +11500,14 @@ package body Sem_Ch6 is
-- Start of processing for Spec_Postconditions
begin
-- Process postconditions expressed as contract-cases
if Present (Spec_CTC_List (Contract (Spec_Id))) then
Process_Contract_Cases (Spec_Id);
end if;
-- Process spec postconditions
if Present (Spec_PPC_List (Contract (Spec_Id))) then
Process_Post_Conditions (Spec_Id, Class => False);
end if;

134
gcc/ada/sem_prag.adb
View File

@ -181,10 +181,10 @@ package body Sem_Prag is
-- original one, following the renaming chain) is returned. Otherwise the
-- entity is returned unchanged. Should be in Einfo???
procedure Preanalyze_TC_Args (N, Arg_Req, Arg_Ens : Node_Id);
procedure Preanalyze_CTC_Args (N, Arg_Req, Arg_Ens : Node_Id);
-- Preanalyze the boolean expressions in the Requires and Ensures arguments
-- of a Test_Case pragma if present (possibly Empty). We treat these as
-- spec expressions (i.e. similar to a default expression).
-- of a Contract_Case or Test_Case pragma if present (possibly Empty). We
-- treat these as spec expressions (i.e. similar to a default expression).
procedure rv;
-- This is a dummy function called by the processing for pragma Reviewable.
@ -637,15 +637,16 @@ package body Sem_Prag is
-- that the constraint is static as required by the restrictions for
-- Unchecked_Union.
procedure Check_Test_Case;
-- Called to process a test-case pragma. The treatment is similar to the
-- one for pre- and postcondition in Check_Precondition_Postcondition,
-- except the placement rules for the test-case pragma are stricter.
-- This pragma may only occur after a subprogram spec declared directly
-- in a package spec unit. In this case, the pragma is chained to the
-- subprogram in question (using Spec_TC_List and Next_Pragma) and
-- analysis of the pragma is delayed till the end of the spec. In
-- all other cases, an error message for bad placement is given.
procedure Check_Contract_Or_Test_Case;
-- Called to process a contract-case or test-case pragma. The
-- treatment is similar to the one for pre- and postcondition in
-- Check_Precondition_Postcondition, except the placement rules for the
-- contract-case and test-case pragmas are stricter. These pragmas may
-- only occur after a subprogram spec declared directly in a package
-- spec unit. In this case, the pragma is chained to the subprogram in
-- question (using Spec_CTC_List and Next_Pragma) and analysis of the
-- pragma is delayed till the end of the spec. In all other cases, an
-- error message for bad placement is given.
procedure Check_Valid_Configuration_Pragma;
-- Legality checks for placement of a configuration pragma
@ -2113,24 +2114,25 @@ package body Sem_Prag is
end case;
end Check_Static_Constraint;
---------------------
-- Check_Test_Case --
---------------------
---------------------------------
-- Check_Contract_Or_Test_Case --
---------------------------------
procedure Check_Test_Case is
procedure Check_Contract_Or_Test_Case is
P : Node_Id;
PO : Node_Id;
procedure Chain_TC (PO : Node_Id);
procedure Chain_CTC (PO : Node_Id);
-- If PO is a [generic] subprogram declaration node, then the
-- test-case applies to this subprogram and the processing for the
-- pragma is completed. Otherwise the pragma is misplaced.
-- contract-case or test-case applies to this subprogram and the
-- processing for the pragma is completed. Otherwise the pragma
-- is misplaced.
--------------
-- Chain_TC --
--------------
---------------
-- Chain_CTC --
---------------
procedure Chain_TC (PO : Node_Id) is
procedure Chain_CTC (PO : Node_Id) is
S : Entity_Id;
begin
@ -2166,21 +2168,21 @@ package body Sem_Prag is
-- in this analysis, allowing forward references. The analysis
-- happens at the end of Analyze_Declarations.
-- There should not be another test case with the same name
-- associated to this subprogram.
-- There should not be another contract-case or test-case with the
-- same name associated to this subprogram.
declare
Name : constant String_Id := Get_Name_From_Test_Case_Pragma (N);
TC : Node_Id;
Name : constant String_Id := Get_Name_From_Case_Pragma (N);
CTC : Node_Id;
begin
TC := Spec_TC_List (Contract (S));
while Present (TC) loop
CTC := Spec_CTC_List (Contract (S));
while Present (CTC) loop
if String_Equal
(Name, Get_Name_From_Test_Case_Pragma (TC))
(Name, Get_Name_From_Case_Pragma (CTC))
then
Error_Msg_Sloc := Sloc (TC);
Error_Msg_Sloc := Sloc (CTC);
if From_Aspect_Specification (N) then
Error_Pragma ("name for aspect% is already used#");
@ -2189,24 +2191,24 @@ package body Sem_Prag is
end if;
end if;
TC := Next_Pragma (TC);
CTC := Next_Pragma (CTC);
end loop;
end;
-- Chain spec TC pragma to list for subprogram
-- Chain spec CTC pragma to list for subprogram
Set_Next_Pragma (N, Spec_TC_List (Contract (S)));
Set_Spec_TC_List (Contract (S), N);
end Chain_TC;
Set_Next_Pragma (N, Spec_CTC_List (Contract (S)));
Set_Spec_CTC_List (Contract (S), N);
end Chain_CTC;
-- Start of processing for Check_Test_Case
-- Start of processing for Check_Contract_Or_Test_Case
begin
if not Is_List_Member (N) then
Pragma_Misplaced;
end if;
-- Test cases should only appear in package spec unit
-- Contract-case or test-case should only appear in package spec unit
if Get_Source_Unit (N) = No_Unit
or else not Nkind_In (Sinfo.Unit (Cunit (Get_Source_Unit (N))),
@ -2224,9 +2226,9 @@ package body Sem_Prag is
-- If the previous node is a generic subprogram, do not go to to
-- the original node, which is the unanalyzed tree: we need to
-- attach the test-case to the analyzed version at this point.
-- They get propagated to the original tree when analyzing the
-- corresponding body.
-- attach the contract-case or test-case to the analyzed version
-- at this point. They get propagated to the original tree when
-- analyzing the corresponding body.
if Nkind (P) not in N_Generic_Declaration then
PO := Original_Node (P);
@ -2258,7 +2260,7 @@ package body Sem_Prag is
Pragma_Misplaced;
else
Chain_TC (PO);
Chain_CTC (PO);
return;
end if;
end loop;
@ -2266,7 +2268,7 @@ package body Sem_Prag is
-- If we fall through, pragma was misplaced
Pragma_Misplaced;
end Check_Test_Case;
end Check_Contract_Or_Test_Case;
--------------------------------------
-- Check_Valid_Configuration_Pragma --
@ -13904,18 +13906,21 @@ package body Sem_Prag is
end if;
end Task_Storage;
---------------
-- Test_Case --
---------------
-------------------------------
-- Contract_Case | Test_Case --
-------------------------------
-- pragma Test_Case ([Name =>] Static_String_EXPRESSION
-- pragma (Contract_Case | Test_Case)
-- ([Name =>] Static_String_EXPRESSION
-- ,[Mode =>] MODE_TYPE
-- [, Requires => Boolean_EXPRESSION]
-- [, Ensures => Boolean_EXPRESSION]);
-- MODE_TYPE ::= Nominal | Robustness
when Pragma_Test_Case => Test_Case : declare
when Pragma_Contract_Case |
Pragma_Test_Case =>
Contract_Or_Test_Case : declare
begin
GNAT_Pragma;
Check_At_Least_N_Arguments (2);
@ -13947,8 +13952,8 @@ package body Sem_Prag is
Check_Identifier_Is_One_Of (Arg3, Name_Requires, Name_Ensures);
end if;
Check_Test_Case;
end Test_Case;
Check_Contract_Or_Test_Case;
end Contract_Or_Test_Case;
--------------------------
-- Thread_Local_Storage --
@ -14819,11 +14824,11 @@ package body Sem_Prag is
when Pragma_Exit => null;
end Analyze_Pragma;
-----------------------------
-- Analyze_TC_In_Decl_Part --
-----------------------------
------------------------------
-- Analyze_CTC_In_Decl_Part --
------------------------------
procedure Analyze_TC_In_Decl_Part (N : Node_Id; S : Entity_Id) is
procedure Analyze_CTC_In_Decl_Part (N : Node_Id; S : Entity_Id) is
begin
-- Install formals and push subprogram spec onto scope stack so that we
-- can see the formals from the pragma.
@ -14834,15 +14839,15 @@ package body Sem_Prag is
-- Preanalyze the boolean expressions, we treat these as spec
-- expressions (i.e. similar to a default expression).
Preanalyze_TC_Args (N,
Get_Requires_From_Test_Case_Pragma (N),
Get_Ensures_From_Test_Case_Pragma (N));
Preanalyze_CTC_Args (N,
Get_Requires_From_Case_Pragma (N),
Get_Ensures_From_Case_Pragma (N));
-- Remove the subprogram from the scope stack now that the pre-analysis
-- of the expressions in the test-case is done.
-- of the expressions in the contract-case or test-case is done.
End_Scope;
end Analyze_TC_In_Decl_Part;
end Analyze_CTC_In_Decl_Part;
--------------------
-- Check_Disabled --
@ -15077,6 +15082,7 @@ package body Sem_Prag is
Pragma_Complete_Representation => 0,
Pragma_Complex_Representation => 0,
Pragma_Component_Alignment => -1,
Pragma_Contract_Case => -1,
Pragma_Controlled => 0,
Pragma_Convention => 0,
Pragma_Convention_Identifier => 0,
@ -15431,11 +15437,11 @@ package body Sem_Prag is
end if;
end Make_Aspect_For_PPC_In_Gen_Sub_Decl;
------------------------
-- Preanalyze_TC_Args --
------------------------
-------------------------
-- Preanalyze_CTC_Args --
-------------------------
procedure Preanalyze_TC_Args (N, Arg_Req, Arg_Ens : Node_Id) is
procedure Preanalyze_CTC_Args (N, Arg_Req, Arg_Ens : Node_Id) is
begin
-- Preanalyze the boolean expressions, we treat these as spec
-- expressions (i.e. similar to a default expression).
@ -15465,7 +15471,7 @@ package body Sem_Prag is
(Original_Node (Get_Pragma_Arg (Arg_Ens)), Standard_Boolean);
end if;
end if;
end Preanalyze_TC_Args;
end Preanalyze_CTC_Args;
--------------------------------------
-- Process_Compilation_Unit_Pragmas --

14
gcc/ada/sem_prag.ads
View File

@ -46,13 +46,13 @@ package Sem_Prag is
procedure Analyze_Pragma (N : Node_Id);
-- Analyze procedure for pragma reference node N
procedure Analyze_TC_In_Decl_Part (N : Node_Id; S : Entity_Id);
-- Special analyze routine for test-case pragma that appears within a
-- declarative part where the pragma is associated with a subprogram
-- specification. N is the pragma node, and S is the entity for the related
-- subprogram. This procedure does a preanalysis of the expressions in the
-- pragma as "spec expressions" (see section in Sem "Handling of Default
-- and Per-Object Expressions...").
procedure Analyze_CTC_In_Decl_Part (N : Node_Id; S : Entity_Id);
-- Special analyze routine for contract-case and test-case pragmas that
-- appears within a declarative part where the pragma is associated with
-- a subprogram specification. N is the pragma node, and S is the entity
-- for the related subprogram. This procedure does a preanalysis of the
-- expressions in the pragma as "spec expressions" (see section in Sem
-- "Handling of Default and Per-Object Expressions...").
function Check_Disabled (Nam : Name_Id) return Boolean;
-- This function is used in connection with pragmas Assertion, Check,

30
gcc/ada/sem_util.adb
View File

@ -4490,11 +4490,11 @@ package body Sem_Util is
end if;
end Get_Enum_Lit_From_Pos;
---------------------------------------
-- Get_Ensures_From_Test_Case_Pragma --
---------------------------------------
----------------------------------
-- Get_Ensures_From_Case_Pragma --
----------------------------------
function Get_Ensures_From_Test_Case_Pragma (N : Node_Id) return Node_Id is
function Get_Ensures_From_Case_Pragma (N : Node_Id) return Node_Id is
Args : constant List_Id := Pragma_Argument_Associations (N);
Res : Node_Id;
@ -4514,7 +4514,7 @@ package body Sem_Util is
end if;
return Res;
end Get_Ensures_From_Test_Case_Pragma;
end Get_Ensures_From_Case_Pragma;
------------------------
-- Get_Generic_Entity --
@ -4602,16 +4602,16 @@ package body Sem_Util is
return Entity_Id (Get_Name_Table_Info (Id));
end Get_Name_Entity_Id;
------------------------------------
-- Get_Name_From_Test_Case_Pragma --
------------------------------------
-------------------------------
-- Get_Name_From_Case_Pragma --
-------------------------------
function Get_Name_From_Test_Case_Pragma (N : Node_Id) return String_Id is
function Get_Name_From_Case_Pragma (N : Node_Id) return String_Id is
Arg : constant Node_Id :=
Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
begin
return Strval (Expr_Value_S (Arg));
end Get_Name_From_Test_Case_Pragma;
end Get_Name_From_Case_Pragma;
-------------------
-- Get_Pragma_Id --
@ -4656,11 +4656,11 @@ package body Sem_Util is
return R;
end Get_Renamed_Entity;
----------------------------------------
-- Get_Requires_From_Test_Case_Pragma --
----------------------------------------
-----------------------------------
-- Get_Requires_From_Case_Pragma --
-----------------------------------
function Get_Requires_From_Test_Case_Pragma (N : Node_Id) return Node_Id is
function Get_Requires_From_Case_Pragma (N : Node_Id) return Node_Id is
Args : constant List_Id := Pragma_Argument_Associations (N);
Res : Node_Id;
@ -4677,7 +4677,7 @@ package body Sem_Util is
end if;
return Res;
end Get_Requires_From_Test_Case_Pragma;
end Get_Requires_From_Case_Pragma;
-------------------------
-- Get_Subprogram_Body --

14
gcc/ada/sem_util.ads
View File

@ -538,8 +538,9 @@ package Sem_Util is
-- If expression N references a part of an object, return this object.
-- Otherwise return Empty. Expression N should have been resolved already.
function Get_Ensures_From_Test_Case_Pragma (N : Node_Id) return Node_Id;
-- Return the Ensures component of Test_Case pragma N, or Empty otherwise
function Get_Ensures_From_Case_Pragma (N : Node_Id) return Node_Id;
-- Return the Ensures component of Contract_Case or Test_Case pragma N, or
-- Empty otherwise.
function Get_Generic_Entity (N : Node_Id) return Entity_Id;
-- Returns the true generic entity in an instantiation. If the name in the
@ -572,8 +573,8 @@ package Sem_Util is
-- is the innermost visible entity with the given name. See the body of
-- Sem_Ch8 for further details on handling of entity visibility.
function Get_Name_From_Test_Case_Pragma (N : Node_Id) return String_Id;
-- Return the Name component of Test_Case pragma N
function Get_Name_From_Case_Pragma (N : Node_Id) return String_Id;
-- Return the Name component of Contract_Case or Test_Case pragma N
function Get_Pragma_Id (N : Node_Id) return Pragma_Id;
pragma Inline (Get_Pragma_Id);
@ -590,8 +591,9 @@ package Sem_Util is
-- not a renamed entity, returns its argument. It is an error to call this
-- with any other kind of entity.
function Get_Requires_From_Test_Case_Pragma (N : Node_Id) return Node_Id;
-- Return the Requires component of Test_Case pragma N, or Empty otherwise
function Get_Requires_From_Case_Pragma (N : Node_Id) return Node_Id;
-- Return the Requires component of Contract_Case or Test_Case pragma N, or
-- Empty otherwise.
function Get_Subprogram_Entity (Nod : Node_Id) return Entity_Id;
-- Nod is either a procedure call statement, or a function call, or an

10
gcc/ada/sem_warn.adb
View File

@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 1999-2011, Free Software Foundation, Inc. --
-- Copyright (C) 1999-2012, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@ -1749,7 +1749,7 @@ package body Sem_Warn is
function Within_Postcondition return Boolean;
-- Returns True iff N is within a Postcondition or
-- Ensures component in a Test_Case.
-- Ensures component in a Contract_Case or Test_Case.
--------------------------
-- Within_Postcondition --
@ -1770,9 +1770,11 @@ package body Sem_Warn is
P := Parent (Nod);
if Nkind (P) = N_Pragma
and then Pragma_Name (P) = Name_Test_Case
and then
Nod = Get_Ensures_From_Test_Case_Pragma (P)
(Pragma_Name (P) = Name_Contract_Case
or else Pragma_Name (P) = Name_Test_Case)
and then
Nod = Get_Ensures_From_Case_Pragma (P)
then
return True;
end if;

10
gcc/ada/sinfo.adb
View File

@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- Copyright (C) 1992-2012, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@ -2812,13 +2812,13 @@ package body Sinfo is
return Node1 (N);
end Spec_PPC_List;
function Spec_TC_List
function Spec_CTC_List
(N : Node_Id) return Node_Id is
begin
pragma Assert (False
or else NT (N).Nkind = N_Contract);
return Node2 (N);
end Spec_TC_List;
end Spec_CTC_List;
function Specification
(N : Node_Id) return Node_Id is
@ -5892,13 +5892,13 @@ package body Sinfo is
Set_Node1 (N, Val); -- semantic field, no parent set
end Set_Spec_PPC_List;
procedure Set_Spec_TC_List
procedure Set_Spec_CTC_List
(N : Node_Id; Val : Node_Id) is
begin
pragma Assert (False
or else NT (N).Nkind = N_Contract);
Set_Node2 (N, Val); -- semantic field, no parent set
end Set_Spec_TC_List;
end Set_Spec_CTC_List;
procedure Set_Specification
(N : Node_Id; Val : Node_Id) is

25
gcc/ada/sinfo.ads
View File

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- Copyright (C) 1992-2012, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@ -6969,7 +6969,7 @@ package Sinfo is
-- N_Contract
-- Sloc points to the subprogram's name
-- Spec_PPC_List (Node1) (set to Empty if none)
-- Spec_TC_List (Node2) (set to Empty if none)
-- Spec_CTC_List (Node2) (set to Empty if none)
-- Spec_PPC_List points to a list of Precondition and Postcondition
-- pragma nodes for preconditions and postconditions declared in the
@ -6978,11 +6978,12 @@ package Sinfo is
-- Note that this includes precondition/postcondition pragmas generated
-- to correspond to Pre/Post aspects.
-- Spec_TC_List points to a list of Test_Case pragma nodes for
-- test-cases declared in the spec of the entry/subprogram. The last
-- pragma encountered is at the head of this list, so it is in reverse
-- order of textual appearance. Note that this includes test-case
-- pragmas generated to correspond to Test_Case aspects.
-- Spec_CTC_List points to a list of Contract_Case and Test_Case pragma
-- nodes for contract-cases and test-cases declared in the spec of the
-- entry/subprogram. The last pragma encountered is at the head of this
-- list, so it is in reverse order of textual appearance. Note that
-- this includes contract-case and test-case pragmas generated from
-- Contract_Case and Test_Case aspects.
-------------------
-- Expanded_Name --
@ -8963,7 +8964,7 @@ package Sinfo is
function Spec_PPC_List
(N : Node_Id) return Node_Id; -- Node1
function Spec_TC_List
function Spec_CTC_List
(N : Node_Id) return Node_Id; -- Node2
function Specification
@ -9944,7 +9945,7 @@ package Sinfo is
procedure Set_Spec_PPC_List
(N : Node_Id; Val : Node_Id); -- Node1
procedure Set_Spec_TC_List
procedure Set_Spec_CTC_List
(N : Node_Id; Val : Node_Id); -- Node2
procedure Set_Specification
@ -11590,7 +11591,7 @@ package Sinfo is
N_Contract =>
(1 => False, -- Spec_PPC_List (Node1)
2 => False, -- Spec_TC_List (Node2)
2 => False, -- Spec_CTC_List (Node2)
3 => False, -- unused
4 => False, -- unused
5 => False), -- unused
@ -12084,7 +12085,7 @@ package Sinfo is
pragma Inline (Shift_Count_OK);
pragma Inline (Source_Type);
pragma Inline (Spec_PPC_List);
pragma Inline (Spec_TC_List);
pragma Inline (Spec_CTC_List);
pragma Inline (Specification);
pragma Inline (Split_PPC);
pragma Inline (Statements);
@ -12407,7 +12408,7 @@ package Sinfo is
pragma Inline (Set_Shift_Count_OK);
pragma Inline (Set_Source_Type);
pragma Inline (Set_Spec_PPC_List);
pragma Inline (Set_Spec_TC_List);
pragma Inline (Set_Spec_CTC_List);
pragma Inline (Set_Specification);
pragma Inline (Set_Split_PPC);
pragma Inline (Set_Statements);

2
gcc/ada/snames.ads-tmpl
View File

@ -448,6 +448,7 @@ package Snames is
Name_Common_Object : constant Name_Id := N + $; -- GNAT
Name_Complete_Representation : constant Name_Id := N + $; -- GNAT
Name_Complex_Representation : constant Name_Id := N + $; -- GNAT
Name_Contract_Case : constant Name_Id := N + $; -- GNAT
Name_Controlled : constant Name_Id := N + $;
Name_Convention : constant Name_Id := N + $;
Name_CPP_Class : constant Name_Id := N + $; -- GNAT
@ -1623,6 +1624,7 @@ package Snames is
Pragma_Common_Object,
Pragma_Complete_Representation,
Pragma_Complex_Representation,
Pragma_Contract_Case,
Pragma_Controlled,
Pragma_Convention,
Pragma_CPP_Class,