Patchwork [Ada] Assertions_Policy must be captured at time of aspect specification

login
register
mail settings
Submitter Arnaud Charlet
Date April 23, 2013, 9:52 a.m.
Message ID <20130423095218.GA3002@adacore.com>
Download mbox | patch
Permalink /patch/238844/
State New
Headers show

Comments

Arnaud Charlet - April 23, 2013, 9:52 a.m.
This patch ensures that the assertion policy is properly captured at the
time when the aspect is declared. In particular for Postconditions, this
was done wrong (and we captured the policy at the point where the body
was declared).

The following program:

     1. pragma Ada_2012;
     2. procedure DeclIgnore is
     3.    pragma Assertion_Policy (Post => Check);
     4.    procedure Q with Post => False;
     5.    pragma Assertion_Policy (Post => Ignore);
     6.    procedure Q is begin null; end Q;
     7. begin
     8.    Q;
     9. end DeclIgnore;

compiled and run with default options now raises an exception:

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE :
  failed postcondition from decligdb:4

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

2013-04-23  Robert Dewar  <dewar@adacore.com>

	* sem_ch13.adb (Analyze_Aspect_Specifications): Significant
	rewrite to make sure Is_Ignore is properly captured when aspect
	is declared.
	* sem_ch6.adb: Minor reformatting.
	* sem_prag.adb (Analyze_Pragma): Do not test policy at time of
	pragma for the case of a pragma coming from an aspect (already
	tested when we analyzed the aspect).

Patch

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 198183)
+++ sem_prag.adb	(working copy)
@@ -2138,12 +2138,7 @@ 
          --  For a pragma PPC in the extended main source unit, record enabled
          --  status in SCO.
 
-         --  This may seem redundant with the call to Check_Kind test that
-         --  occurs later on when the pragma is rewritten into a pragma Check
-         --  but is actually required in the case of a postcondition within a
-         --  generic.
-
-         if Check_Kind (Pname) = Name_Check and then not Split_PPC (N) then
+         if not Is_Ignored (N) and then not Split_PPC (N) then
             Set_SCO_Pragma_Enabled (Loc);
          end if;
 
@@ -6775,14 +6770,20 @@ 
          Pname := Chars (Identifier (Corresponding_Aspect (N)));
       end if;
 
-      Check_Applicable_Policy (N);
+      --  Check applicable policy. We skip this for a pragma that came from
+      --  an aspect, since we already dealt with the Disable case, and we set
+      --  the Is_Ignored flag at the time the aspect was analyzed.
 
-      --  If pragma is disabled, rewrite as Null statement and skip analysis
+      if not From_Aspect_Specification (N) then
+         Check_Applicable_Policy (N);
 
-      if Is_Disabled (N) then
-         Rewrite (N, Make_Null_Statement (Loc));
-         Analyze (N);
-         raise Pragma_Exit;
+         --  If pragma is disabled, rewrite as NULL and skip analysis
+
+         if Is_Disabled (N) then
+            Rewrite (N, Make_Null_Statement (Loc));
+            Analyze (N);
+            raise Pragma_Exit;
+         end if;
       end if;
 
       --  Preset arguments
@@ -8109,27 +8110,38 @@ 
 
             --  Set Check_On to indicate check status
 
-            case Check_Kind (Cname) is
-               when Name_Ignore =>
-                  Check_On := False;
+            --  If this comes from an aspect, we have already taken care of
+            --  the policy active when the aspect was analyzed, and Is_Ignore
+            --  is set appriately already.
 
-               when Name_Check =>
-                  Check_On := True;
+            if From_Aspect_Specification (N) then
+               Check_On := not Is_Ignored (N);
 
-               --  For disable, rewrite pragma as null statement and skip
-               --  rest of the analysis of the pragma.
+            --  Otherwise check the status right now
 
-               when Name_Disable =>
-                  Rewrite (N, Make_Null_Statement (Loc));
-                  Analyze (N);
-                  raise Pragma_Exit;
+            else
+               case Check_Kind (Cname) is
+                  when Name_Ignore =>
+                     Check_On := False;
 
-               --  No other possibilities
+                  when Name_Check =>
+                     Check_On := True;
 
-               when others =>
-                  raise Program_Error;
-            end case;
+                  --  For disable, rewrite pragma as null statement and skip
+                  --  rest of the analysis of the pragma.
 
