===================================================================
@@ -23,6 +23,7 @@
-- --
------------------------------------------------------------------------------
+with Aspects; use Aspects;
with Atree; use Atree;
with Debug; use Debug;
with Errout; use Errout;
@@ -125,13 +126,13 @@
-- Calls above procedure for each element of the list L
procedure Set_Table_Entry
- (C1 : Character;
- C2 : Character;
- From : Source_Ptr;
- To : Source_Ptr;
- Last : Boolean;
- Pragma_Sloc : Source_Ptr := No_Location;
- Pragma_Name : Pragma_Id := Unknown_Pragma);
+ (C1 : Character;
+ C2 : Character;
+ From : Source_Ptr;
+ To : Source_Ptr;
+ Last : Boolean;
+ Pragma_Sloc : Source_Ptr := No_Location;
+ Pragma_Aspect_Name : Name_Id := No_Name);
-- Append an entry to SCO_Table with fields set as per arguments
type Dominant_Info is record
@@ -487,15 +488,22 @@
Loc : Source_Ptr := No_Location;
-- Node whose Sloc is used for the decision
+ Nam : Name_Id := No_Name;
+ -- For the case of an aspect, aspect name
+
begin
case T is
- when 'I' | 'E' | 'W' =>
+ when 'I' | 'E' | 'W' | 'a' =>
- -- For IF, EXIT, WHILE, the token SLOC can be found from
- -- the SLOC of the parent of the expression.
+ -- For IF, EXIT, WHILE, or aspects, the token SLOC is that of
+ -- the parent of the expression.
Loc := Sloc (Parent (N));
+ if T = 'a' then
+ Nam := Chars (Identifier (Parent (N)));
+ end if;
+
when 'G' | 'P' =>
-- For entry guard, the token sloc is from the N_Entry_Body.
@@ -533,12 +541,20 @@
end case;
Set_Table_Entry
- (C1 => T,
- C2 => ' ',
- From => Loc,
- To => No_Location,
- Last => False,
- Pragma_Sloc => Pragma_Sloc);
+ (C1 => T,
+ C2 => ' ',
+ From => Loc,
+ To => No_Location,
+ Last => False,
+ Pragma_Sloc => Pragma_Sloc,
+ Pragma_Aspect_Name => Nam);
+
+ -- For an aspect specification, which will be rewritten into a
+ -- pragma, enter a hash table entry now.
+
+ if T = 'a' then
+ Condition_Pragma_Hash_Table.Set (Loc, SCO_Table.Last);
+ end if;
end Output_Header;
------------------------------
@@ -731,6 +747,8 @@
procedure Populate_SCO_Instance_Table is
new Sinput.Iterate_On_Instances (Record_Instance);
+ SCO_Index : Nat;
+
begin
if Debug_Flag_Dot_OO then
dsco;
@@ -796,6 +814,24 @@
end;
end loop;
+ -- Stamp out SCO entries for decisions in disabled constructs (pragmas
+ -- or aspects).
+
+ SCO_Index := 1;
+ while SCO_Index <= SCO_Table.Last loop
+ if Is_Decision (SCO_Table.Table (SCO_Index).C1)
+ and then SCO_Pragma_Disabled
+ (SCO_Table.Table (SCO_Index).Pragma_Sloc)
+ then
+ loop
+ SCO_Table.Table (SCO_Index).C1 := ASCII.NUL;
+ exit when SCO_Table.Table (SCO_Index).Last;
+ SCO_Index := SCO_Index + 1;
+ end loop;
+ end if;
+ SCO_Index := SCO_Index + 1;
+ end loop;
+
-- Now the tables are all setup for output to the ALI file
Write_SCOs_To_ALI_File;
@@ -824,8 +860,30 @@
declare
T : SCO_Table_Entry renames SCO_Table.Table (Index);
begin
- pragma Assert (T.C1 = 'S');
- return T.C2 = 'p';
+ case T.C1 is
+ when 'S' =>
+ -- Pragma statement
+
+ return T.C2 = 'p';
+
+ when 'A' =>
+ -- Aspect decision (enabled)
+
+ return False;
+
+ when 'a' =>
+ -- Aspect decision (not enabled)
+
+ return True;
+
+ when ASCII.NUL =>
+ -- Nullified disabled SCO
+
+ return True;
+
+ when others =>
+ raise Program_Error;
+ end case;
end;
else
@@ -976,13 +1034,28 @@
T : SCO_Table_Entry renames SCO_Table.Table (Index);
begin
- -- Called multiple times for the same sloc (need to allow for
- -- C2 = 'P') ???
+ -- Note: may be called multiple times for the same sloc, so
+ -- account for the fact that the entry may already have been
+ -- marked enabled.
- pragma Assert (T.C1 = 'S'
- and then
- (T.C2 = 'p' or else T.C2 = 'P'));
- T.C2 := 'P';
+ case T.C1 is
+ -- Aspect (decision SCO)
+
+ when 'a' =>
+ T.C1 := 'A';
+
+ when 'A' =>
+ null;
+
+ -- Pragma (statement SCO)
+
+ when 'S' =>
+ pragma Assert (T.C2 = 'p' or else T.C2 = 'P');
+ T.C2 := 'P';
+
+ when others =>
+ raise Program_Error;
+ end case;
end;
end if;
end Set_SCO_Pragma_Enabled;
@@ -992,23 +1065,23 @@
---------------------
procedure Set_Table_Entry
- (C1 : Character;
- C2 : Character;
- From : Source_Ptr;
- To : Source_Ptr;
- Last : Boolean;
- Pragma_Sloc : Source_Ptr := No_Location;
- Pragma_Name : Pragma_Id := Unknown_Pragma)
+ (C1 : Character;
+ C2 : Character;
+ From : Source_Ptr;
+ To : Source_Ptr;
+ Last : Boolean;
+ Pragma_Sloc : Source_Ptr := No_Location;
+ Pragma_Aspect_Name : Name_Id := No_Name)
is
begin
SCO_Table.Append
- ((C1 => C1,
- C2 => C2,
- From => To_Source_Location (From),
- To => To_Source_Location (To),
- Last => Last,
- Pragma_Sloc => Pragma_Sloc,
- Pragma_Name => Pragma_Name));
+ ((C1 => C1,
+ C2 => C2,
+ From => To_Source_Location (From),
+ To => To_Source_Location (To),
+ Last => Last,
+ Pragma_Sloc => Pragma_Sloc,
+ Pragma_Aspect_Name => Pragma_Aspect_Name));
end Set_Table_Entry;
------------------------
@@ -1133,6 +1206,9 @@
procedure Traverse_One (N : Node_Id);
-- Traverse one declaration or statement
+ procedure Traverse_Aspects (N : Node_Id);
+ -- Helper for Traverse_One: traverse N's aspect specifications
+
-------------------------
-- Set_Statement_Entry --
-------------------------
@@ -1156,21 +1232,21 @@
To := No_Location;
end if;
Set_Table_Entry
- (C1 => '>',
- C2 => Current_Dominant.K,
- From => From,
- To => To,
- Last => False,
- Pragma_Sloc => No_Location,
- Pragma_Name => Unknown_Pragma);
+ (C1 => '>',
+ C2 => Current_Dominant.K,
+ From => From,
+ To => To,
+ Last => False,
+ Pragma_Sloc => No_Location,
+ Pragma_Aspect_Name => No_Name);
end;
end if;
end if;
declare
- SCE : SC_Entry renames SC.Table (J);
- Pragma_Sloc : Source_Ptr := No_Location;
- Pragma_Name : Pragma_Id := Unknown_Pragma;
+ SCE : SC_Entry renames SC.Table (J);
+ Pragma_Sloc : Source_Ptr := No_Location;
+ Pragma_Aspect_Name : Name_Id := No_Name;
begin
-- For the case of a statement SCO for a pragma controlled by
-- Set_SCO_Pragma_Enabled, set Pragma_Sloc so that the SCO (and
@@ -1181,20 +1257,22 @@
Pragma_Sloc := SCE.From;
Condition_Pragma_Hash_Table.Set
(Pragma_Sloc, SCO_Table.Last + 1);
- Pragma_Name := Get_Pragma_Id (Sinfo.Pragma_Name (SCE.N));
+ Pragma_Aspect_Name := Pragma_Name (SCE.N);
+ pragma Assert (Pragma_Aspect_Name /= No_Name);
elsif SCE.Typ = 'P' then
- Pragma_Name := Get_Pragma_Id (Sinfo.Pragma_Name (SCE.N));
+ Pragma_Aspect_Name := Pragma_Name (SCE.N);
+ pragma Assert (Pragma_Aspect_Name /= No_Name);
end if;
Set_Table_Entry
- (C1 => 'S',
- C2 => SCE.Typ,
- From => SCE.From,
- To => SCE.To,
- Last => (J = SC_Last),
- Pragma_Sloc => Pragma_Sloc,
- Pragma_Name => Pragma_Name);
+ (C1 => 'S',
+ C2 => SCE.Typ,
+ From => SCE.From,
+ To => SCE.To,
+ Last => (J = SC_Last),
+ Pragma_Sloc => Pragma_Sloc,
+ Pragma_Aspect_Name => Pragma_Aspect_Name);
end;
end loop;
@@ -1293,6 +1371,76 @@
SD.Append ((Empty, L, T, Current_Pragma_Sloc));
end Process_Decisions_Defer;
+ ----------------------
+ -- Traverse_Aspects --
+ ----------------------
+
+ procedure Traverse_Aspects (N : Node_Id) is
+ AN : Node_Id;
+ AE : Node_Id;
+
+ begin
+ AN := First (Aspect_Specifications (N));
+ while Present (AN) loop
+ AE := Expression (AN);
+
+ case Get_Aspect_Id (Chars (Identifier (AN))) is
+
+ -- Aspects rewritten into pragmas controlled by a Check_Policy:
+ -- Current_Pragma_Sloc must be set to the sloc of the aspect
+ -- specification. The corresponding pragma will have the same
+ -- sloc.
+
+ when Aspect_Pre |
+ Aspect_Precondition |
+ Aspect_Post |
+ Aspect_Postcondition =>
+
+ -- SCOs are generated before semantic analysis/expansion:
+ -- PPCs are not split yet.
+
+ pragma Assert (not Split_PPC (AN));
+
+ -- A Pre/Post aspect will be rewritten into a pragma
+ -- Precondition/Postcondition with the same sloc.
+
+ pragma Assert (Current_Pragma_Sloc = No_Location);
+
+ Current_Pragma_Sloc := Sloc (AN);
+
+ -- Create the decision as potentially disabled aspect ('a').
+ -- Set_SCO_Pragma_Enabled will subsequently switch to 'A'.
+
+ Process_Decisions_Defer (AE, 'a');
+ Current_Pragma_Sloc := No_Location;
+
+ -- Aspects whose checks are generated in client units,
+ -- regardless of whether or not the check is activated in the
+ -- unit which contains the declaration.
+
+ when Aspect_Predicate |
+ Aspect_Static_Predicate |
+ Aspect_Dynamic_Predicate |
+ Aspect_Invariant |
+ Aspect_Type_Invariant =>
+
+ Process_Decisions_Defer (AE, 'A');
+
+ -- Other aspects: just process any decision nested in the
+ -- aspect expression.
+
+ when others =>
+
+ if Has_Decision (AE) then
+ Process_Decisions_Defer (AE, 'X');
+ end if;
+
+ end case;
+
+ Next (AN);
+ end loop;
+ end Traverse_Aspects;
+
------------------
-- Traverse_One --
------------------
@@ -1825,6 +1973,9 @@
end if;
end case;
+ -- Process aspects if present
+
+ Traverse_Aspects (N);
end Traverse_One;
-- Start of processing for Traverse_Declarations_Or_Statements
===================================================================
@@ -28,12 +28,9 @@
-- the ALI file, and by Get_SCO/Put_SCO to read and write the text form that
-- is used in the ALI file.
-with Snames; use Snames;
+with Namet; use Namet;
+with Types; use Types;
-with Types; use Types;
-
with GNAT.Table;
package SCOs is
@@ -248,18 +245,21 @@
-- C* sloc expression
- -- Here * is one of the following characters:
+ -- Here * is one of the following:
- -- E decision in EXIT WHEN statement
- -- G decision in entry guard
- -- I decision in IF statement or if expression
- -- P decision in pragma Assert/Check/Pre_Condition/Post_Condition
- -- W decision in WHILE iteration scheme
- -- X decision appearing in some other expression context
+ -- E decision in EXIT WHEN statement
+ -- G decision in entry guard
+ -- I decision in IF statement or if expression
+ -- P decision in pragma Assert / Check / Pre/Post_Condition
+ -- A[name] decision in aspect Pre/Post (aspect name optional)
+ -- W decision in WHILE iteration scheme
+ -- X decision in some other expression context
-- For E, G, I, P, W, sloc is the source location of the EXIT, ENTRY, IF,
-- PRAGMA or WHILE token, respectively
+ -- For A sloc is the source location of the aspect identifier
+
-- For X, sloc is omitted
-- The expression is a prefix polish form indicating the structure of
@@ -369,10 +369,12 @@
Pragma_Sloc : Source_Ptr := No_Location;
-- For the statement SCO for a pragma, or for any expression SCO nested
-- in a pragma Debug/Assert/PPC, location of PRAGMA token (used for
- -- control of SCO output, value not recorded in ALI file).
+ -- control of SCO output, value not recorded in ALI file). For the
+ -- decision SCO for an aspect, or for any expression SCO nested in an
+ -- aspect, location of aspect identifier token (likewise).
- Pragma_Name : Pragma_Id := Unknown_Pragma;
- -- For the statement SCO for a pragma, gives the pragma name
+ Pragma_Aspect_Name : Name_Id := No_Name;
+ -- For the SCO for a pragma/aspect, gives the pragma/apsect name
end record;
package SCO_Table is new GNAT.Table (
@@ -382,6 +384,11 @@
Table_Initial => 500,
Table_Increment => 300);
+ Is_Decision : constant array (Character) of Boolean :=
+ ('E' | 'G' | 'I' | 'P' | 'A' | 'W' | 'X' => True,
+ others => False);
+ -- Indicates which C1 values correspond to decisions
+
-- The SCO_Table_Entry values appear as follows:
-- Statements
@@ -432,8 +439,21 @@
-- SCO contexts, the only pragmas with decisions are Assert, Check,
-- dyadic Debug, Precondition and Postcondition). These entries will
-- be omitted in output if the pragma is disabled (see comments for
- -- statement entries).
+ -- statement entries). This is achieved by setting C1 to NUL for all
+ -- SCO entries of the decision.
+ -- Decision (ASPECT)
+ -- C1 = 'A'
+ -- C2 = ' '
+ -- From = aspect identifier
+ -- To = No_Source_Location
+ -- Last = unused
+
+ -- Note: when the parse tree is first scanned, we unconditionally build a
+ -- pragma decision entry for any decision in an aspect (Pre/Post/
+ -- [Type_]Invariant/[Static_|Dynamic_]Predicate). Entries for disabled
+ -- Pre/Post aspects will be omitted from output.
+
-- Decision (Expression)
-- C1 = 'X'
-- C2 = ' '
===================================================================
@@ -23,10 +23,9 @@
-- --
------------------------------------------------------------------------------
+with Namet; use Namet;
with Opt; use Opt;
-with Par_SCO; use Par_SCO;
with SCOs; use SCOs;
-with Snames; use Snames;
procedure Put_SCOs is
Current_SCO_Unit : SCO_Unit_Index := 0;
@@ -195,18 +194,10 @@
if Sent.C1 = 'S'
and then (Sent.C2 = 'P' or else Sent.C2 = 'p')
- and then Sent.Pragma_Name /= Unknown_Pragma
+ and then Sent.Pragma_Aspect_Name /= No_Name
then
- -- Strip leading "PRAGMA_"
-
- declare
- Pnam : constant String :=
- Sent.Pragma_Name'Img;
- begin
- Output_String
- (Pnam (Pnam'First + 7 .. Pnam'Last));
- Write_Info_Char (':');
- end;
+ Write_Info_Name (Sent.Pragma_Aspect_Name);
+ Write_Info_Char (':');
end if;
end if;
@@ -240,57 +231,55 @@
-- Decision
- when 'E' | 'G' | 'I' | 'P' | 'W' | 'X' =>
+ when 'E' | 'G' | 'I' | 'P' | 'W' | 'X' | 'A' =>
Start := Start + 1;
- -- For disabled pragma, or nested decision therein, skip
- -- decision output.
+ Write_SCO_Initiate (U);
+ Write_Info_Char (T.C1);
- if SCO_Pragma_Disabled (T.Pragma_Sloc) then
- while not SCO_Table.Table (Start).Last loop
- Start := Start + 1;
- end loop;
+ if T.C1 = 'A' then
+ Write_Info_Name (T.Pragma_Aspect_Name);
+ end if;
- -- For all other cases output decision line
+ if T.C1 /= 'X' then
+ Write_Info_Char (' ');
+ Output_Source_Location (T.From);
+ end if;
- else
- Write_SCO_Initiate (U);
- Write_Info_Char (T.C1);
+ -- Loop through table entries for this decision
- if T.C1 /= 'X' then
+ loop
+ declare
+ T : SCO_Table_Entry
+ renames SCO_Table.Table (Start);
+
+ begin
Write_Info_Char (' ');
- Output_Source_Location (T.From);
- end if;
- -- Loop through table entries for this decision
+ if T.C1 = '!' or else
+ T.C1 = '&' or else
+ T.C1 = '|'
+ then
+ Write_Info_Char (T.C1);
+ Output_Source_Location (T.From);
- loop
- declare
- T : SCO_Table_Entry
- renames SCO_Table.Table (Start);
+ else
+ Write_Info_Char (T.C2);
+ Output_Range (T);
+ end if;
- begin
- Write_Info_Char (' ');
+ exit when T.Last;
+ Start := Start + 1;
+ end;
+ end loop;
- if T.C1 = '!' or else
- T.C1 = '&' or else
- T.C1 = '|'
- then
- Write_Info_Char (T.C1);
- Output_Source_Location (T.From);
+ Write_Info_Terminate;
- else
- Write_Info_Char (T.C2);
- Output_Range (T);
- end if;
+ when ASCII.NUL =>
- exit when T.Last;
- Start := Start + 1;
- end;
- end loop;
+ -- Nullified entry: skip
- Write_Info_Terminate;
- end if;
+ null;
when others =>
raise Program_Error;
===================================================================
@@ -2,11 +2,11 @@
-- --
-- GNAT COMPILER COMPONENTS --
-- --
+-- P U T _ S C O S --
-- --
-- S p e c --
-- --
+-- Copyright (C) 2009-2012, 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- --
@@ -28,6 +28,7 @@
-- the ALI file. The interface allows control over the destination of the
-- output, so that this routine can also be used for debugging purposes.
+with Namet; use Namet;
with Types; use Types;
generic
@@ -43,6 +44,9 @@
-- Initiates write of new line to output file, the parameter is the
-- keyword character for the line.
+ with procedure Write_Info_Name (Nam : Name_Id) is <>;
+ -- Outputs one name
+
with procedure Write_Info_Nat (N : Nat) is <>;
-- Writes image of N to output file with no leading or trailing blanks
===================================================================
@@ -28,8 +28,8 @@
-- read SCO information from ALI files (Xcov and sco_test). Ada 2005
-- constructs may therefore be used freely (and are indeed).
+with Namet; use Namet;
with SCOs; use SCOs;
-with Snames; use Snames;
with Types; use Types;
with Ada.IO_Exceptions; use Ada.IO_Exceptions;
@@ -203,6 +203,8 @@
N : Natural;
-- Scratch buffer, and index into it
+ Nam : Name_Id;
+
-- Start of processing for Get_Scos
begin
@@ -308,7 +310,6 @@
declare
Typ : Character;
Key : Character;
- Pid : Pragma_Id;
begin
Key := 'S';
@@ -327,7 +328,7 @@
-- Loop through items on one line
loop
- Pid := Unknown_Pragma;
+ Nam := No_Name;
Typ := Nextc;
case Typ is
@@ -348,25 +349,16 @@
Skipc;
if Typ = 'P' or else Typ = 'p' then
if Nextc not in '1' .. '9' then
- N := 1;
+ Name_Len := 0;
loop
- Buf (N) := Getc;
+ Name_Len := Name_Len + 1;
+ Name_Buffer (Name_Len) := Getc;
exit when Nextc = ':';
- N := N + 1;
end loop;
- Skipc;
+ Skipc; -- Past ':'
- begin
- Pid :=
- Pragma_Id'Value ("pragma_" & Buf (1 .. N));
- exception
- when Constraint_Error =>
-
- -- Pid remains set to Unknown_Pragma
-
- null;
- end;
+ Nam := Name_Find;
end if;
end if;
end case;
@@ -379,13 +371,13 @@
end if;
SCO_Table.Append
- ((C1 => Key,
- C2 => Typ,
- From => Loc1,
- To => Loc2,
- Last => At_EOL,
- Pragma_Sloc => No_Location,
- Pragma_Name => Pid));
+ ((C1 => Key,
+ C2 => Typ,
+ From => Loc1,
+ To => Loc2,
+ Last => At_EOL,
+ Pragma_Sloc => No_Location,
+ Pragma_Aspect_Name => Nam));
if Key = '>' then
Key := 'S';
@@ -397,8 +389,21 @@
-- Decision entry
- when 'E' | 'G' | 'I' | 'P' | 'W' | 'X' =>
+ when 'E' | 'G' | 'I' | 'P' | 'W' | 'X' | 'A' =>
Dtyp := C;
+
+ if C = 'A' then
+ Name_Len := 0;
+ while Nextc /= ' ' loop
+ Name_Len := Name_Len + 1;
+ Name_Buffer (Name_Len) := Getc;
+ end loop;
+ Nam := Name_Find;
+
+ else
+ Nam := No_Name;
+ end if;
+
Skip_Spaces;
-- Output header
@@ -416,12 +421,13 @@
end if;
SCO_Table.Append
- ((C1 => Dtyp,
- C2 => ' ',
- From => Loc,
- To => No_Source_Location,
- Last => False,
- others => <>));
+ ((C1 => Dtyp,
+ C2 => ' ',
+ From => Loc,
+ To => No_Source_Location,
+ Last => False,
+ Pragma_Aspect_Name => Nam,
+ others => <>));
end;
-- Loop through terms in complex expression
This change to the SCO generation circuitry adds support for Ada 2012 aspects. SCO lines will be generated for precondition, postcondition, invariant, and predicate aspects. The following compilation must produce the indicated CA SCO: $ gcc -c -fdump-scos -gnata -gnat12 main.adb $ grep ^CA main.ali CApost 4:11 c4:19-4:27 procedure Main is procedure Add (A : in Integer; B : in Integer; C : out Integer) with Post => C = A + B; procedure Add (A : in Integer; B : in Integer; C : out Integer) is begin C := A + B; end Add; R : Integer; begin Add (1, 2, R); end Main; 2012-12-05 Thomas Quinot <quinot@adacore.com> * par_sco.adb, scos.ads, sco_test.adb, put_scos.adb, put_scos.ads, get_scos.adb: Generation of SCOs for aspects.