Patchwork [Ada] Correct placement and checking of Test_Case pragma

login
register
mail settings
Submitter Arnaud Charlet
Date Aug. 4, 2011, 1:38 p.m.
Message ID <20110804133815.GA10374@adacore.com>
Download mbox | patch
Permalink /patch/108465/
State New
Headers show

Comments

Arnaud Charlet - Aug. 4, 2011, 1:38 p.m.
Follow-up of changes for Test_Case pragma. Pragma is not allowed inside
subprogram body, only after separate declaration. No two test cases with same
name allowed on same entity. Correct error in checking procedure.

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-08-04  Yannick Moy  <moy@adacore.com>

	* gnat_rm.texi: Document that Test_Case pragma can only appear on
	separate declarations.
	* sem_prag.adb (procedure Check_Identifier_Is_One_Of): new procedure to
	check identifier of pragma argument.
	(Chain_TC): check that no other test case associated to the same entity
	share the same name.
	(Check_Test_Case): disallow test case inside subprogram body
	(Analyze_Pragma): correct call to check identifier and not argument
	* sem_util.adb, sem_util.ads (Get_Name_From_Test_Case_Pragma): new
	function gets name from test case pragma.

Patch

Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi	(revision 177384)
+++ gnat_rm.texi	(working copy)
@@ -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
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 177384)
+++ sem_prag.adb	(working copy)
@@ -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;
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 177384)
+++ sem_util.adb	(working copy)
@@ -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 --
    -------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 177384)
+++ sem_util.ads	(working copy)
@@ -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