+                  when Name_Disable =>
+                     Rewrite (N, Make_Null_Statement (Loc));
+                     Analyze (N);
+                     raise Pragma_Exit;
+
+                     --  No other possibilities
+
+                  when others =>
+                     raise Program_Error;
+               end case;
+            end if;
+
             --  If check kind was not Disable, then continue pragma analysis
 
             Expr := Get_Pragma_Arg (Arg2);
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 198178)
+++ sem_ch6.adb	(working copy)
@@ -12082,16 +12082,12 @@ 
 
                      declare
                         New_Expr : constant Node_Id :=
-                                     Get_Pragma_Arg
-                                       (Next
-                                         (First
-                                           (Pragma_Argument_Associations
-                                             (Inherited_Precond))));
+                          Get_Pragma_Arg
+                            (Next (First (Pragma_Argument_Associations
+                                            (Inherited_Precond))));
                         Old_Expr : constant Node_Id :=
-                                     Get_Pragma_Arg
-                                       (Next
-                                         (First
-                                           (Pragma_Argument_Associations
+                          Get_Pragma_Arg
+                            (Next (First (Pragma_Argument_Associations
                                              (Precond))));
 
                      begin
@@ -12404,8 +12400,7 @@ 
 
          declare
             Post_Proc : constant Entity_Id :=
-                          Make_Defining_Identifier (Loc,
-                            Chars => Name_uPostconditions);
+              Make_Defining_Identifier (Loc, Chars => Name_uPostconditions);
             --  The entity for the _Postconditions procedure
 
          begin
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 198179)
+++ sem_ch13.adb	(working copy)
@@ -961,7 +961,7 @@ 
 
       Aspect := First (L);
       Aspect_Loop : while Present (Aspect) loop
-         declare
+         Analyze_One_Aspect : declare
             Expr : constant Node_Id    := Expression (Aspect);
             Id   : constant Node_Id    := Identifier (Aspect);
             Loc  : constant Source_Ptr := Sloc (Aspect);
@@ -977,13 +977,23 @@ 
             --  is set below when Expr is present.
 
             procedure Analyze_Aspect_External_Or_Link_Name;
-            --  This routine performs the analysis of the External_Name or
-            --  Link_Name aspects.
+            --  Perform analysis of the External_Name or Link_Name aspects
 
             procedure Analyze_Aspect_Implicit_Dereference;
-            --  This routine performs the analysis of the Implicit_Dereference
-            --  aspects.
+            --  Perform  analysis of the Implicit_Dereference aspects
 
+            procedure Make_Aitem_Pragma
+              (Pragma_Argument_Associations : List_Id;
+               Pragma_Name                  : Name_Id);
+            --  This is a wrapper for Make_Pragma used for converting aspects
+            --  to pragmas. It takes care of Sloc (set from Loc) and building
+            --  the pragma identifier from the given name. In addition the
+            --  flags Class_Present and Split_PPC are set from the aspect
+            --  node, as well as Is_Ignored. This routine also sets the
+            --  From_Aspect_Specification in the resulting pragma node to
+            --  True, and sets Corresponding_Aspect to point to the aspect.
+            --  The resulting pragma is assigned to Aitem.
+
             ------------------------------------------
             -- Analyze_Aspect_External_Or_Link_Name --
             ------------------------------------------
@@ -1051,6 +1061,42 @@ 
                end if;
             end Analyze_Aspect_Implicit_Dereference;
 
+            -----------------------
+            -- Make_Aitem_Pragma --
+            -----------------------
+
+            procedure Make_Aitem_Pragma
+              (Pragma_Argument_Associations : List_Id;
+               Pragma_Name                  : Name_Id)
+            is
+            begin
+               --  We should never get here if aspect was disabled
+
+               pragma Assert (not Is_Disabled (Aspect));
+
+               --  Build the pragma
+
+               Aitem :=
+                 Make_Pragma (Loc,
+                   Pragma_Argument_Associations =>
+                     Pragma_Argument_Associations,
+                   Pragma_Identifier =>
+                     Make_Identifier (Sloc (Id), Pragma_Name),
+                     Class_Present     => Class_Present (Aspect),
+                     Split_PPC         => Split_PPC (Aspect));
+
+               --  Set additional semantic fields
+
+               if Is_Ignored (Aspect) then
+                  Set_Is_Ignored (Aitem);
+               end if;
+
+               Set_Corresponding_Aspect (Aitem, Aspect);
+               Set_From_Aspect_Specification (Aitem, True);
+            end Make_Aitem_Pragma;
+
+         --  Start of processing for Analyze_One_Aspect
+
          begin
             --  Skip aspect if already analyzed (not clear if this is needed)
 
@@ -1059,7 +1105,8 @@ 
             end if;
 
             --  Skip looking at aspect if it is totally disabled. Just mark
-            --  it as such for later reference in the tree.
+            --  it as such for later reference in the tree. This also sets
+            --  the Is_Ignored flag appropriately.
 
             Check_Applicable_Policy (Aspect);
 
@@ -1218,54 +1265,52 @@ 
                --  referring to the entity, and the second argument is the
                --  aspect definition expression.
 
+               --  Suppress/Unsuppress
+
                when Aspect_Suppress   |
                     Aspect_Unsuppress =>
 
-                  Aitem :=
-                    Make_Pragma (Loc,
-                      Pragma_Argument_Associations => New_List (
-                        Make_Pragma_Argument_Association (Loc,
-                          Expression => New_Occurrence_Of (E, Loc)),
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => New_Occurrence_Of (E, Loc)),
+                       Make_Pragma_Argument_Association (Sloc (Expr),
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Chars (Id));
 
-                        Make_Pragma_Argument_Association (Sloc (Expr),
-                          Expression => Relocate_Node (Expr))),
+               --  Synchronization
 
-                      Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Chars (Id)));
+               --  Corresponds to pragma Implemented, construct the pragma
 
