Patchwork [Ada] Implement non-classwide Pre/Post aspects

login
register
mail settings
Submitter Arnaud Charlet
Date Oct. 12, 2010, 10:20 a.m.
Message ID <20101012102056.GA12579@adacore.com>
Download mbox | patch
Permalink /patch/67517/
State New
Headers show

Comments

Arnaud Charlet - Oct. 12, 2010, 10:20 a.m.
This patch completes the implementation of the non-classwide versions
of the Pre/Post aspects. The following shows a simple test:

with Text_IO; use Text_IO;
procedure prepost is
   function F (X : Integer) return Integer with
   Pre  => X > 10,
   Post => F'Result = X + 1;

   function F (X : Integer) return Integer is
   begin
      if X = 13 then
         return X;
      else
         return X + 1;
      end if;
   end F;


begin
   Put_Line (F (11)'Img);

   begin
      Put_Line (F (10)'Img);
   exception
      when others =>
         Put_Line ("precondition fails");
   end;

   begin
      Put_Line (F (13)'Img);
   exception
      when others =>
         Put_Line ("postcondition fails");
   end;
end;

Compiled and run with -gnat12 -gnata, the output is:

 12
precondition fails
postcondition fails

The following test shows some error messages given now:

     1. package PrePostErr is
     2.    procedure P1 is abstract with
     3.      Pre  => True,
             |
        >>> aspect "Pre" requires 'Class for abstract subprogram

     4.      Post => False;
             |
        >>> aspect "Post" requires 'Class for abstract subprogram

     5.
     6.    procedure P2 is abstract;
     7.    pragma Precondition (True);
           |
        >>> pragma "Precondition" cannot be applied to abstract subprogram

     8.    pragma Postcondition (False);
           |
        >>> pragma "Postcondition" cannot be applied to abstract subprogram

     9.
    10.    procedure P3 with
    11.      Pre  => True,
    12.      Post => False;
    13.    pragma Precondition (True);
           |
        >>> pragma "Precondition" not allowed, "Pre" aspect given at line 11

    14.    pragma Postcondition (False);
           |
        >>> pragma "Postcondition" not allowed, "Post" aspect given at line 12

    15. end PrePostErr;

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

2010-10-12  Robert Dewar  <dewar@adacore.com>

	* par-ch13.adb (P_Aspect_Specifications): Fix handling of 'Class aspects
	* sem_ch13.adb (Analyze_Aspect_Specifications): Fix bad Sloc on aspects
	* sem_prag.adb (Fix_Error): Only change pragma names for pragmas from
	aspects.
	(Check_Optional_Identifier): Handle case of direct arguments
	(Chain_PPC): Test for abstract case, giving appropriate messages
	* sinfo.ads, sinfo.adb (Class_Present): Allowed on N_Pragma node

Patch

Index: sinfo.adb
===================================================================
--- sinfo.adb	(revision 165354)
+++ sinfo.adb	(revision 165355)
@@ -412,7 +412,8 @@  package body Sinfo is
       (N : Node_Id) return Boolean is
    begin
       pragma Assert (False
-        or else NT (N).Nkind = N_Aspect_Specification);
+        or else NT (N).Nkind = N_Aspect_Specification
+        or else NT (N).Nkind = N_Pragma);
       return Flag6 (N);
    end Class_Present;
 
@@ -3372,7 +3373,8 @@  package body Sinfo is
       (N : Node_Id; Val : Boolean := True) is
    begin
       pragma Assert (False
-        or else NT (N).Nkind = N_Aspect_Specification);
+        or else NT (N).Nkind = N_Aspect_Specification
+        or else NT (N).Nkind = N_Pragma);
       Set_Flag6 (N, Val);
    end Set_Class_Present;
 
Index: sinfo.ads
===================================================================
--- sinfo.ads	(revision 165354)
+++ sinfo.ads	(revision 165355)
@@ -2028,6 +2028,7 @@  package Sinfo is
       --  Is_Delayed_Aspect (Flag14-Sem)
       --  Import_Interface_Present (Flag16-Sem)
       --  Aspect_Cancel (Flag11-Sem)
+      --  Class_Present (Flag6) (set False if not from Aspect with 'Class)
 
       --  Note: we should have a section on what pragmas are passed on to
       --  the back end to be processed. This section should note that pragma
Index: par-ch13.adb
===================================================================
--- par-ch13.adb	(revision 165354)
+++ par-ch13.adb	(revision 165355)
@@ -409,10 +409,9 @@  package body Ch13 is
 
          --  We have an identifier (which should be an aspect identifier)
 
-         Aspect := Token_Node;
          A_Id := Get_Aspect_Id (Token_Name);
          Aspect :=
-           Make_Aspect_Specification (Sloc (Aspect),
+           Make_Aspect_Specification (Token_Ptr,
              Identifier => Token_Node);
 
          --  No valid aspect identifier present
@@ -465,6 +464,10 @@  package body Ch13 is
                      if Token = Tok_Identifier then
                         Scan; -- past identifier not CLASS
                      end if;
+
+                  else
+                     Scan; -- past CLASS
+                     Set_Class_Present (Aspect);
                   end if;
                end if;
             end if;
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 165354)
+++ sem_prag.adb	(revision 165355)
@@ -566,9 +566,8 @@  package body Sem_Prag is
       --  This is called prior to issuing an error message. Msg is a string
       --  which typically contains the substring pragma. If the current pragma
       --  comes from an aspect, each such "pragma" substring is replaced with
-      --  the characters "aspect", and in addition, if Error_Msg_Name_1 is
-      --  Name_Precondition (resp Name_Postcondition) it is replaced with
-      --  Name_Pre (resp Name_Post).
+      --  the characters "aspect", and if Error_Msg_Name_1 is Name_Precondition
+      --  (resp Name_Postcondition) it is changed to Name_Pre (resp Name_Post).
 
       procedure Gather_Associations
         (Names : Name_List;
@@ -1463,7 +1462,10 @@  package body Sem_Prag is
 
       procedure Check_Optional_Identifier (Arg : Node_Id; Id : Name_Id) is
       begin
-         if Present (Arg) and then Chars (Arg) /= No_Name then
+         if Present (Arg)
+           and then Nkind (Arg) = N_Pragma_Argument_Association
+           and then Chars (Arg) /= No_Name
+         then
             if Chars (Arg) /= Id then
                Error_Msg_Name_1 := Pname;
                Error_Msg_Name_2 := Id;
@@ -1499,11 +1501,26 @@  package body Sem_Prag is
          ---------------
 
          procedure Chain_PPC (PO : Node_Id) is
-            S : Node_Id;
+            S   : Entity_Id;
+            P   : Node_Id;
 
          begin
-            if not Nkind_In (PO, N_Subprogram_Declaration,
-                                 N_Generic_Subprogram_Declaration)
+            if Nkind (PO) = N_Abstract_Subprogram_Declaration then
+               if not From_Aspect_Specification (N) then
+                  Error_Pragma
+                    ("pragma% cannot be applied to abstract subprogram");
+
+               elsif Class_Present (N) then
+                  Error_Pragma
+                    ("aspect `%''Class` not implemented yet");
+
+               else
+                  Error_Pragma
+                    ("aspect % requires ''Class for abstract subprogram");
+               end if;
+
+            elsif not Nkind_In (PO, N_Subprogram_Declaration,
+                                    N_Generic_Subprogram_Declaration)
             then
                Pragma_Misplaced;
             end if;
@@ -1512,6 +1529,35 @@  package body Sem_Prag is
 
             S := Defining_Unit_Name (Specification (PO));
 
+            --  Make sure we do not have the case of a pre/postcondition
+            --  pragma when the corresponding aspect is present. This is
+            --  never allowed. We allow either pragmas or aspects, not both.
+
+            --  We do this by looking at pragmas already chained to the entity
+            --  since the aspect derived pragma will be put on this list first.
+
+            if not From_Aspect_Specification (N) then
+               P := Spec_PPC_List (S);
+               while Present (P) loop
+                  if Pragma_Name (P) = Pragma_Name (N)
+                    and then From_Aspect_Specification (P)
+                  then
+                     Error_Msg_Sloc := Sloc (P);
+
+                     if Prag_Id = Pragma_Precondition then
+                        Error_Msg_Name_2 := Name_Pre;
+                     else
+                        Error_Msg_Name_2 := Name_Post;
+                     end if;
+
+                     Error_Pragma
+                       ("pragma% not allowed, % aspect given#");
+                  end if;
+
+                  P := Next_Pragma (P);
+               end loop;
+            end if;
+
             --  Analyze the pragma unless it appears within a package spec,
             --  which is the case where we delay the analysis of the PPC until
             --  the end of the package declarations (for details, see
@@ -2059,12 +2105,12 @@  package body Sem_Prag is
                   Msg (J .. J + 5) := "aspect";
                end if;
             end loop;
-         end if;
 
-         if Error_Msg_Name_1 = Name_Precondition then
-            Error_Msg_Name_1 := Name_Pre;
-         elsif Error_Msg_Name_1 = Name_Postcondition then
-            Error_Msg_Name_1 := Name_Post;
+            if Error_Msg_Name_1 = Name_Precondition then
+               Error_Msg_Name_1 := Name_Pre;
+            elsif Error_Msg_Name_1 = Name_Postcondition then
+               Error_Msg_Name_1 := Name_Post;
+            end if;
          end if;
       end Fix_Error;
 
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 165354)
+++ sem_ch13.adb	(revision 165355)
@@ -663,10 +663,11 @@  package body Sem_Ch13 is
       Aspect := First (L);
       while Present (Aspect) loop
          declare
-            Id   : constant Node_Id   := Identifier (Aspect);
-            Expr : constant Node_Id   := Expression (Aspect);
-            Nam  : constant Name_Id   := Chars (Id);
-            A_Id : constant Aspect_Id := Get_Aspect_Id (Nam);
+            Loc  : constant Source_Ptr := Sloc (Aspect);
+            Id   : constant Node_Id    := Identifier (Aspect);
+            Expr : constant Node_Id    := Expression (Aspect);
+            Nam  : constant Name_Id    := Chars (Id);
+            A_Id : constant Aspect_Id  := Get_Aspect_Id (Nam);
             Anod : Node_Id;
             T    : Entity_Id;
 
@@ -728,7 +729,7 @@  package body Sem_Ch13 is
                   --  Build corresponding pragma node
 
                   Aitem :=
-                    Make_Pragma (Sloc (Aspect),
+                    Make_Pragma (Loc,
                       Pragma_Argument_Associations => New_List (Ent),
                       Pragma_Identifier            =>
                         Make_Identifier (Sloc (Id), Chars (Id)));
@@ -797,7 +798,7 @@  package body Sem_Ch13 is
                   --  Construct the attribute definition clause
 
                   Aitem :=
-                    Make_Attribute_Definition_Clause (Sloc (Aspect),
+                    Make_Attribute_Definition_Clause (Loc,
                       Name       => Ent,
                       Chars      => Chars (Id),
                       Expression => Relocate_Node (Expr));
@@ -823,7 +824,7 @@  package body Sem_Ch13 is
                   --  Construct the pragma
 
                   Aitem :=
-                    Make_Pragma (Sloc (Aspect),
+                    Make_Pragma (Loc,
                       Pragma_Argument_Associations => New_List (
                         New_Occurrence_Of (E, Sloc (Expr)),
                         Relocate_Node (Expr)),
@@ -844,54 +845,61 @@  package body Sem_Ch13 is
                   --  Construct the pragma
 
                   Aitem :=
-                    Make_Pragma (Sloc (Aspect),
+                    Make_Pragma (Loc,
                       Pragma_Argument_Associations => New_List (
                         Relocate_Node (Expr),
                         New_Occurrence_Of (E, Sloc (Expr))),
                       Pragma_Identifier            =>
-                         Make_Identifier (Sloc (Id), Chars (Id)));
+                        Make_Identifier (Sloc (Id), Chars (Id)),
+                      Class_Present                => Class_Present (Aspect));
 
                   --  We don't have to play the delay game here, since the only
                   --  values are check names which don't get analyzed anyway.
 
                   Delay_Required := False;
 
-               --  Aspect Post corresponds to pragma Postcondition with single
+               --  Aspect Pre corresponds to pragma Precondition with single
                --  argument that is the expression (we never give a message
-               --  argument. This is inserted right after the declaration,
+               --  argument). This is inserted right after the declaration,
                --  to get the required pragma placement.
 
-               when Aspect_Post =>
+               when Aspect_Pre =>
 
                   --  Construct the pragma
 
                   Aitem :=
-                    Make_Pragma (Sloc (Expr),
-                      Pragma_Argument_Associations => New_List (
-                        Relocate_Node (Expr)),
+                    Make_Pragma (Loc,
                       Pragma_Identifier            =>
-                      Make_Identifier (Sloc (Id), Name_Postcondition));
+                        Make_Identifier (Sloc (Id), Name_Precondition),
+                      Class_Present                => Class_Present (Aspect),
+                      Pragma_Argument_Associations => New_List (
+                        Make_Pragma_Argument_Association (Sloc (Expr),
+                          Chars      => Name_Check,
+                          Expression => Relocate_Node (Expr))));
 
                   --  We don't have to play the delay game here. The required
                   --  delay in this case is already implemented by the pragma.
 
                   Delay_Required := False;
 
-               --  Aspect Pre corresponds to pragma Precondition with single
+               --  Aspect Post corresponds to pragma Postcondition with single
                --  argument that is the expression (we never give a message
-               --  argument). This is inserted right after the declaration,
+               --  argument. This is inserted right after the declaration,
                --  to get the required pragma placement.
 
-               when Aspect_Pre =>
+               when Aspect_Post =>
 
                   --  Construct the pragma
 
                   Aitem :=
-                    Make_Pragma (Sloc (Expr),
-                      Pragma_Argument_Associations => New_List (
-                        Relocate_Node (Expr)),
+                    Make_Pragma (Sloc (Aspect),
                       Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Name_Precondition));
+                        Make_Identifier (Sloc (Id), Name_Postcondition),
+                      Class_Present                => Class_Present (Aspect),
+                      Pragma_Argument_Associations => New_List (
+                        Make_Pragma_Argument_Association (Sloc (Expr),
+                          Chars      => Name_Check,
+                          Expression => Relocate_Node (Expr))));
 
                   --  We don't have to play the delay game here. The required
                   --  delay in this case is already implemented by the pragma.