Patchwork [Ada] Implement new attribute Restriction_Set

login
register
mail settings
Submitter Arnaud Charlet
Date July 8, 2013, 8:15 a.m.
Message ID <20130708081543.GA10996@adacore.com>
Download mbox | patch
Permalink /patch/257500/
State New
Headers show

Comments

Arnaud Charlet - July 8, 2013, 8:15 a.m.
This attribute allows compile time testing of restrictions that
are currently in effect. It is primarily intended for specializing
code in the run-time based on restrictions that are active (e.g.
don't need to save fpt registers if restriction No_Floating_Point
is known to be in effect), but can be used anywhere.

There are two forms:

   System'Restriction_Set (partition_boolean_restriction_NAME)

   System'Restriction_Set (No_Dependence => library_unit_NAME);

In the case of the first form, the only restriction names
allowed are parameterless restrictions that are checked
for consistency at bind time. For a complete list see the
subtype System.Rident.Partition_Boolean_Restrictions.

The result returned is True if the restriction is known to
be in effect, and False if the restriction is known not to
be in effect. An important guarantee is that the value of
a Restriction_Set attribute is known to be consistent throughout
all the code of a partition.

This is trivially achieved if the entire partition is compiled
with a consistent set of restriction pragmas. However, the
compilation model does not require this. It is possible to
compile one set of units with one set of pragmas, and another
set of units with another set of pragmas. It is even possible
to compile a spec with one set of pragmas, and then WITH the
same spec with a different set of pragmas. Inconsistencies
in the actual use of the restriction are checked at bind time.

In order to achieve the guarantee of consistency for the
Restriction_Set pragma, we consider that a use of the pragma
that yields False is equivalent to a violation of the
restriction.

So for example if you write

   if System'Restriction_Set (No_Floating_Point) then
      ...
   else
      ...
   end if;

And the result is False, so that the else branch is executed,
you can assume that this restriction is not set for any unit
in the partition. This is checked by considering this use of
the restriction pragma to be a violation of the restriction
No_Floating_Point. This means that no other unit can attempt
to set this restriction (if some unit does attempt to set it,
the binder will refuse to bind the partition).

Technical note: The restriction name and the unit name are
intepreted entirely syntactically, as in the corresponding
Restrictions pragma, they are not analyzed semantically,
so they do not have a type.

Notes:

We abandoned the three state model (known_set, known_not_set,
unknown) since it is just too difficult to reason about. It
does allow more flexibility, but our discussions indicated
that this flexibility was not worth the complexity.

We abandoned the requirement for WITHing System'Restrictions.
We no longer need it for the result, and it seems fine since
this is our own attribute to intepret the restriction names
purely syntactically.

We allow only the restrictions that are checked by the binder,
because those are the only ones for which we can make the
important guarantee of consistent evaluation throughout
the partition.

The following program compiles with the indicated errors
using the switch -gnatq:

     1. with System;
     2. package RSetBad is
     3.    X1 : Boolean := Standard'Restriction_Set (No_IO);     -- ERR
                           |
        >>> prefix of "Restriction_Set" attribute must be System

     4.    X2 : Boolean := System'Restriction_Set (No_IO);       -- OK
     5.    X3 : Boolean := System'Restriction_Set (SPARK_05);    -- ERR
                                                   |
        >>> "SPARK_05" is not a boolean partition-wide restriction

     6.    X4 : Boolean := System'Restriction_Set ("No_IO");     -- ERR
                                                   |
        >>> attribute "Restriction_Set" requires restriction identifier

     7.    X5 : Boolean := System'Restriction_Set (RSetBad);     -- ERR
                                                   |
        >>> invalid restriction identifier "RSetBad"

     8.    X6 : Boolean := System'Restriction_Set
     9.                      (No_Dependence => Ada.Text_IO);     -- OK
    10.    X7 : Boolean := System'Restriction_Set
    11.                      (No_Dependence => "Ada.Text_IO");   -- ERR
                                               |
        >>> name expected
        >>> wrong form for unit name for No_Dependence

    12.    X8 : Boolean := System'Restriction_Set
    13.                      (No_IO => Ada.Text_IO);             -- ERR
                                    1     2
        >>> named parameters not permitted for attributes
        >>> attribute "Restriction_Set" requires restriction identifier

    14. end;

The following program compiles without errors, and the resulting
binder files do not mention Calendar.

     1. pragma Restrictions (No_Delay);
     2. pragma Restrictions (No_Dependence => Ada.Text_IO);
     3. with System;
     4. with GNAT.IO; use GNAT.IO;
     5. procedure RSetGood is
     6. begin
     7.     if System'Restriction_Set (No_Floating_Point) then
     8.       Put_Line ("ERROR 1");
     9.    else
    10.       Put_Line ("OK 1");
    11.    end if;
    12.
    13.    if System'Restriction_Set (No_Delay) then
    14.       Put_Line ("OK 2");
    15.    else
    16.       Put_Line ("ERROR 2");
    17.    end if;
    18.
    19.    if System'Restriction_Set (No_Dependence => Ada.Text_IO) then
    20.       Put_Line ("OK 3");
    21.    else
    22.       Put_Line ("ERROR 3");
    23.    end if;
    24.
    25.    if System'Restriction_Set (No_Dependence => Ada.Calendar) then
    26.       Put_Line ("ERROR 4");
    27.    else
    28.       Put_Line ("OK 4");
    29.    end if;
    30.
    31. end RSetGood;

