Patchwork [Ada] Split PRE/POST expressions into AND THEN sections

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

Comments

Arnaud Charlet - Oct. 12, 2010, 10:33 a.m.
If a Pre or Post expression has AND THEN operations at the outer
level, the expression is split into sections, generating multiple
precondition/postcondition pragmas, and exception messages point
to the relevant part of the original expression, as shown in this
example, compiled with -gnat12 -gnata

     1. with Text_IO; use Text_IO;
     2. with Ada.Exceptions; use Ada.Exceptions;
     3. procedure prepost is
     4.    function F (X : Integer) return Integer with
     5.    Pre  => X > 11
     6.              and then
     7.            X mod 2 = 1,
     8.    Post => F'Result = X + 1
     9.              and then
    10.            F'Result /= 18;
    11.
    12.    function F (X : Integer) return Integer is
    13.    begin
    14.       if X = 13 then
    15.          return X;
    16.       else
    17.          return X + 1;
    18.       end if;
    19.    end F;
    20.
    21.
    22. begin
    23.    Put_Line (F (31)'Img);
    24.
    25.    begin
    26.       Put_Line (F (13)'Img);
    27.    exception
    28.       when E : others =>
    29.          Put_Line ("exception raised for F (13): "
    30.                    & Exception_Message (E));
    31.    end;
    32.
    33.    begin
    34.       Put_Line (F (12)'Img);
    35.    exception
    36.       when E : others =>
    37.          Put_Line ("exception raised for F (12): "
    38.                    & Exception_Message (E));
    39.    end;
    40.
    41.    begin
    42.       Put_Line (F (11)'Img);
    43.    exception
    44.       when E : others =>
    45.          Put_Line ("exception raised for F (11): "
    46.                    & Exception_Message (E));
    47.    end;
    48.
    49.    begin
    50.       Put_Line (F (17)'Img);
    51.    exception
    52.       when E : others =>
    53.          Put_Line ("exception raised for F (17): "
    54.                    & Exception_Message (E));
    55.    end;
    56. end prepost;

The output when this program is executed is:

 32
exception raised for F (13): failed postcondition from line 8
exception raised for F (12): failed precondition from line 7
exception raised for F (11): failed precondition from line 5
exception raised for F (17): failed postcondition from line 10

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

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

	* sem_ch13.adb (Analyze_Aspect_Specifications): For Pre/Post, break
	apart expressions with AND THEN clauses into separate pragmas.
	* sinput.ads, sinput.adab (Get_Logical_Line_Number_Img): New function.

Patch

Index: sinput.adb
===================================================================
--- sinput.adb	(revision 165316)
+++ sinput.adb	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2009, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2010, 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- --
@@ -227,8 +227,7 @@  package body Sinput is
          Get_Name_String_And_Append
            (Reference_Name (Get_Source_File_Index (Ptr)));
          Add_Char_To_Name_Buffer (':');
-         Add_Nat_To_Name_Buffer
-           (Nat (Get_Logical_Line_Number (Ptr)));
+         Add_Nat_To_Name_Buffer (Nat (Get_Logical_Line_Number (Ptr)));
 
          Ptr := Instantiation_Location (Ptr);
          exit when Ptr = No_Location;
@@ -299,6 +298,19 @@  package body Sinput is
       end if;
    end Get_Logical_Line_Number;
 
+   ---------------------------------
+   -- Get_Logical_Line_Number_Img --
+   ---------------------------------
+
+   function Get_Logical_Line_Number_Img
+     (P : Source_Ptr) return String
+   is
+   begin
+      Name_Len := 0;
+      Add_Nat_To_Name_Buffer (Nat (Get_Logical_Line_Number (P)));
+      return Name_Buffer (1 .. Name_Len);
+   end Get_Logical_Line_Number_Img;
+
    ------------------------------
    -- Get_Physical_Line_Number --
    ------------------------------
Index: sinput.ads
===================================================================
--- sinput.ads	(revision 165316)
+++ sinput.ads	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2009, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2010, 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- --
@@ -487,6 +487,11 @@  package Sinput is
    --  reference pragmas have been encountered, the value returned is
    --  the same as the physical line number.
 
+   function Get_Logical_Line_Number_Img
+     (P : Source_Ptr) return String;
+   --  Same as above function, but returns the line number as a string of
+   --  decimal digits, with no leading space. Destroys Name_Buffer.
+
    function Get_Physical_Line_Number
      (P : Source_Ptr) return Physical_Line_Number;
    --  The line number of the specified source position is obtained by
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 165355)
+++ sem_ch13.adb	(working copy)
@@ -50,6 +50,7 @@  with Sem_Res;  use Sem_Res;
 with Sem_Type; use Sem_Type;
 with Sem_Util; use Sem_Util;
 with Sem_Warn; use Sem_Warn;
+with Sinput;   use Sinput;
 with Snames;   use Snames;
 with Stand;    use Stand;
 with Sinfo;    use Sinfo;
@@ -81,10 +82,10 @@  package body Sem_Ch13 is
    --  posted as required, and a value of No_Uint is returned.
 
    function Is_Operational_Item (N : Node_Id) return Boolean;
-   --  A specification for a stream attribute is allowed before the full
-   --  type is declared, as explained in AI-00137 and the corrigendum.
-   --  Attributes that do not specify a representation characteristic are
-   --  operational attributes.
+   --  A specification for a stream attribute is allowed before the full type
+   --  is declared, as explained in AI-00137 and the corrigendum. Attributes
+   --  that do not specify a representation characteristic are operational
+   --  attributes.
 
    procedure New_Stream_Subprogram
      (N    : Node_Id;
@@ -666,6 +667,7 @@  package body Sem_Ch13 is
             Loc  : constant Source_Ptr := Sloc (Aspect);
             Id   : constant Node_Id    := Identifier (Aspect);
             Expr : constant Node_Id    := Expression (Aspect);
+            Eloc :          Source_Ptr := Sloc (Expr);
             Nam  : constant Name_Id    := Chars (Id);
             A_Id : constant Aspect_Id  := Get_Aspect_Id (Nam);
             Anod : Node_Id;
@@ -675,11 +677,15 @@  package body Sem_Ch13 is
             Set_Entity (Aspect, E);
             Ent := New_Occurrence_Of (E, Sloc (Id));
 
-            --  Check for duplicate aspect
+            --  Check for duplicate aspect. Note that the Comes_From_Source
+            --  test allows duplicate Pre/Post's that we generate internally
+            --  to escape being flagged here.
 
             Anod := First (L);
             while Anod /= Aspect loop
-               if Nam = Chars (Identifier (Anod)) then
+               if Nam = Chars (Identifier (Anod))
+                 and then Comes_From_Source (Aspect)
+               then
                   Error_Msg_Name_1 := Nam;
                   Error_Msg_Sloc := Sloc (Anod);
                   Error_Msg_NE
@@ -826,7 +832,7 @@  package body Sem_Ch13 is
                   Aitem :=
                     Make_Pragma (Loc,
                       Pragma_Argument_Associations => New_List (
-                        New_Occurrence_Of (E, Sloc (Expr)),
+                        New_Occurrence_Of (E, Eloc),
                         Relocate_Node (Expr)),
                       Pragma_Identifier            =>
                       Make_Identifier (Sloc (Id), Chars (Id)));
@@ -848,7 +854,7 @@  package body Sem_Ch13 is
                     Make_Pragma (Loc,
                       Pragma_Argument_Associations => New_List (
                         Relocate_Node (Expr),
-                        New_Occurrence_Of (E, Sloc (Expr))),
+                        New_Occurrence_Of (E, Eloc)),
                       Pragma_Identifier            =>
                         Make_Identifier (Sloc (Id), Chars (Id)),
                       Class_Present                => Class_Present (Aspect));
@@ -858,53 +864,74 @@  package body Sem_Ch13 is
 
                   Delay_Required := False;
 
-               --  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,
-               --  to get the required pragma placement.
-
-               when Aspect_Pre =>
-
-                  --  Construct the pragma
-
-                  Aitem :=
-                    Make_Pragma (Loc,
-                      Pragma_Identifier            =>
-                        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))));
+               --  Aspects Pre/Post generate Precondition/Postcondition pragmas
+               --  with a first argument that is the expression, and a second
+               --  argument that is an informative message if the test fails.
+               --  This is inserted right after the declaration, to get the
+               --  required pragma placement.
+
+               when Aspect_Pre | Aspect_Post => declare
+                  Pname : Name_Id;
+                  Msg   : Node_Id;
 
-                  --  We don't have to play the delay game here. The required
-                  --  delay in this case is already implemented by the pragma.
+               begin
+                  if A_Id = Aspect_Pre then
+                     Pname := Name_Precondition;
+                  else
+                     Pname := Name_Postcondition;
+                  end if;
 
-                  Delay_Required := False;
+                  --  If the expressions is of the form A and then B, then
+                  --  we generate separate Pre/Post aspects for the separate
+                  --  clauses. Since we allow multiple pragmas, there is no
+                  --  problem in allowing multiple Pre/Post aspects internally.
+
+                  while Nkind (Expr) = N_And_Then loop
+                     Insert_After (Aspect,
+                       Make_Aspect_Specification (Sloc (Right_Opnd (Expr)),
+                         Identifier    => Identifier (Aspect),
+                         Expression    => Relocate_Node (Right_Opnd (Expr)),
+                         Class_Present => Class_Present (Aspect)));
+                     Rewrite (Expr, Relocate_Node (Left_Opnd (Expr)));
+                     Eloc := Sloc (Expr);
+                  end loop;
 
-               --  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,
-               --  to get the required pragma placement.
+                  --  Proceed with handling what's left after this split up
 
-               when Aspect_Post =>
+                  Msg :=
+                    Make_String_Literal (Eloc,
+                      Strval => "failed "
+                                  & Get_Name_String (Pname)
+                                  & " from line "
+                                  & Get_Logical_Line_Number_Img (Eloc));
 
                   --  Construct the pragma
 
                   Aitem :=
-                    Make_Pragma (Sloc (Aspect),
+                    Make_Pragma (Loc,
                       Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Name_Postcondition),
+                        Make_Identifier (Sloc (Id),
+                          Chars => Pname),
                       Class_Present                => Class_Present (Aspect),
                       Pragma_Argument_Associations => New_List (
-                        Make_Pragma_Argument_Association (Sloc (Expr),
+                        Make_Pragma_Argument_Association (Eloc,
                           Chars      => Name_Check,
-                          Expression => Relocate_Node (Expr))));
+                          Expression => Relocate_Node (Expr)),
+                        Make_Pragma_Argument_Association (Eloc,
+                          Chars      => Name_Message,
+                          Expression => Msg)));
+
+                  Set_From_Aspect_Specification (Aitem, True);
+
+                  --  For Pre/Post cases, insert immediately after the entity
+                  --  declaration, since that is the required pragma placement.
+                  --  Note that for these aspects, we do not have to worry
+                  --  about delay issues, since the pragmas themselves deal
+                  --  with delay of visibility for the expression analysis.
 
-                  --  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;
+                  Insert_After (N, Aitem);
+                  goto Continue;
+               end;
 
                --  Aspects currently unimplemented