Patchwork [Ada] Handle inherited postconditions (AI05-0145)

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

Comments

Arnaud Charlet - Oct. 12, 2010, 10:42 a.m.
This patch handles inherited postconditions for the simple inheritance
case. Interfaces are not yet handled. The following test, compiled
with -gnata -gnat12:

with Text_IO; use Text_IO;
with Ada.Exceptions; use Ada.Exceptions;
procedure PrePostI is
   function Ident (X : Integer) return Integer is
   begin
      return X;
   end;

   package Ops is
      G : Integer := Ident (13);

      type R is tagged record
         X : Integer;
      end record;

      procedure RP (Arg : in out R) with
        Post'Class => Arg.X = Arg.X'Old + 1
                        and then
                      Arg.X /= G;
   end Ops;

   package Ops2 is
      G : Integer := Ident (999);

      type RN is new Ops.R with record
         Y : Integer;
      end record;

      procedure RP (Arg : in out RN) with
        Post => Arg.Y = Incr (Arg.Y'Old)
                  and then
                Arg.Y /= 11;

      function Incr (Arg : Integer) return Integer;
   end Ops2;

   package body Ops is
      procedure RP (Arg : in out R) is
      begin
         null;
      end;
   end Ops;

   package body Ops2 is
      procedure RP (Arg : in out RN) is
      begin
         Arg.X := Arg.X + 1;
         Arg.Y := Arg.Y + 1;
      end RP;

      function Incr (Arg : Integer) return Integer is
      begin
         return Arg + 1;
      end Incr;
   end Ops2;

   use Ops, Ops2;

   V : RN;

begin
   V.X := 49;
   V.Y := 42;
   RP (V);
   Put_Line ("V.X =" & V.X'Img);
   Put_Line ("V.Y =" & V.Y'Img);

   begin
      V.X := 12;
      V.Y := 72;
      RP (V);
      Put_Line ("RP (12,72), no exception");
   exception
      when E : others =>
         Put_Line ("exception raised for RP ((12,72))): "
                   & Exception_Message (E));
   end;

   begin
      V.X := 52;
      V.Y := 10;
      RP (V);
      Put_Line ("RP (52,10), no exception");
   exception
      when E : others =>
         Put_Line ("exception raised for RP ((52,10))): "
                   & Exception_Message (E));
   end;
end PrePostI;

generates the output:

V.X = 50
V.Y = 43
exception raised for RP ((12,72))): failed inherited postcondition from line 19
exception raised for RP ((52,10))): failed postcondition from line 32

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

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

	* sem_ch6.adb (Process_PPCs): Handle inherited postconditions.

Patch

Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 165353)
+++ sem_ch6.adb	(working copy)
@@ -4636,10 +4636,12 @@  package body Sem_Ch6 is
         and then (not Is_Hidden (Overridden_Subp)
                    or else
                      ((Chars (Overridden_Subp) = Name_Initialize
-                         or else Chars (Overridden_Subp) = Name_Adjust
-                         or else Chars (Overridden_Subp) = Name_Finalize)
-                       and then Present (Alias (Overridden_Subp))
-                       and then not Is_Hidden (Alias (Overridden_Subp))))
+                         or else
+                       Chars (Overridden_Subp) = Name_Adjust
+                         or else
+                       Chars (Overridden_Subp) = Name_Finalize)
+                      and then Present (Alias (Overridden_Subp))
+                      and then not Is_Hidden (Alias (Overridden_Subp))))
       then
          if Must_Not_Override (Spec) then
             Error_Msg_Sloc := Sloc (Overridden_Subp);
@@ -8584,25 +8586,58 @@  package body Sem_Ch6 is
       Body_Id : Entity_Id)
    is
       Loc   : constant Source_Ptr := Sloc (N);
+      Plist : List_Id             := No_List;
       Prag  : Node_Id;
-      Plist : List_Id := No_List;
       Subp  : Entity_Id;
       Parms : List_Id;
 
-      function Grab_PPC (Nam : Name_Id) return Node_Id;
-      --  Prag contains an analyzed precondition or postcondition pragma.
-      --  This function copies the pragma, changes it to the corresponding
-      --  Check pragma and returns the Check pragma as the result. The
-      --  argument Nam is either Name_Precondition or Name_Postcondition.
+      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
+      --  pragma and returns the Check pragma as the result. If Pspec is non-
+      --  empty, this is the case of inheriting a PPC, where we must change
+      --  references to parameters of the inherited subprogram to point to the
+      --  corresponding parameters of the current subprogram.
 
       --------------
       -- Grab_PPC --
       --------------
 
-      function Grab_PPC (Nam : Name_Id) return Node_Id is
-         CP : constant Node_Id := New_Copy_Tree (Prag);
+      function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id is
+         Nam : constant Name_Id := Pragma_Name (Prag);
+         Map : Elist_Id;
+         CP  : Node_Id;
 
       begin
+         --  Prepare map if this is the case where we have to map entities of
+         --  arguments in the overridden subprogram to corresponding entities
+         --  of the current subprogram.
+
+         if No (Pspec) then
+            Map := No_Elist;
+
+         else
+            declare
+               PF : Entity_Id;
+               CF : Entity_Id;
+
+            begin
+               Map := New_Elmt_List;
+               PF := First_Formal (Pspec);
+               CF := First_Formal (Spec_Id);
+               while Present (PF) loop
+                  Append_Elmt (PF, Map);
+                  Append_Elmt (CF, Map);
+                  Next_Formal (PF);
+                  Next_Formal (CF);
+               end loop;
+            end;
+         end if;
+
+         --  Now we can copy the tree, doing any required substituations
+
+         CP := New_Copy_Tree (Prag, Map => Map, New_Scope => Current_Scope);
+
          --  Set Analyzed to false, since we want to reanalyze the check
          --  procedure. Note that it is only at the outer level that we
          --  do this fiddling, for the spec cases, the already preanalyzed
