From patchwork Tue Oct 12 10:33:21 2010 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 67520 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) by ozlabs.org (Postfix) with SMTP id C338DB70A6 for ; Tue, 12 Oct 2010 21:33:40 +1100 (EST) Received: (qmail 18393 invoked by alias); 12 Oct 2010 10:33:37 -0000 Received: (qmail 18152 invoked by uid 22791); 12 Oct 2010 10:33:33 -0000 X-SWARE-Spam-Status: No, hits=-1.8 required=5.0 tests=AWL, BAYES_00, TW_TR, T_RP_MATCHES_RCVD X-Spam-Check-By: sourceware.org Received: from mel.act-europe.fr (HELO mel.act-europe.fr) (212.99.106.210) by sourceware.org (qpsmtpd/0.43rc1) with ESMTP; Tue, 12 Oct 2010 10:33:24 +0000 Received: from localhost (localhost [127.0.0.1]) by filtered-smtp.eu.adacore.com (Postfix) with ESMTP id 21984CB028A; Tue, 12 Oct 2010 12:33:22 +0200 (CEST) Received: from mel.act-europe.fr ([127.0.0.1]) by localhost (smtp.eu.adacore.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id lyRWMfNSlAw0; Tue, 12 Oct 2010 12:33:22 +0200 (CEST) Received: from saumur.act-europe.fr (saumur.act-europe.fr [10.10.0.183]) by mel.act-europe.fr (Postfix) with ESMTP id 0CBF0CB01EA; Tue, 12 Oct 2010 12:33:22 +0200 (CEST) Received: by saumur.act-europe.fr (Postfix, from userid 525) id E434BD9BB5; Tue, 12 Oct 2010 12:33:21 +0200 (CEST) Date: Tue, 12 Oct 2010 12:33:21 +0200 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Robert Dewar Subject: [Ada] Split PRE/POST expressions into AND THEN sections Message-ID: <20101012103321.GA1828@adacore.com> Mime-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.9i X-IsSubscribed: yes Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org 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 * 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. 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