===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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 --
------------------------------
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- 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
===================================================================
@@ -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
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.