@@ -8630,6 +8665,23 @@  package body Sem_Ch6 is
            Make_Identifier (Sloc (Prag),
              Chars => Name_Check));
 
+         --  If this is inherited case then the current message starts with
+         --  "failed p" and we change this to "failed inherited p".
+
+         if Present (Pspec) then
+            String_To_Name_Buffer
+              (Strval (Expression (Last (Pragma_Argument_Associations (CP)))));
+            pragma Assert (Name_Buffer (1 .. 8) = "failed p");
+            Name_Len := Name_Len + 10;
+            Name_Buffer (17 .. Name_Len) := Name_Buffer (7 .. Name_Len - 10);
+            Name_Buffer (7 .. 16) := " inherited";
+            Set_Strval
+              (Expression (Last (Pragma_Argument_Associations (CP))),
+               String_From_Name_Buffer);
+         end if;
+
+         --  Return the check pragma
+
          return CP;
       end Grab_PPC;
 
@@ -8660,7 +8712,7 @@  package body Sem_Ch6 is
                --  which is what we want since new entries were chained to
                --  the head of the list.
 
-               Prepend (Grab_PPC (Name_Precondition), Declarations (N));
+               Prepend (Grab_PPC, Declarations (N));
             end if;
 
             Prag := Next_Pragma (Prag);
@@ -8698,13 +8750,13 @@  package body Sem_Ch6 is
 
                   Analyze (Prag);
 
-                  --  If expansion is disabled, as in a generic unit,
-                  --  save pragma for later expansion.
+                  --  If expansion is disabled, as in a generic unit, save
+                  --  pragma for later expansion.
 
                   if not Expander_Active then
-                     Prepend (Grab_PPC (Name_Postcondition), Declarations (N));
+                     Prepend (Grab_PPC, Declarations (N));
                   else
-                     Append (Grab_PPC (Name_Postcondition), Plist);
+                     Append (Grab_PPC, Plist);
                   end if;
                end if;
 
@@ -8726,27 +8778,78 @@  package body Sem_Ch6 is
       --  Now deal with any postconditions from the spec
 
       if Present (Spec_Id) then
+         declare
+            Parent_Op : Node_Id;
 
-         --  Loop through PPC pragmas from spec
-
-         Prag := Spec_PPC_List (Spec_Id);
-         while Present (Prag) loop
-            if Pragma_Name (Prag) = Name_Postcondition
-              and then Pragma_Enabled (Prag)
-            then
-               if Plist = No_List then
-                  Plist := Empty_List;
-               end if;
+            procedure Process_Post_Conditions
+              (Spec  : Node_Id;
+               Class : Boolean);
+            --  This processes the Spec_PPC_List from Spec, processing any
+            --  postconditions from the list. If Class is True, then only
+            --  postconditions marked with Class_Present are considered.
+            --  The caller has checked that Spec_PPC_List is non-Empty.
+
+            -----------------------------
+            -- Process_Post_Conditions --
+            -----------------------------
+
+            procedure Process_Post_Conditions
+              (Spec  : Node_Id;
+               Class : Boolean)
+            is
+               Pspec : Node_Id;
 
-               if not Expander_Active then
-                  Prepend (Grab_PPC (Name_Postcondition), Declarations (N));
+            begin
+               if Class then
+                  Pspec := Spec;
                else
-                  Append (Grab_PPC (Name_Postcondition), Plist);
+                  Pspec := Empty;
                end if;
+
+               --  Loop through PPC pragmas from spec
+
+               Prag := Spec_PPC_List (Spec);
+               loop
+                  if Pragma_Name (Prag) = Name_Postcondition
+                    and then Pragma_Enabled (Prag)
+                    and then (not Class or else Class_Present (Prag))
+                  then
+                     if Plist = No_List then
+                        Plist := Empty_List;
+                     end if;
+
+                     if not Expander_Active then
+                        Prepend
+                          (Grab_PPC (Pspec), Declarations (N));
+                     else
+                        Append (Grab_PPC (Pspec), Plist);
+                     end if;
+                  end if;
+
+                  Prag := Next_Pragma (Prag);
+                  exit when No (Prag);
+               end loop;
+            end Process_Post_Conditions;
+
+         begin
+            if Present (Spec_PPC_List (Spec_Id)) then
+               Process_Post_Conditions (Spec_Id, Class => False);
             end if;
 
-            Prag := Next_Pragma (Prag);
-         end loop;
+            --  Process directly inherited specifications
+
+            Parent_Op := Spec_Id;
+            loop
+               Parent_Op := Overridden_Operation (Parent_Op);
+               exit when No (Parent_Op);
+
+               if Ekind (Parent_Op) /= E_Enumeration_Literal
+                 and then Present (Spec_PPC_List (Parent_Op))
+               then
+                  Process_Post_Conditions (Parent_Op, Class => True);
+               end if;
+            end loop;
+         end;
       end if;
 
       --  If we had any postconditions and expansion is enabled, build
@@ -8773,6 +8876,7 @@  package body Sem_Ch6 is
                    Make_Defining_Identifier (Loc,
                      Chars => Name_uPostconditions);
             --  The entity for the _Postconditions procedure
+
          begin
             Prepend_To (Declarations (N),
               Make_Subprogram_Body (Loc,