From patchwork Tue Oct 12 12:23:45 2010 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 67547 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 48CB4B70A5 for ; Tue, 12 Oct 2010 23:24:04 +1100 (EST) Received: (qmail 27985 invoked by alias); 12 Oct 2010 12:23:59 -0000 Received: (qmail 27969 invoked by uid 22791); 12 Oct 2010 12:23:57 -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 12:23:48 +0000 Received: from localhost (localhost [127.0.0.1]) by filtered-smtp.eu.adacore.com (Postfix) with ESMTP id 35E98CB028D; Tue, 12 Oct 2010 14:23:46 +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 bjMiDkvYu3U4; Tue, 12 Oct 2010 14:23:46 +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 2172FCB028B; Tue, 12 Oct 2010 14:23:46 +0200 (CEST) Received: by saumur.act-europe.fr (Postfix, from userid 525) id F2FB8D9BB5; Tue, 12 Oct 2010 14:23:45 +0200 (CEST) Date: Tue, 12 Oct 2010 14:23:45 +0200 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Robert Dewar Subject: [Ada] Final fix to inheriting of Pre'Class preconditions Message-ID: <20101012122345.GA17318@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 With this patch, the inheritance of Pre'Class preconditions with the resulting composite condition formed by linking the inherited expressions with OR ELSE is working. Still to do a) deal with visibility issue, GNAT currently only delays pre/post analysis in the package case, the RM does it in all declarative units. b) deal with interfaces c) deal with entries Here is the latest status of the test programs Testing for errors: (compiled with -gnata12 -gnatld7 -gnatj60) 1. package Preposterr is 2. procedure P0 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 P1 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 P2 with 11. Pre => True, 12. Post => False; 13. pragma Precondition (True); 14. pragma Postcondition (False); 15. 16. procedure P3 with 17. Pre'Class => True, 18. Post'Class => False; 19. pragma Precondition (True); | >>> pragma "Precondition" not allowed, "Pre'Class" aspect given at line 17 20. pragma Postcondition (False); 21. 22. procedure P4 with 23. Pre => True, 24. Pre'Class => True; | >>> aspect "Pre'Class" for "P4" is not allowed here, since aspect "Pre" previously given at line 23 25. 26. procedure P5 with 27. Pre'Class => True, 28. Pre => True; | >>> aspect "Pre" for "P5" is not allowed here, since aspect "Pre'Class" previously given at line 27 29. 30. procedure P6 with 31. Pre => True, 32. Pre => True; | >>> aspect "Pre" for "P6" previously given at line 31 33. 34. procedure P7 with 35. Pre'Class => True, 36. Pre'Class => True; | >>> aspect "Pre'Class" for "P7" previously given at line 35 37. 38. procedure P8 with 39. Post => True, 40. Post'Class => True; 41. 42. procedure P9 with 43. Post'Class => True, 44. Post => True; 45. 46. procedure P10 with 47. Post => True, 48. Post => True; | >>> aspect "Post" for "P10" previously given at line 47 49. 50. procedure P11 with 51. Post'Class => True, 52. Post'Class => True; | >>> aspect "Post'Class" for "P11" previously given at line 51 53. 54. type T is tagged null record; 55. procedure PT (Arg : T) with 56. Pre'Class => True; 57. 58. type NT is new T with null record; 59. procedure PT (Arg : NT) with | >>> info: "PT" inherits "Pre'Class" aspect from line 56 60. Pre => True; | >>> aspect "Pre" not allowed, "Pre'Class" aspect inherited from line 56 61. end Preposterr; Testing non-inherited pre/postconditions compiled with -gnata12 -gnatld7 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 => 6. X > 11 7. and then 8. X mod 2 = 1, 9. Post => 10. F'Result = X + 1 11. and then 12. F'Result /= 18; 13. 14. function F (X : Integer) return Integer is 15. begin 16. if X = 13 then 17. return X; 18. else 19. return X + 1; 20. end if; 21. end F; 22. 23. 24. begin 25. Put_Line (F (31)'Img); 26. 27. begin 28. Put_Line (F (13)'Img); 29. exception 30. when E : others => 31. Put_Line ("exception for F (13): " 32. & Exception_Message (E)); 33. end; 34. 35. begin 36. Put_Line (F (12)'Img); 37. exception 38. when E : others => 39. Put_Line ("exception for F (12): " 40. & Exception_Message (E)); 41. end; 42. 43. begin 44. Put_Line (F (11)'Img); 45. exception 46. when E : others => 47. Put_Line ("exception for F (11): " 48. & Exception_Message (E)); 49. end; 50. 51. begin 52. Put_Line (F (17)'Img); 53. exception 54. when E : others => 55. Put_Line ("exception for F (17): " 56. & Exception_Message (E)); 57. end; 58. end prepost; The output is: 32 exception for F (13): failed postcondition from prepost.adb:10 exception for F (12): failed precondition from prepost.adb:8 exception for F (11): failed precondition from prepost.adb:6 exception for F (17): failed postcondition from prepost.adb:12 If gnat.adc contains pragma Suppress_Exception_Locations, then the output is: 32 exception for F (13): exception for F (12): exception for F (11): exception for F (17): Testing for inherited pre/post conditions: (compiled with -gnata12-gnatld7) 1. with Text_IO; use Text_IO; 2. with Ada.Exceptions; use Ada.Exceptions; 3. procedure PrePostI is 4. function Ident (X : Integer) return Integer is 5. begin 6. return X; 7. end; 8. 9. package Ops is 10. G : Integer := Ident (13); 11. 12. type R is tagged record 13. X : Integer; 14. end record; 15. 16. procedure RP (Arg : in out R) with 17. Post'Class => 18. Arg.X = Arg.X'Old + 1 19. and then 20. Arg.X /= G, 21. Pre'Class => 22. Arg.X = 99 or else Arg.X = 12; 23. end Ops; 24. 25. package Ops2 is 26. G : Integer := Ident (999); 27. 28. type RN is new Ops.R with record 29. Y : Integer; 30. end record; 31. 32. procedure RP (Arg : in out RN) with | >>> info: "RP" inherits "Post'Class" aspect from line 17 >>> info: "RP" inherits "Pre'Class" aspect from line 21 33. Post => 34. Arg.Y = Incr (Arg.Y'Old) 35. and then 36. Arg.Y /= 11, 37. Pre'Class => 38. Arg.Y = 10 39. or else 40. Arg.Y = 99 41. or else 42. Arg.Y = 77; 43. function Incr (Arg : Integer) return Integer; 44. end Ops2; 45. 46. package body Ops is 47. procedure RP (Arg : in out R) is 48. begin 49. null; 50. end; 51. end Ops; 52. 53. package body Ops2 is 54. procedure RP (Arg : in out RN) is 55. begin 56. if Arg.X /= 99 then 57. Arg.X := Arg.X + 1; 58. end if; 59. 60. if Arg.Y /= 99 then 61. Arg.Y := Arg.Y + 1; 62. end if; 63. end RP; 64. 65. function Incr (Arg : Integer) return Integer is 66. begin 67. return Arg + 1; 68. end Incr; 69. end Ops2; 70. 71. use Ops, Ops2; 72. 73. V : RN; 74. 75. begin 76. V.X := 63; 77. V.Y := 77; 78. RP (V); 79. Put_Line ("V.X =" & V.X'Img); 80. Put_Line ("V.Y =" & V.Y'Img); 81. 82. begin 83. V.X := 99; 84. V.Y := 72; 85. RP (V); 86. Put_Line ("RP (99,72), no exception"); 87. exception 88. when E : others => 89. New_Line; 90. Put_Line ("exception for RP ((99,72))):"); 91. Put_Line (" " & Exception_Message (E)); 92. end; 93. 94. begin 95. V.X := 12; 96. V.Y := 72; 97. RP (V); 98. Put_Line ("RP (12,72), no exception"); 99. exception 100. when E : others => 101. New_Line; 102. Put_Line ("exception for RP ((12,72))):"); 103. Put_Line (" " & Exception_Message (E)); 104. end; 105. 106. begin 107. V.X := 52; 108. V.Y := 10; 109. RP (V); 110. Put_Line ("RP (52,10), no exception"); 111. exception 112. when E : others => 113. New_Line; 114. Put_Line ("exception for RP ((52,10))): "); 115. Put_Line (" " & Exception_Message (E)); 116. end; 117. 118. begin 119. V.X := 23; 120. V.Y := 99; 121. RP (V); 122. Put_Line ("RP (23,99), no exception"); 123. exception 124. when E : others => 125. New_Line; 126. Put_Line ("exception for RP ((23,99))): "); 127. Put_Line (" " & Exception_Message (E)); 128. end; 129. 130. begin 131. V.X := 24; 132. V.Y := 99; 133. RP (V); 134. Put_Line ("RP (24,99), no exception"); 135. exception 136. when E : others => 137. New_Line; 138. Put_Line ("exception for RP ((24,99))): "); 139. Put_Line (" " & Exception_Message (E)); 140. end; 141. 142. begin 143. V.X := 23; 144. V.Y := 98; 145. RP (V); 146. Put_Line ("RP (23,98), no exception"); 147. exception 148. when E : others => 149. New_Line; 150. Put_Line ("exception for RP ((23,98))): "); 151. Put_Line (" " & Exception_Message (E)); 152. end; 153. end PrePostI; The output is: V.X = 64 V.Y = 78 exception for RP ((99,72))): failed inherited postcondition from preposti.adb:18 exception for RP ((12,72))): failed inherited postcondition from preposti.adb:20 exception for RP ((52,10))): failed postcondition from preposti.adb:36 exception for RP ((23,99))): failed postcondition from preposti.adb:34 exception for RP ((24,99))): failed postcondition from preposti.adb:34 exception for RP ((23,98))): failed precondition from preposti.adb:41 also failed inherited precondition from preposti.adb:22 If gnat.adc contains pragma Suppress_Exception_Locations, then the output is: V.X = 64 V.Y = 78 exception for RP ((99,72))): exception for RP ((12,72))): exception for RP ((52,10))): exception for RP ((23,99))): exception for RP ((24,99))): exception for RP ((23,98))): Tested on x86_64-pc-linux-gnu, committed on trunk 2010-10-12 Robert Dewar * sem_ch6.adb (Process_PPCs): Fix error in inheriting Pre'Class when no exception messages are generated. (Process_PPCs): Fix error in inheriting Pre'Class. Index: sem_ch6.adb =================================================================== --- sem_ch6.adb (revision 165361) +++ sem_ch6.adb (working copy) @@ -8569,7 +8569,6 @@ package body Sem_Ch6 is -- Now set the kind (mode) of each formal Param_Spec := First (T); - while Present (Param_Spec) loop Formal := Defining_Identifier (Param_Spec); Set_Formal_Mode (Formal); @@ -8791,7 +8790,7 @@ package body Sem_Ch6 is if Pragma_Name (Prag) = Name_Precondition and then Class_Present (Prag) then - Inherited_Precond := Grab_PPC; + Inherited_Precond := Grab_PPC (Inherited (J)); -- No precondition so far, so establish this as the first @@ -8838,23 +8837,27 @@ package body Sem_Ch6 is -- also failed inherited precondition from bla -- ... - declare - New_Msg : constant Node_Id := - Get_Pragma_Arg - (Last - (Pragma_Argument_Associations - (Inherited_Precond))); - Old_Msg : constant Node_Id := - Get_Pragma_Arg - (Last - (Pragma_Argument_Associations - (Precond))); - begin - Start_String (Strval (Old_Msg)); - Store_String_Chars (ASCII.LF & " also "); - Store_String_Chars (Strval (New_Msg)); - Set_Strval (Old_Msg, End_String); - end; + -- Skip this if exception locations are suppressed + + if not Exception_Locations_Suppressed then + declare + New_Msg : constant Node_Id := + Get_Pragma_Arg + (Last + (Pragma_Argument_Associations + (Inherited_Precond))); + Old_Msg : constant Node_Id := + Get_Pragma_Arg + (Last + (Pragma_Argument_Associations + (Precond))); + begin + Start_String (Strval (Old_Msg)); + Store_String_Chars (ASCII.LF & " also "); + Store_String_Chars (Strval (New_Msg)); + Set_Strval (Old_Msg, End_String); + end; + end if; end if; end if;