The output of the above program is:

OK 1
OK 2
OK 3
OK 4

Finally given the two additional units:

     1. with RsetGood;
     2. with RsetGood2;
     3. procedure RsetGoodM is
     4. begin
     5.    null;
     6. end;

     1. pragma Restrictions (No_Dependence => Ada.Calendar);
     2. pragma Restrictions (No_Floating_Point);
     3. package RsetGood2 is
     4. end;

The attempt to build RsetGoodM as a main program fails
at bind time with the output:

error: "rsetgood2.ads" has restriction No_Floating_Point
error: but the following files violate this restriction:
error:   "rsetgood.adb"
error: file "rsetgood.adb" violates restriction
  No_Dependence => "ada.calendar"

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

2013-07-08  Robert Dewar  <dewar@adacore.com>

	* exp_attr.adb (Expand_N_Attribute_Reference): Add dummy entry
	for Restriction_Set.
	* gnat_rm.texi: Add missing menu entry for Attribute Ref Add
	documentation for attribute Restriction_Set.
	* lib-writ.adb (Write_With_Lines): Generate special W lines
	for Restriction_Set.
	* lib-writ.ads: Document special use of W lines for
	Restriction_Set.
	* lib.ads (Restriction_Set_Dependences): New table.
	* par-ch4.adb (Is_Parameterless_Attribute): Add Loop_Entry to
	list (Scan_Name_Extension_Apostrophe): Remove kludge test for
	Loop_Entry (Scan_Name_Extension_Apostrophe): Handle No_Dependence
	for Restricton_Set.
	* restrict.adb (Check_SPARK_Restriction): Put in Alfa order
	(OK_No_Dependence_Unit_Name): New function.
	* restrict.ads (OK_No_Dependence_Unit_Name): New function.
	* rtsfind.adb: Minor reformatting Minor code reorganization.
	* sem_attr.adb (Analyze_Attribute): Add processing for
	Restriction_Set.
	* sem_prag.adb (Process_Restrictions_Or_Restriction_Warnings):
	Remove Check_Unit_Name and use new function
	OK_No_Dependence_Unit_Name instead.
	* sinfo.ads: Minor comment updates.
	* snames.ads-tmpl: Add entry for Restriction_Set attribute.

Patch

Index: lib.ads
===================================================================
--- lib.ads	(revision 200753)
+++ lib.ads	(working copy)
@@ -688,6 +688,42 @@ 
    --  of the printout. If Withs is True, we print out units with'ed by this
    --  unit (not counting limited withs).
 
+   ---------------------------------------------------------------
+   -- Special Handling for Restriction_Set (No_Dependence) Case --
+   ---------------------------------------------------------------
+
+   --  If we have a Restriction_Set attribute for No_Dependence => unit,
+   --  and the unit is not given in a No_Dependence restriction that we
+   --  can see, the attribute will return False.
+
+   --  We have to ensure in this case that the binder will reject any attempt
+   --  to set a No_Dependence restriction in some other unit in the partition.
+
+   --  If the unit is in the semantic closure, then of course it is properly
+   --  WITH'ed by someone, and the binder will do this job automatically as
+   --  part of its normal processing.
+
+   --  But if the unit is not in the semantic closure, we must make sure the
+   --  binder knows about it. The use of the Restriction_Set attribute giving
+   --  a result of False does not mean of itself that we have to include the
+   --  unit in the partition. So what we do is to generate a with (W) line in
+   --  the ali file (with no file name information), but no corresponding D
+   --  (dependency) line. This is recognized by the binder as meaning "Don't
+   --  let anyone specify No_Dependence for this unit, but you don't have to
+   --  include it if there is no real W line for the unit".
+
+   --  The following table keeps track of relevant units. It is used in the
+   --  Lib.Writ circuit for outputting With lines to output the special with
+   --  line with RA if the unit is not in the semantic closure.
+
+   package Restriction_Set_Dependences is new Table.Table (
+     Table_Component_Type => Unit_Name_Type,
+     Table_Index_Type     => Int,
+     Table_Low_Bound      => 0,
+     Table_Initial        => 10,
+     Table_Increment      => 100,
+     Table_Name           => "Restriction_Attribute_Dependences");
+
 private
    pragma Inline (Cunit);
    pragma Inline (Cunit_Entity);
Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi	(revision 200769)
+++ gnat_rm.texi	(working copy)
@@ -343,6 +343,8 @@ 
 * Attribute Passed_By_Reference::
 * Attribute Pool_Address::
 * Attribute Range_Length::
+* Attribute Ref::
+* Attribute Restriction_Set::
 * Attribute Result::
 * Attribute Safe_Emax::
 * Attribute Safe_Large::
@@ -7645,6 +7647,7 @@ 
 * Attribute Pool_Address::
 * Attribute Range_Length::
 * Attribute Ref::