-               --  The aspect corresponds to pragma Implemented. Construct the
-               --  pragma.
-
                when Aspect_Synchronization =>
-                  Aitem :=
-                    Make_Pragma (Loc,
-                      Pragma_Argument_Associations => New_List (
-                        Make_Pragma_Argument_Association (Loc,
-                          Expression => New_Occurrence_Of (E, Loc)),
 
-                        Make_Pragma_Argument_Association (Sloc (Expr),
-                          Expression => Relocate_Node (Expr))),
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => New_Occurrence_Of (E, Loc)),
+                       Make_Pragma_Argument_Association (Sloc (Expr),
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Implemented);
 
-                      Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Name_Implemented));
-
                   --  No delay is required since the only values are: By_Entry
                   --  | By_Protected_Procedure | By_Any | Optional which don't
                   --  get analyzed anyway.
 
                   Delay_Required := False;
 
+               --  Attach Handler
+
                when Aspect_Attach_Handler =>
-                  Aitem :=
-                    Make_Pragma (Loc,
-                      Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Name_Attach_Handler),
-                          Pragma_Argument_Associations => New_List (
-                            Make_Pragma_Argument_Association (Sloc (Ent),
-                              Expression => Ent),
-                            Make_Pragma_Argument_Association (Sloc (Expr),
-                              Expression => Relocate_Node (Expr))));
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Sloc (Ent),
+                         Expression => Ent),
+                       Make_Pragma_Argument_Association (Sloc (Expr),
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Attach_Handler);
 
+               --  Dynamic_Predicate, Predicate, Static_Predicate
+
                when Aspect_Dynamic_Predicate |
                     Aspect_Predicate         |
                     Aspect_Static_Predicate  =>
@@ -1274,16 +1319,13 @@ 
                   --  flags recording whether it is static/dynamic). We also
                   --  set flags recording this in the type itself.
 
