===================================================================
@@ -5025,14 +5025,16 @@
@end smallexample
@noindent
-The @code{Test_Case} pragma applies to the same entities as pragmas
-@code{Precondition} and @code{Postcondition}. In particular, the
-placement and visibility rules are identical to those described for pre-
-and postconditions. But the presence of pragma @code{Test_Case} does not
-lead to any modification of the code generated by the compiler. Rather,
-its purpose is to document finer-grain specifications for use by testing
-and verification tools.
+The @code{Test_Case} pragma allows defining fine-grain specifications
+for use by testing and verification tools. The compiler only checks its
+validity but the presence of pragma @code{Test_Case} does not lead to
+any modification of the code generated by the compiler.
+@code{Test_Case} pragmas may only appear immediately following the
+(separate) declaration of a subprogram. Only other pragmas may intervene
+(that is appear between the subprogram declaration and its
+postconditions).
+
The compiler checks that boolean expression 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
@@ -5053,14 +5055,6 @@
end Math_Functions;
@end smallexample
-@noindent
-@code{Test_Case} pragmas may appear either immediately following the
-(separate) declaration of a subprogram, or at the start of the
-declarations of a subprogram body. Only other pragmas may intervene
-(that is appear between the subprogram declaration and its test cases,
-or appear before the test case in the declaration sequence in a
-subprogram body).
-
@node Pragma Thread_Local_Storage
@unnumberedsec Pragma Thread_Local_Storage
@findex Thread_Local_Storage
===================================================================
@@ -423,8 +423,14 @@
-- Checks that the given argument has an identifier, and if so, requires
-- it to match the given identifier name. If there is no identifier, or
-- a non-matching identifier, then an error message is given and
- -- Error_Pragmas raised.
+ -- Pragma_Exit is raised.
+ procedure Check_Identifier_Is_One_Of (Arg : Node_Id; N1, N2 : Name_Id);
+ -- Checks that the given argument has an identifier, and if so, requires
+ -- it to match one of the given identifier names. If there is no
+ -- identifier, or a non-matching identifier, then an error message is
+ -- given and Pragma_Exit is raised.
+
procedure Check_In_Main_Program;
-- Common checks for pragmas that appear within a main program
-- (Priority, Main_Storage, Time_Slice, Relative_Deadline, CPU).
@@ -454,12 +460,12 @@
procedure Check_Optional_Identifier (Arg : Node_Id; Id : Name_Id);
-- Checks if the given argument has an identifier, and if so, requires
-- it to match the given identifier name. If there is a non-matching
- -- identifier, then an error message is given and Error_Pragmas raised.
+ -- identifier, then an error message is given and Pragma_Exit is raised.
procedure Check_Optional_Identifier (Arg : Node_Id; Id : String);
-- Checks if the given argument has an identifier, and if so, requires
-- it to match the given identifier name. If there is a non-matching
- -- identifier, then an error message is given and Error_Pragmas raised.
+ -- identifier, then an error message is given and Pragma_Exit is raised.
-- In this version of the procedure, the identifier name is given as
-- a string with lower case letters.
@@ -1432,6 +1438,30 @@
end if;
end Check_Identifier;
+ --------------------------------
+ -- Check_Identifier_Is_One_Of --
+ --------------------------------
+
+ procedure Check_Identifier_Is_One_Of (Arg : Node_Id; N1, N2 : Name_Id) is
+ begin
+ if Present (Arg)
+ and then Nkind (Arg) = N_Pragma_Argument_Association
+ then
+ if Chars (Arg) = No_Name then
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_N ("pragma% argument expects an identifier", Arg);
+ raise Pragma_Exit;
+
+ elsif Chars (Arg) /= N1
+ and then Chars (Arg) /= N2
+ then
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_N ("invalid identifier for pragma% argument", Arg);
+ raise Pragma_Exit;
+ end if;
+ end if;
+ end Check_Identifier_Is_One_Of;
+
---------------------------
-- Check_In_Main_Program --
---------------------------
@@ -1989,6 +2019,33 @@
-- 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.
+
+ declare
+ Name : constant String_Id := Get_Name_From_Test_Case_Pragma (N);
+ TC : Node_Id;
+
+ begin
+ TC := Spec_TC_List (Contract (S));
+ while Present (TC) loop
+
+ if String_Equal
+ (Name, Get_Name_From_Test_Case_Pragma (TC))
+ then
+ Error_Msg_Sloc := Sloc (TC);
+
+ if From_Aspect_Specification (N) then
+ Error_Pragma ("name for aspect% is already used#");
+ else
+ Error_Pragma ("name for pragma% is already used#");
+ end if;
+ end if;
+
+ TC := Next_Pragma (TC);
+ end loop;
+ end;
+
-- Chain spec TC pragma to list for subprogram
Set_Next_Pragma (N, Spec_TC_List (Contract (S)));
@@ -2039,25 +2096,9 @@
end loop;
-- If we fall through loop, pragma is at start of list, so see if it
- -- is at the start of declarations of a subprogram body.
+ -- is in the pragmas after a library level subprogram.
- if Nkind (Parent (N)) = N_Subprogram_Body
- and then List_Containing (N) = Declarations (Parent (N))
- then
- if Operating_Mode /= Generate_Code
- or else Inside_A_Generic
- then
- -- Analyze pragma expressions for correctness and for ASIS use
-
- Preanalyze_TC_Args (Get_Requires_From_Test_Case_Pragma (N),
- Get_Ensures_From_Test_Case_Pragma (N));
- end if;
-
- return;
-
- -- See if it is in the pragmas after a library level subprogram
-
- elsif Nkind (Parent (N)) = N_Compilation_Unit_Aux then
+ if Nkind (Parent (N)) = N_Compilation_Unit_Aux then
Chain_TC (Unit (Parent (Parent (N))));
return;
end if;
@@ -13246,7 +13287,7 @@
Check_Identifier (Arg3, Name_Requires);
Check_Identifier (Arg4, Name_Ensures);
else
- Check_Arg_Is_One_Of (Arg3, Name_Requires, Name_Ensures);
+ Check_Identifier_Is_One_Of (Arg3, Name_Requires, Name_Ensures);
end if;
Check_Test_Case;
===================================================================
@@ -4331,6 +4331,16 @@
return Entity_Id (Get_Name_Table_Info (Id));
end Get_Name_Entity_Id;
+ ------------------------------------
+ -- Get_Name_From_Test_Case_Pragma --
+ ------------------------------------
+
+ function Get_Name_From_Test_Case_Pragma (N : Node_Id) return String_Id is
+ begin
+ return
+ Strval (Get_Pragma_Arg (First (Pragma_Argument_Associations (N))));
+ end Get_Name_From_Test_Case_Pragma;
+
-------------------
-- Get_Pragma_Id --
-------------------
===================================================================
@@ -485,7 +485,7 @@
-- 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 components of Test_Case pragma N, or Empty otherwise
+ -- Return the Ensures component of 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
@@ -518,6 +518,9 @@
-- 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_Pragma_Id (N : Node_Id) return Pragma_Id;
pragma Inline (Get_Pragma_Id);
-- Obtains the Pragma_Id from the Chars field of Pragma_Identifier (N)
@@ -534,7 +537,7 @@
-- with any other kind of entity.
function Get_Requires_From_Test_Case_Pragma (N : Node_Id) return Node_Id;
- -- Return the Requires components of Test_Case pragma N, or Empty otherwise
+ -- Return the Requires component of 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