+* Attribute Restriction_Set::
 * Attribute Result::
 * Attribute Safe_Emax::
 * Attribute Safe_Large::
@@ -8332,12 +8335,76 @@ 
 @unnumberedsec Attribute Ref
 @findex Ref
 @noindent
-The @code{System.Address'Ref}
-(@code{System.Address} is the only permissible prefix)
-denotes a function identical to
-@code{System.Storage_Elements.To_Address} except that
-it is a static attribute.  See @ref{Attribute To_Address} for more details.
 
+
+@node Attribute Restriction_Set
+@unnumberedsec Attribute Restriction_Set
+@findex Restriction_Set
+@cindex Restrictions
+@noindent
+This attribute allows compile time testing of restrictions that
+are currently in effect. It is primarily intended for specializing
+code in the run-time based on restrictions that are active (e.g.
+don't need to save fpt registers if restriction No_Floating_Point
+is known to be in effect), but can be used anywhere.
+
+There are two forms:
+
+@smallexample @c ada
+System'Restriction_Set (partition_boolean_restriction_NAME)
+System'Restriction_Set (No_Dependence => library_unit_NAME);
+@end smallexample
+
+@noindent
+In the case of the first form, the only restriction names
+allowed are parameterless restrictions that are checked
+for consistency at bind time. For a complete list see the
+subtype @code{System.Rident.Partition_Boolean_Restrictions}.
+
+The result returned is True if the restriction is known to
+be in effect, and False if the restriction is known not to
+be in effect. An important guarantee is that the value of
+a Restriction_Set attribute is known to be consistent throughout
+all the code of a partition.
+
+This is trivially achieved if the entire partition is compiled
+with a consistent set of restriction pragmas. However, the
+compilation model does not require this. It is possible to
+compile one set of units with one set of pragmas, and another
+set of units with another set of pragmas. It is even possible
+to compile a spec with one set of pragmas, and then WITH the
+same spec with a different set of pragmas. Inconsistencies
+in the actual use of the restriction are checked at bind time.
+
+In order to achieve the guarantee of consistency for the
+Restriction_Set pragma, we consider that a use of the pragma
+that yields False is equivalent to a violation of the
+restriction.
+
+So for example if you write
+
+@smallexample @c ada
+if System'Restriction_Set (No_Floating_Point) then
+   ...
+else
+   ...
+end if;
+@end smallexample
+
+@noindent
+And the result is False, so that the else branch is executed,
+you can assume that this restriction is not set for any unit
+in the partition. This is checked by considering this use of
+the restriction pragma to be a violation of the restriction
+No_Floating_Point. This means that no other unit can attempt
+to set this restriction (if some unit does attempt to set it,
+the binder will refuse to bind the partition).
+
+Technical note: The restriction name and the unit name are
+intepreted entirely syntactically, as in the corresponding
+Restrictions pragma, they are not analyzed semantically,
+so they do not have a type.
+
 @node Attribute Result
 @unnumberedsec Attribute Result
 @findex Result
Index: exp_attr.adb
===================================================================
--- exp_attr.adb	(revision 200688)
+++ exp_attr.adb	(working copy)
@@ -6500,6 +6500,7 @@ 
            Attribute_Modulus                      |
            Attribute_Partition_ID                 |
            Attribute_Range                        |
+           Attribute_Restriction_Set              |
            Attribute_Safe_Emax                    |
            Attribute_Safe_First                   |
            Attribute_Safe_Large                   |
Index: sinfo.ads
===================================================================
--- sinfo.ads	(revision 200711)
+++ sinfo.ads	(working copy)
@@ -1516,14 +1516,14 @@ 
    --    in rtsfind to indicate implicit dependencies on predefined units. Used
    --    to prevent multiple with_clauses for the same unit in a given context.
    --    A postorder traversal of the tree whose nodes are units and whose
-   --    links are with_clauses defines the order in which Inspector must
+   --    links are with_clauses defines the order in which CodePeer must
    --    examine a compiled unit and its full context. This ordering ensures
    --    that any subprogram call is examined after the subprogram declaration
    --    has been seen.
 
    --  Next_Named_Actual (Node4-Sem)
-   --    Present in parameter association node. Set during semantic analysis to
-   --    point to the next named parameter, where parameters are ordered by
+   --    Present in parameter association nodes. Set during semantic analysis
+   --    to point to the next named parameter, where parameters are ordered by
    --    declaration order (as opposed to the actual order in the call, which
    --    may be different due to named associations). Not that this field
    --    points to the explicit actual parameter itself, not to the
Index: lib-writ.adb
===================================================================
--- lib-writ.adb	(revision 200711)
+++ lib-writ.adb	(working copy)
@@ -882,6 +882,38 @@ 
 
             Write_Info_EOL;
          end loop;
+
+         --  Finally generate the special lines for cases of Restriction_Set
+         --  with No_Dependence and no restriction present.
+
+         declare
+            Unam : Unit_Name_Type;
+
+         begin
+            for J in Restriction_Set_Dependences.First ..
+                     Restriction_Set_Dependences.Last
+            loop
+               Unam := Restriction_Set_Dependences.Table (J);
+
+               --  Don't need an entry if already in the unit table
+
+               for U in 0 .. Last_Unit loop
+                  if Unit_Name (U) = Unam then
+                     goto Continue;
+                  end if;
+               end loop;
+
+               --  Otherwise generate the entry
+
+               Write_Info_Initiate ('W');
+               Write_Info_Char (' ');
+               Write_Info_Name (Unam);
+               Write_Info_EOL;
+
+            <<Continue>>
+               null;
+            end loop;
+         end;
       end Write_With_Lines;
 
    --  Start of processing for Write_ALI
Index: lib-writ.ads
===================================================================
--- lib-writ.ads	(revision 200688)
+++ lib-writ.ads	(working copy)
@@ -402,7 +402,9 @@ 
 
    --    No restriction pragma is present for the named boolean restriction.
    --    However, the compiler did detect one or more violations of this
-   --    restriction, which may require a binder consistency check.
+   --    restriction, which may require a binder consistency check. Note that
+   --    one case of a violation is the use of a Restriction_Set attribute for
+   --    the restriction that yielded False.
 
    --  For the case of restrictions that take a parameter, we need both the
    --  information from pragma if present, and the actual information about
@@ -618,9 +620,9 @@ 
    --  Following each U line, is a series of lines of the form
 
    --    W unit-name [source-name lib-name] [E] [EA] [ED] [AD]
-   --    or
+   --      or
    --    Y unit-name [source-name lib-name] [E] [EA] [ED] [AD]
-   --    or
+   --      or
    --    Z unit-name [source-name lib-name] [E] [EA] [ED] [AD]
    --
    --      One W line is present for each unit that is mentioned in an explicit
@@ -655,6 +657,14 @@ 
    --      The parameter source-name and lib-name are omitted for the case of a
    --      generic unit compiled with earlier versions of GNAT which did not
    --      generate object or ali files for generics.
+   --
+   --      The parameter source-name and lib-name are also omitted for the W
+   --      lines that result from use of a Restriction_Set attribute which gets
+   --      a result of False from a No_Dependence check, in the case where the
+   --      unit is not in the semantic closure. In such a case, the bare W
+   --      line is generated, but no D (dependency) line. This will make the
+   --      binder do the consistency check, but not include the unit in the
+   --      partition closure (unless it is properly With'ed somewhere).
 
    --  -----------------------
    --  -- L  Linker_Options --
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 200766)
+++ sem_prag.adb	(working copy)
@@ -6990,31 +6990,6 @@ 
          Expr  : Node_Id;
          Val   : Uint;
 
-         procedure Check_Unit_Name (N : Node_Id);
-         --  Checks unit name parameter for No_Dependence. Returns if it has
-         --  an appropriate form, otherwise raises pragma argument error.
-
-         ---------------------
-         -- Check_Unit_Name --
-         ---------------------
-
-         procedure Check_Unit_Name (N : Node_Id) is
-         begin
-            if Nkind (N) = N_Selected_Component then
-               Check_Unit_Name (Prefix (N));
-               Check_Unit_Name (Selector_Name (N));
-
-            elsif Nkind (N) = N_Identifier then
-               return;
-
-            else
-               Error_Pragma_Arg
-                 ("wrong form for unit name for No_Dependence", N);
-            end if;
-         end Check_Unit_Name;
-
-      --  Start of processing for Process_Restrictions_Or_Restriction_Warnings
-
       begin
          --  Ignore all Restrictions pragmas in CodePeer mode
 
@@ -7174,7 +7149,9 @@ 
             --  already made the necessary entry in the No_Dependence table.
 
             elsif Id = Name_No_Dependence then
-               Check_Unit_Name (Expr);
+               if not OK_No_Dependence_Unit_Name (Expr) then
+                  raise Pragma_Exit;
+               end if;
 
             --  Case of No_Specification_Of_Aspect => Identifier.
 
Index: rtsfind.adb
===================================================================
--- rtsfind.adb	(revision 200688)
+++ rtsfind.adb	(working copy)
@@ -82,7 +82,7 @@ 
 
    --  A unit retrieved through rtsfind  may end up in the context of several
    --  other units, in addition to the main unit. These additional with_clauses
-   --  are needed to generate a proper traversal order for Inspector. To
+   --  are needed to generate a proper traversal order for CodePeer. To
    --  minimize somewhat the redundancy created by numerous calls to rtsfind
    --  from different units, we keep track of the list of implicit with_clauses
    --  already created for the current loaded unit.
@@ -123,7 +123,7 @@ 
    --  with_clauses to the extended main unit if needed, and also to whatever
    --  unit needs them, which is not necessarily the main unit. The former
    --  ensures that the object is correctly loaded by the binder. The latter
-   --  is necessary for SofCheck Inspector.
+   --  is necessary for CodePeer.
 
    --  The field First_Implicit_With in the unit table record are used to
    --  avoid creating duplicate with_clauses.
@@ -827,10 +827,9 @@ 
       --  We do not need to generate a with_clause for a call issued from
       --  RTE_Component_Available. However, for CodePeer, we need these
       --  additional with's, because for a sequence like "if RTE_Available (X)
-      --  then ... RTE (X)" the RTE call fails to create some necessary
-      --  with's.
+      --  then ... RTE (X)" the RTE call fails to create some necessary with's.
 
-      if RTE_Available_Call and then not Generate_SCIL then
+      if RTE_Available_Call and not Generate_SCIL then
          return;
       end if;
 
@@ -840,8 +839,8 @@ 
          return;
       end if;
 
-      --  Add the with_clause, if not already in the context of the
-      --  current compilation unit.
+      --  Add the with_clause, if not already in the context of the current
+      --  compilation unit.
 
       declare
          LibUnit : constant Node_Id := Unit (Cunit (U.Unum));
Index: par-ch4.adb
===================================================================
--- par-ch4.adb	(revision 200688)
+++ par-ch4.adb	(working copy)
@@ -40,6 +40,7 @@ 
       Attribute_Class        => True,
       Attribute_External_Tag => True,
       Attribute_Img          => True,
+      Attribute_Loop_Entry   => True,
       Attribute_Stub_Type    => True,
       Attribute_Version      => True,
       Attribute_Type_Key     => True,
@@ -50,6 +51,13 @@ 
    --  list because it may denote a slice operation (X'Img (1 .. 2)) or
    --  a type conversion (X'Class (Y)).
 
+   --  Note: Loop_Entry is in this list because, although it can take an
+   --  optional argument (the loop name), we can't distinguish that at parse
+   --  time from the case where no loop name is given and a legitimate index
+   --  expression is present. So we parse the argument as an indexed component
+   --  and the semantic analysis sorts out this syntactic ambiguity based on
+   --  the type and form of the expression.
+
    --  Note that this map designates the minimum set of attributes where a
    --  construct in parentheses that is not an argument can appear right
    --  after the attribute. For attributes like 'Size, we do not put them
@@ -503,29 +511,24 @@ 
             Set_Attribute_Name (Name_Node, Attr_Name);
 
             --  Scan attribute arguments/designator. We skip this if we know
-            --  that the attribute cannot have an argument.
+            --  that the attribute cannot have an argument (see documentation
+            --  of Is_Parameterless_Attribute for further details).
 
             if Token = Tok_Left_Paren
               and then not
                 Is_Parameterless_Attribute (Get_Attribute_Id (Attr_Name))
             then
-               --  Attribute Loop_Entry has no effect on the name extension
-               --  parsing logic, as if the attribute never existed in the
-               --  source. Continue parsing the subsequent expressions or
-               --  ranges.
-
-               if Attr_Name = Name_Loop_Entry then
-                  Scan; -- past left paren
-                  goto Scan_Name_Extension_Left_Paren;
-
                --  Attribute Update contains an array or record association
                --  list which provides new values for various components or
-               --  elements. The list is parsed as an aggregate.
+               --  elements. The list is parsed as an aggregate, and we get
+               --  better error handling by knowing that in the parser.
 
-               elsif Attr_Name = Name_Update then
+               if Attr_Name = Name_Update then
                   Set_Expressions (Name_Node, New_List);
                   Append (P_Aggregate, Expressions (Name_Node));
 
+               --  All other cases of parsing attribute arguments
+
                else
                   Set_Expressions (Name_Node, New_List);
                   Scan; -- past left paren
@@ -533,13 +536,41 @@ 
                   loop
                      declare
                         Expr : constant Node_Id := P_Expression_If_OK;
+                        Rnam : Node_Id;
 
                      begin
+                        --  Case of => for named notation
+
                         if Token = Tok_Arrow then
-                           Error_Msg_SC
-                             ("named parameters not permitted for attributes");
-                           Scan; -- past junk arrow
 
+                           --  Named notation allowed only for the special
+                           --  case of System'Restriction_Set (No_Dependence =>
+                           --  unit_NAME), in which case construct a parameter
+                           --  assocation node and append to the arguments.
+
+                           if Attr_Name = Name_Restriction_Set
+                             and then Nkind (Expr) = N_Identifier
+                             and then Chars (Expr) = Name_No_Dependence
+                           then
+                              Scan; -- past arrow
+                              Rnam := P_Name;
+                              Append_To (Expressions (Name_Node),
+                                Make_Parameter_Association (Sloc (Rnam),
+                                  Selector_Name             => Expr,
+                                  Explicit_Actual_Parameter => Rnam));
+                              exit;
+
+                           --  For all other cases named notation is illegal
+
+                           else
+                              Error_Msg_SC
+                                ("named parameters not permitted "
+                                 & "for attributes");
+                              Scan; -- past junk arrow
+                           end if;
+
+                        --  Here for normal case (not => for named parameter)
+
                         else
                            Append (Expr, Expressions (Name_Node));
                            exit when not Comma_Present;
Index: sem_attr.adb
===================================================================
--- sem_attr.adb	(revision 200688)
+++ sem_attr.adb	(working copy)
@@ -72,6 +72,7 @@ 
 with Ttypes;   use Ttypes;
 with Tbuild;   use Tbuild;
 with Uintp;    use Uintp;
+with Uname;    use Uname;
 with Urealp;   use Urealp;
 
 package body Sem_Attr is
@@ -1642,9 +1643,7 @@ 
       begin
          Check_E0;
 
-         if Nkind (P) /= N_Identifier
-           or else Chars (P) /= Name_Standard
-         then
+         if Nkind (P) /= N_Identifier or else Chars (P) /= Name_Standard then
             Error_Attr ("only allowed prefix for % attribute is Standard", P);
          end if;
       end Check_Standard_Prefix;
@@ -1658,12 +1657,11 @@ 
          Btyp : Entity_Id;
 
          In_Shared_Var_Procs : Boolean;
-         --  True when compiling the body of System.Shared_Storage.
-         --  Shared_Var_Procs. For this runtime package (always compiled in
-         --  GNAT mode), we allow stream attributes references for limited
-         --  types for the case where shared passive objects are implemented
-         --  using stream attributes, which is the default in GNAT's persistent
-         --  storage implementation.
+         --  True when compiling System.Shared_Storage.Shared_Var_Procs body.
+         --  For this runtime package (always compiled in GNAT mode), we allow
+         --  stream attributes references for limited types for the case where
+         --  shared passive objects are implemented using stream attributes,
+         --  which is the default in GNAT's persistent storage implementation.
 
       begin
          Validate_Non_Static_Attribute_Function_Call;
@@ -2049,16 +2047,11 @@ 
       --  some attributes for which we do not analyze the prefix, since the
       --  prefix is not a normal name, or else needs special handling.
 
-      if Aname /= Name_Elab_Body
-           and then
-         Aname /= Name_Elab_Spec
-           and then
-         Aname /= Name_Elab_Subp_Body
-           and then
-         Aname /= Name_UET_Address
-           and then
-         Aname /= Name_Enabled
-           and then
+      if Aname /= Name_Elab_Body       and then
+         Aname /= Name_Elab_Spec       and then
+         Aname /= Name_Elab_Subp_Body  and then
+         Aname /= Name_UET_Address     and then
+         Aname /= Name_Enabled         and then
          Aname /= Name_Old
       then
          Analyze (P);
@@ -2122,12 +2115,18 @@ 
 
       else
          E1 := First (Exprs);
-         Analyze (E1);
 
-         --  Check for missing/bad expression (result of previous error)
+         --  Skip analysis for case of Restriction_Set, we do not expect
+         --  the argument to be analyzed in this case.
 
-         if No (E1) or else Etype (E1) = Any_Type then
-            raise Bad_Attribute;
+         if Aname /= Name_Restriction_Set then
+            Analyze (E1);
+
+            --  Check for missing/bad expression (result of previous error)
+
+            if No (E1) or else Etype (E1) = Any_Type then
+               raise Bad_Attribute;
+            end if;
          end if;
 
          E2 := Next (E1);
@@ -4832,6 +4831,121 @@ 
          Resolve (E1, P_Base_Type);
          Resolve (E2, P_Base_Type);
 
+      ---------------------
+      -- Restriction_Set --
+      ---------------------
+
+      when Attribute_Restriction_Set => Restriction_Set : declare
+         R    : Restriction_Id;
+         U    : Node_Id;
+         Unam : Unit_Name_Type;
+
+         procedure Set_Result (B : Boolean);
+         --  Replace restriction node by static constant False or True,
+         --  depending on the value of B.
+
+         ----------------
+         -- Set_Result --
+         ----------------
+
+         procedure Set_Result (B : Boolean) is
+         begin
+            if B then
+               Rewrite (N, New_Occurrence_Of (Standard_True, Loc));
+            else
+               Rewrite (N, New_Occurrence_Of (Standard_False, Loc));
+            end if;
+
+            Set_Is_Static_Expression (N);
+         end Set_Result;
+
+      --  Start of processing for Restriction_Set
+
+      begin
+         Check_E1;
+         Analyze (P);
+
+         if Nkind (P) /= N_Identifier or else Chars (P) /= Name_System then
+            Set_Result (False);
+            Error_Attr_P ("prefix of % attribute must be System");
+         end if;
+
+         --  No_Dependence case
+
+         if Nkind (E1) = N_Parameter_Association then
+            pragma Assert (Chars (Selector_Name (E1)) = Name_No_Dependence);
+            U := Explicit_Actual_Parameter (E1);
+
+            if not OK_No_Dependence_Unit_Name (U) then
+               Set_Result (False);
+               Error_Attr;
+            end if;
+
+            --  See if there is an entry already in the table. That's the
+            --  case in which we can return True.
+
+            for J in No_Dependences.First .. No_Dependences.Last loop
+               if Designate_Same_Unit (U, No_Dependences.Table (J).Unit)
+                 and then No_Dependences.Table (J).Warn = False
+               then
+                  Set_Result (True);
+                  return;
+               end if;
+            end loop;
+
+            --  If not in the No_Dependence table, result is False
+
+            Set_Result (False);
+
+            --  In this case, we must ensure that the binder will reject any
+            --  other unit in the partition that sets No_Dependence for this
+            --  unit. We do that by making an entry in the special table kept
+            --  for this purpose (if the entry is not there already).
+
+            Unam := Get_Spec_Name (Get_Unit_Name (U));
+
+            for J in Restriction_Set_Dependences.First ..
+                     Restriction_Set_Dependences.Last
+            loop
+               if Restriction_Set_Dependences.Table (J) = Unam then
+                  return;
+               end if;
+            end loop;
+
+            Restriction_Set_Dependences.Append (Unam);
+
+         --  Normal restriction case
+
+         else
+            if Nkind (E1) /= N_Identifier then
+               Set_Result (False);
+               Error_Attr ("attribute % requires restriction identifier", E1);
+
+            else
+               R := Get_Restriction_Id (Process_Restriction_Synonyms (E1));
+
+               if R = Not_A_Restriction_Id then
+                  Set_Result (False);
+                  Error_Msg_Node_1 := E1;
+                  Error_Attr ("invalid restriction identifier &", E1);
+
+               elsif R not in Partition_Boolean_Restrictions then
+                  Set_Result (False);
+                  Error_Msg_Node_1 := E1;
+                  Error_Attr
+                    ("& is not a boolean partition-wide restriction", E1);
+               end if;
+
+               if Restriction_Active (R) then
+                  Set_Result (True);
+               else
+                  Check_Restriction (R, N);
+                  Set_Result (False);
+               end if;
+            end if;
+         end if;
+      end Restriction_Set;
+
       -----------
       -- Round --
       -----------
@@ -5334,9 +5448,7 @@ 
          Check_E1;
          Analyze (P);
 
-         if Nkind (P) /= N_Identifier
-           or else Chars (P) /= Name_System
-         then
+         if Nkind (P) /= N_Identifier or else Chars (P) /= Name_System then
             Error_Attr_P ("prefix of % attribute must be System");
          end if;
 
@@ -8072,6 +8184,16 @@ 
          Fold_Ureal (N, Eval_Fat.Remainder (P_Base_Type, X, Y), Static);
       end Remainder;
 
+      -----------------
+      -- Restriction --
+      -----------------
+
+      when Attribute_Restriction_Set => Restriction_Set : declare
+      begin
+         Rewrite (N, New_Occurrence_Of (Standard_False, Loc));
+         Set_Is_Static_Expression (N);
+      end Restriction_Set;
+
       -----------
       -- Round --
       -----------
Index: restrict.adb
===================================================================
--- restrict.adb	(revision 200769)
+++ restrict.adb	(working copy)
@@ -184,69 +184,6 @@ 
       Check_Restriction (No_Elaboration_Code, N);
    end Check_Elaboration_Code_Allowed;
 
-   -----------------------------
-   -- Check_SPARK_Restriction --
-   -----------------------------
-
-   procedure Check_SPARK_Restriction
-     (Msg   : String;
-      N     : Node_Id;
-      Force : Boolean := False)
-   is
-      Msg_Issued          : Boolean;
-      Save_Error_Msg_Sloc : Source_Ptr;
-
-   begin
-      if Force or else Comes_From_Source (Original_Node (N)) then
-         if Restriction_Check_Required (SPARK_05)
-           and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
-         then
-            return;
-         end if;
-
-         --  Since the call to Restriction_Msg from Check_Restriction may set
-         --  Error_Msg_Sloc to the location of the pragma restriction, save and
-         --  restore the previous value of the global variable around the call.
-
-         Save_Error_Msg_Sloc := Error_Msg_Sloc;
-         Check_Restriction (Msg_Issued, SPARK_05, First_Node (N));
-         Error_Msg_Sloc := Save_Error_Msg_Sloc;
-
-         if Msg_Issued then
-            Error_Msg_F ("\\| " & Msg, N);
-         end if;
-      end if;
-   end Check_SPARK_Restriction;
-
-   procedure Check_SPARK_Restriction (Msg1, Msg2 : String; N : Node_Id) is
-      Msg_Issued          : Boolean;
-      Save_Error_Msg_Sloc : Source_Ptr;
-
-   begin
-      pragma Assert (Msg2'Length /= 0 and then Msg2 (Msg2'First) = '\');
-
-      if Comes_From_Source (Original_Node (N)) then
-         if Restriction_Check_Required (SPARK_05)
-           and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
-         then
-            return;
-         end if;
-
-         --  Since the call to Restriction_Msg from Check_Restriction may set
-         --  Error_Msg_Sloc to the location of the pragma restriction, save and
-         --  restore the previous value of the global variable around the call.
-
-         Save_Error_Msg_Sloc := Error_Msg_Sloc;
-         Check_Restriction (Msg_Issued, SPARK_05, First_Node (N));
-         Error_Msg_Sloc := Save_Error_Msg_Sloc;
-
-         if Msg_Issued then
-            Error_Msg_F ("\\| " & Msg1, N);
-            Error_Msg_F (Msg2, N);
-         end if;
-      end if;
-   end Check_SPARK_Restriction;
-
    --------------------------------
    -- Check_No_Implicit_Aliasing --
    --------------------------------
@@ -883,6 +820,27 @@ 
         and then Restriction_Active (No_Exception_Propagation);
    end No_Exception_Propagation_Active;
 
+   --------------------------------
+   -- OK_No_Dependence_Unit_Name --
+   --------------------------------
+
+   function OK_No_Dependence_Unit_Name (N : Node_Id) return Boolean is
+   begin
+      if Nkind (N) = N_Selected_Component then
+         return
+           OK_No_Dependence_Unit_Name (Prefix (N))
+             and then
+           OK_No_Dependence_Unit_Name (Selector_Name (N));
+
+      elsif Nkind (N) = N_Identifier then
+         return True;
+
+      else
+         Error_Msg_N ("wrong form for unit name for No_Dependence", N);
+         return False;
+      end if;
+   end OK_No_Dependence_Unit_Name;
+
    ----------------------------------
    -- Process_Restriction_Synonyms --
    ----------------------------------
@@ -1437,6 +1395,69 @@ 
       end if;
    end Set_Restriction_No_Use_Of_Pragma;
 
+   -----------------------------
+   -- Check_SPARK_Restriction --
+   -----------------------------
+
+   procedure Check_SPARK_Restriction
+     (Msg   : String;
+      N     : Node_Id;
+      Force : Boolean := False)
+   is
+      Msg_Issued          : Boolean;
+      Save_Error_Msg_Sloc : Source_Ptr;
+
+   begin
+      if Force or else Comes_From_Source (Original_Node (N)) then
+         if Restriction_Check_Required (SPARK_05)
+           and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
+         then
+            return;
+         end if;
+
+         --  Since the call to Restriction_Msg from Check_Restriction may set
+         --  Error_Msg_Sloc to the location of the pragma restriction, save and
+         --  restore the previous value of the global variable around the call.
+
+         Save_Error_Msg_Sloc := Error_Msg_Sloc;
+         Check_Restriction (Msg_Issued, SPARK_05, First_Node (N));
+         Error_Msg_Sloc := Save_Error_Msg_Sloc;
+
+         if Msg_Issued then
+            Error_Msg_F ("\\| " & Msg, N);
+         end if;
+      end if;
+   end Check_SPARK_Restriction;
+
+   procedure Check_SPARK_Restriction (Msg1, Msg2 : String; N : Node_Id) is
+      Msg_Issued          : Boolean;
+      Save_Error_Msg_Sloc : Source_Ptr;
+
+   begin
+      pragma Assert (Msg2'Length /= 0 and then Msg2 (Msg2'First) = '\');
+
+      if Comes_From_Source (Original_Node (N)) then
+         if Restriction_Check_Required (SPARK_05)
+           and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
+         then
+            return;
+         end if;
+
+         --  Since the call to Restriction_Msg from Check_Restriction may set
+         --  Error_Msg_Sloc to the location of the pragma restriction, save and
+         --  restore the previous value of the global variable around the call.
+
+         Save_Error_Msg_Sloc := Error_Msg_Sloc;
+         Check_Restriction (Msg_Issued, SPARK_05, First_Node (N));
+         Error_Msg_Sloc := Save_Error_Msg_Sloc;
+
+         if Msg_Issued then
+            Error_Msg_F ("\\| " & Msg1, N);
+            Error_Msg_F (Msg2, N);
+         end if;
+      end if;
+   end Check_SPARK_Restriction;
+
    ----------------------------------
    -- Suppress_Restriction_Message --
    ----------------------------------
Index: restrict.ads
===================================================================
--- restrict.ads	(revision 200764)
+++ restrict.ads	(working copy)
@@ -302,6 +302,11 @@ 
    --  identifier, and if so returns the corresponding Restriction_Id value,
    --  otherwise returns Not_A_Restriction_Id.
 
+   function OK_No_Dependence_Unit_Name (N : Node_Id) return Boolean;
+   --  Used in checking No_Dependence argument of pragma Restrictions or
+   --  pragma Restrictions_Warning, or attribute Restriction_Set. Returns
+   --  True if N has the proper form for a unit name, False otherwise.
+
    function Is_In_Hidden_Part_In_SPARK (Loc : Source_Ptr) return Boolean;
    --  Determine if given location is covered by a hidden region range in the
    --  SPARK hides table.
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 200764)
+++ snames.ads-tmpl	(working copy)
@@ -903,6 +903,7 @@ 
    Name_Range                          : constant Name_Id := N + $;
    Name_Range_Length                   : constant Name_Id := N + $; -- GNAT
    Name_Ref                            : constant Name_Id := N + $; -- GNAT
+   Name_Restriction_Set                : constant Name_Id := N + $; -- GNAT
    Name_Result                         : constant Name_Id := N + $; -- GNAT
    Name_Round                          : constant Name_Id := N + $;
    Name_Safe_Emax                      : constant Name_Id := N + $; -- Ada 83
@@ -1519,6 +1520,7 @@ 
       Attribute_Range,
       Attribute_Range_Length,
       Attribute_Ref,
+      Attribute_Restriction_Set,
       Attribute_Result,
       Attribute_Round,
       Attribute_Safe_Emax,