-                  Aitem :=
-                    Make_Pragma (Loc,
-                      Pragma_Argument_Associations => New_List (
-                         Make_Pragma_Argument_Association (Sloc (Ent),
-                           Expression => Ent),
-                         Make_Pragma_Argument_Association (Sloc (Expr),
-                           Expression => Relocate_Node (Expr))),
-                      Class_Present                => Class_Present (Aspect),
-                      Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Name_Predicate));
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Sloc (Ent),
+                         Expression => Ent),
+                       Make_Pragma_Argument_Association (Sloc (Expr),
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Predicate);
 
                   --  Mark type has predicates, and remember what kind of
                   --  aspect lead to this predicate (we need this to access
@@ -1301,9 +1343,7 @@ 
                   --  has a freeze node, because that is the one that will be
                   --  visible at freeze time.
 
-                  if Is_Private_Type (E)
-                    and then Present (Full_View (E))
-                  then
+                  if Is_Private_Type (E) and then Present (Full_View (E)) then
                      Set_Has_Predicates (Full_View (E));
 
                      if A_Id = Aspect_Dynamic_Predicate then
@@ -1321,6 +1361,8 @@ 
                --  referring to the entity, and the first argument is the
                --  aspect definition expression.
 
+               --  Convention
+
                when Aspect_Convention  =>
 
                   --  The aspect may be part of the specification of an import
@@ -1387,30 +1429,28 @@ 
                         Append_To (Arg_List, E_Assoc);
                      end if;
 
-                     Aitem :=
-                       Make_Pragma (Loc,
-                         Pragma_Argument_Associations => Arg_List,
-                         Pragma_Identifier            =>
-                            Make_Identifier (Loc, P_Name));
+                     Make_Aitem_Pragma
+                       (Pragma_Argument_Associations => Arg_List,
+                        Pragma_Name                  => P_Name);
                   end;
 
-               --  The following three aspects can be specified for a
-               --  subprogram body, in which case we generate pragmas for them
-               --  and insert them ahead of local declarations, rather than
-               --  after the body.
+               --  CPU, Interrupt_Priority, Priority
 
+               --  These three aspects can be specified for a subprogram body,
+               --  in which case we generate pragmas for them and insert them
+               --  ahead of local declarations, rather than after the body.
+
                when Aspect_CPU                |
                     Aspect_Interrupt_Priority |
                     Aspect_Priority           =>
 
                   if Nkind (N) = N_Subprogram_Body then
-                     Aitem :=
-                       Make_Pragma (Loc,
-                         Pragma_Argument_Associations => New_List (
-                           Make_Pragma_Argument_Association (Sloc (Expr),
-                             Expression => Relocate_Node (Expr))),
-                         Pragma_Identifier            =>
-                           Make_Identifier (Sloc (Id), Chars (Id)));
+                     Make_Aitem_Pragma
+                       (Pragma_Argument_Associations => New_List (
+                          Make_Pragma_Argument_Association (Sloc (Expr),
+                            Expression => Relocate_Node (Expr))),
+                        Pragma_Name                  => Chars (Id));
+
                   else
                      Aitem :=
                        Make_Attribute_Definition_Clause (Loc,
@@ -1419,18 +1459,18 @@ 
                          Expression => Relocate_Node (Expr));
                   end if;
 
+               --  Warnings
+
                when Aspect_Warnings =>
-                  Aitem :=
-                    Make_Pragma (Loc,
-                      Pragma_Argument_Associations => New_List (
-                        Make_Pragma_Argument_Association (Sloc (Expr),
-                          Expression => Relocate_Node (Expr)),
-                        Make_Pragma_Argument_Association (Loc,
-                          Expression => New_Occurrence_Of (E, Loc))),
-                      Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Chars (Id)),
-                      Class_Present                => Class_Present (Aspect));
 
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Sloc (Expr),
+                         Expression => Relocate_Node (Expr)),
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => New_Occurrence_Of (E, Loc))),
+                     Pragma_Name                  => Chars (Id));
+
                   --  We don't have to play the delay game here, since the only
                   --  values are ON/OFF which don't get analyzed anyway.
 
@@ -1443,6 +1483,8 @@ 
                --  entity, a second argument that is the expression and a third
                --  argument that is an appropriate message.
 
+               --  Invariant, Type_Invariant
+
                when Aspect_Invariant      |
                     Aspect_Type_Invariant =>
 
@@ -1450,16 +1492,13 @@ 
                   --  an invariant must apply to a private type, or appear in
                   --  the private part of a spec and apply to a completion.
 
-                  Aitem :=
-                    Make_Pragma (Loc,
-                      Pragma_Argument_Associations => New_List (
-                        Make_Pragma_Argument_Association (Sloc (Ent),
-                          Expression => Ent),
-                        Make_Pragma_Argument_Association (Sloc (Expr),
-                          Expression => Relocate_Node (Expr))),
-                      Class_Present                => Class_Present (Aspect),
-                      Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Name_Invariant));
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Sloc (Ent),
+                         Expression => Ent),
+                       Make_Pragma_Argument_Association (Sloc (Expr),
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Invariant);
 
                   --  Add message unless exception messages are suppressed
 
@@ -1482,50 +1521,49 @@ 
                --  Case 2d : Aspects that correspond to a pragma with one
                --  argument.
 
+               --  Abstract_State
+
                when Aspect_Abstract_State =>
-                  Aitem :=
-                    Make_Pragma (Loc,
-                      Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Name_Abstract_State),
-                      Pragma_Argument_Associations => New_List (
-                        Make_Pragma_Argument_Association (Loc,
-                          Expression => Relocate_Node (Expr))));
-
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Abstract_State);
                   Delay_Required := False;
 
+               --  Depends
+
                --  Aspect Depends must be delayed because it mentions names
                --  of inputs and output that are classified by aspect Global.
 
                when Aspect_Depends =>
-                  Aitem :=
-                    Make_Pragma (Loc,
-                      Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Name_Depends),
-                      Pragma_Argument_Associations => New_List (
-                        Make_Pragma_Argument_Association (Loc,
-                          Expression => Relocate_Node (Expr))));
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Depends);
 
+               --  Global
+
                --  Aspect Global must be delayed because it can mention names
                --  and benefit from the forward visibility rules applicable to
                --  aspects of subprograms.
 
                when Aspect_Global =>
-                  Aitem :=
-                    Make_Pragma (Loc,
-                      Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Name_Global),
-                      Pragma_Argument_Associations => New_List (
-                        Make_Pragma_Argument_Association (Loc,
-                          Expression => Relocate_Node (Expr))));
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Global);
 
+               --  Relative_Deadline
+
                when Aspect_Relative_Deadline =>
-                  Aitem :=
-                    Make_Pragma (Loc,
-                      Pragma_Argument_Associations => New_List (
-                        Make_Pragma_Argument_Association (Loc,
-                          Expression => Relocate_Node (Expr))),
-                      Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Name_Relative_Deadline));
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                      Pragma_Name                 => Name_Relative_Deadline);
 
                   --  If the aspect applies to a task, the corresponding pragma
                   --  must appear within its declarations, not after.
@@ -1562,6 +1600,8 @@ 
                --  Case 3a: The aspects listed below don't correspond to
                --  pragmas/attributes but do require delayed analysis.
 
+               --  Default_Value, Default_Component_Value
+
                when Aspect_Default_Value           |
                     Aspect_Default_Component_Value =>
                   Aitem := Empty;
@@ -1569,6 +1609,8 @@ 
                --  Case 3b: The aspects listed below don't correspond to
                --  pragmas/attributes and don't need delayed analysis.
 
+               --  Implicit_Dereference
+
                --  For Implicit_Dereference, External_Name and Link_Name, only
                --  the legality checks are done during the analysis, thus no
                --  delay is required.
@@ -1577,15 +1619,21 @@ 
                   Analyze_Aspect_Implicit_Dereference;
                   goto Continue;
 
+               --  External_Name, Link_Name
+
                when Aspect_External_Name |
                     Aspect_Link_Name     =>
                   Analyze_Aspect_External_Or_Link_Name;
                   goto Continue;
 
+               --  Dimension
+
                when Aspect_Dimension =>
                   Analyze_Aspect_Dimension (N, Id, Expr);
                   goto Continue;
 
+               --  Dimension_System
+
                when Aspect_Dimension_System =>
                   Analyze_Aspect_Dimension_System (N, Id, Expr);
                   goto Continue;
@@ -1595,6 +1643,8 @@ 
                --  Pre/Post/Test_Case/Contract_Cases whose corresponding
                --  pragmas take care of the delay.
 
+               --  Pre/Post
+
                --  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.
@@ -1648,16 +1698,12 @@ 
 
                   --  Build the precondition/postcondition pragma
 
-                  Aitem :=
-                    Make_Pragma (Loc,
-                      Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Pname),
-                      Class_Present                => Class_Present (Aspect),
-                      Split_PPC                    => Split_PPC (Aspect),
-                      Pragma_Argument_Associations => New_List (
-                        Make_Pragma_Argument_Association (Eloc,
-                          Chars      => Name_Check,
-                          Expression => Relocate_Node (Expr))));
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Eloc,
+                         Chars      => Name_Check,
+                         Expression => Relocate_Node (Expr))),
+                       Pragma_Name                => Pname);
 
                   --  Add message unless exception messages are suppressed
 
@@ -1726,6 +1772,8 @@ 
                   goto Continue;
                end;
 
+               --  Test_Case
+
                when Aspect_Test_Case => Test_Case : declare
                   Args      : List_Id;
                   Comp_Expr : Node_Id;
@@ -1786,15 +1834,15 @@ 
 
                   --  Build the test-case pragma
 
-                  Aitem :=
-                    Make_Pragma (Loc,
-                      Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Nam),
-                      Pragma_Argument_Associations => Args);
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => Args,
+                     Pragma_Name                  => Nam);
 
                   Delay_Required := False;
                end Test_Case;
 
+               --  Contract_Cases
+
                when Aspect_Contract_Cases => Contract_Cases : declare
                   Case_Guard  : Node_Id;
                   Extra       : Node_Id;
@@ -1860,13 +1908,11 @@ 
 
                   --  Transform the aspect into a pragma
 
-                  Aitem :=
-                    Make_Pragma (Loc,
-                      Pragma_Identifier            =>
-                        Make_Identifier (Loc, Nam),
-                      Pragma_Argument_Associations => New_List (
-                        Make_Pragma_Argument_Association (Loc,
-                          Expression => Relocate_Node (Expr))));
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Nam);
 
                   Delay_Required := False;
                end Contract_Cases;
@@ -1875,9 +1921,11 @@ 
                --  boolean argument.
 
                --  In the general case, the corresponding pragma cannot be
-               --  generated yet because the evaluation of the boolean needs to
-               --  be delayed til the freeze point.
+               --  generated yet because the evaluation of the boolean needs
+               --  to be delayed till the freeze point.
 
+               --  Boolwn_Aspects
+
                when Boolean_Aspects      |
                     Library_Unit_Aspects =>
 
@@ -1954,13 +2002,11 @@ 
                   --  simply insert the pragma, no delay is required.
 
                   if No (Expr) then
-                     Aitem :=
-                       Make_Pragma (Loc,
-                         Pragma_Argument_Associations => New_List (
-                           Make_Pragma_Argument_Association (Sloc (Ent),
-                             Expression => Ent)),
-                         Pragma_Identifier            =>
-                           Make_Identifier (Sloc (Id), Chars (Id)));
+                     Make_Aitem_Pragma
+                       (Pragma_Argument_Associations => New_List (
+                          Make_Pragma_Argument_Association (Sloc (Ent),
+                            Expression => Ent)),
+                        Pragma_Name                  => Chars (Id));
 
                      Delay_Required := False;
 
@@ -1979,8 +2025,16 @@ 
             if Present (Aitem) then
                Set_From_Aspect_Specification (Aitem, True);
 
+               --  For a pragma, keep pointer to aspect
+
                if Nkind (Aitem) = N_Pragma then
                   Set_Corresponding_Aspect (Aitem, Aspect);
+
+                  --  Also set Is_Ignored flag. No need to set Is_Disabled.
+                  --  We checked that right away, and would not get here.
+
+                  Set_Is_Ignored (Aitem, Is_Ignored (Aspect));
+                  pragma Assert (not Is_Disabled (Aspect));
                end if;
             end if;
 
@@ -2000,9 +2054,9 @@ 
                goto Continue;
 
             --  In the context of a compilation unit, we directly put the
-            --  pragma in the Pragmas_After list of the
-            --  N_Compilation_Unit_Aux node (no delay is required here)
-            --  except for aspects on a subprogram body (see below).
+            --  pragma in the Pragmas_After list of the N_Compilation_Unit_Aux
+            --  node (no delay is required here) except for aspects on a
+            --  subprogram body (see below).
 
             elsif Nkind (Parent (N)) = N_Compilation_Unit
               and then (Present (Aitem) or else Is_Boolean_Aspect (Aspect))
@@ -2018,13 +2072,11 @@ 
 
                   if Is_Boolean_Aspect (Aspect) and then No (Aitem) then
                      if Is_True (Static_Boolean (Expr)) then
-                        Aitem :=
-                          Make_Pragma (Loc,
-                            Pragma_Argument_Associations => New_List (
-                              Make_Pragma_Argument_Association (Sloc (Ent),
-                                Expression => Ent)),
-                            Pragma_Identifier            =>
-                              Make_Identifier (Sloc (Id), Chars (Id)));
+                        Make_Aitem_Pragma
+                          (Pragma_Argument_Associations => New_List (
+                             Make_Pragma_Argument_Association (Sloc (Ent),
+                               Expression => Ent)),
+                           Pragma_Name                  => Chars (Id));
 
                         Set_From_Aspect_Specification (Aitem, True);
                         Set_Corresponding_Aspect (Aitem, Aspect);
@@ -2097,7 +2149,7 @@ 
                Insert_After (Ins_Node, Aitem);
                Ins_Node := Aitem;
             end if;
-         end;
+         end Analyze_One_Aspect;
 
       <<Continue>>
          Next (Aspect);