Patchwork [Ada] Aspect Global

login
register
mail settings
Submitter Arnaud Charlet
Date Jan. 4, 2013, 9:18 a.m.
Message ID <20130104091836.GA24829@adacore.com>
Download mbox | patch
Permalink /patch/209417/
State New
Headers show

Comments

Arnaud Charlet - Jan. 4, 2013, 9:18 a.m.
This patch provides the initial implementation of aspect Global. This construct
is intended for formal verification proofs.

The syntax of the aspect is as follows:

   global_specification ::= (moded_global_list {, moded_global_list})
                            | global_list
                            | null
   moded_global_list    ::= mode_selector => global_list
   global_list          ::= global_item
                            | (global_item {, global_item})
   mode_selector        ::= Input | Output | In_Out | Contract_In
   global_item          ::= name

The semantics of the aspect are as follows:

A global_item of a subprogram shall be a stand alone variable object [that is,
it is not part of a larger object] or it shall be a state abstraction. Each
mode_selector shall occur at most once in a single Global aspect. A function
subprogram may not have a mode_selector of Output or In_Out in its Global
aspect. Global_items in the same Global aspect shall denote distinct entities.  
A global item occurring in a Global aspect of a subprogram aspect specification
shall not have the same defining_identifier as a formal parameter of the
subprogram. A global item of mode in out or out shall not be a Volatile Input
state abstraction (see Abstract State Aspect). A global item of mode in or in
out shall not be a Volatile Output state abstraction.

This patch also corrects the timing of pragma Abstract_State analysis.

------------
-- Source --
------------

--  semantics.ads

package Semantics
   with Abstract_State =>
     ((Input_State  with Volatile, Input),
      (Output_State with Volatile, Output))
is
   type Composite is record
      Comp : Integer;
   end record;
   Var : Composite;

   type Composite_Array is array (1 .. 5) of Composite;
   Arr : Composite_Array;

   procedure Dummy_Proc;
   procedure OK_1
     with Global => (Var, Input_State);
   procedure Error_1
     with Global =>
       (Var.Comp,
        Arr (2),
        Dummy_Proc);
   procedure OK_2
     with Global =>
       (Input  => (Var, Input_State),
        Output => Arr);
   procedure Error_2
     with Global =>
       (Input       => Var,
        Contract_In => Input_State,
        Input       => Arr);
   function OK_3 return Boolean
     with Global =>
       (Input       => Var,
        Contract_In => Input_State);
   function Error_3 return Boolean
     with Global =>
       (In_Out => Arr,
        Output => Var);
   procedure Error_4
     with Global =>
       (Input  => Semantics.Var,
        Output => Var);
   function Error_5 (Formal : Boolean) return Boolean
     with Global => Formal;
   procedure Error_6
     with Global => (In_Out => Input_State);
   procedure Error_7
     with Global => (Output => Input_State);
   procedure Error_8
     with Global => (In_Out => Output_State);
   procedure Error_9
     with Global => (Input => Output_State);
   procedure Error_10
     with Global => Output_State;
   procedure OK_4
     with Global => null;
   procedure Error_11
     with Global => (null, Var);
   procedure Error_12
     with Global => (Var, null, Arr);
   procedure Error_13
     with Global => (Var, null);
end Semantics;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c -gnat12 -gnatd.V semantics.ads
semantics.ads:19:12: global item must denote variable or state
semantics.ads:20:09: global item must denote variable or state
semantics.ads:21:09: global item must denote variable or state
semantics.ads:30:09: duplicate global mode
semantics.ads:37:09: global mode "In_Out" not applicable to functions
semantics.ads:38:09: global mode "Output" not applicable to functions
semantics.ads:42:19: duplicate global item
semantics.ads:44:21: global item cannot reference formal parameter
semantics.ads:46:32: global item of mode In_Out or Output cannot reference Volatile Input state
semantics.ads:48:32: global item of mode In_Out or Output cannot reference Volatile Input state
semantics.ads:50:32: global item of mode In_Out or Input cannot reference Volatile Output state
semantics.ads:52:31: global item of mode In_Out or Input cannot reference Volatile Output state
semantics.ads:54:21: global item of mode In_Out or Input cannot reference Volatile Output state
semantics.ads:58:22: cannot mix null and non-null global items
semantics.ads:60:27: cannot mix null and non-null global items
semantics.ads:62:27: cannot mix null and non-null global items

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

2013-01-04  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb, aspects.ads: Add Aspect_Global to all relevant tables.
	* par-prag.adb: Add pragma Global to the list of pragmas that
	do not need special processing by the parser.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Convert aspect
	Global into a pragma without any form of legality checks. The
	work is done by Analyze_Pragma. The aspect and pragma are both
	marked as needing delayed processing.  Insert the corresponding
	pragma of aspect Abstract_State in the visible declarations of the
	related package.
	(Check_Aspect_At_Freeze_Point): Aspect Global
	does not need processing even though it is marked as delayed.
	Alphabetize the list on aspect names.
	* sem_prag.adb: Add a value for pragma Global in table Sig_Flags.
	(Analyze_Pragma): Add ??? comment about the grammar of pragma
	Abstract_State.  Move the error location from the pragma to the
	state to improve the quality of error placement.  Add legality
	checks for pragma Global.
	* snames.ads-tmpl Add the following specially recognized names

Patch

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 194888)
+++ sem_prag.adb	(working copy)
@@ -789,6 +789,8 @@ 
       procedure S14_Pragma;
       --  Called for all pragmas defined for formal verification to check that
       --  the S14_Extensions flag is set.
+      --  This name needs fixing ??? There is no such thing as an
+      --  "S14_Extensions" flag ???
 
       function Is_Before_First_Decl
         (Pragma_Node : Node_Id;
@@ -6644,6 +6646,8 @@ 
          -- Abstract_State --
          --------------------
 
+         --  ??? no formal grammar available yet
+
          when Pragma_Abstract_State => Abstract_State : declare
             Pack_Id : Entity_Id;
 
@@ -6824,7 +6828,7 @@ 
                --  Any other attempt to declare a state is erroneous
 
                else
-                  Error_Msg_N ("malformed abstract state declaration", N);
+                  Error_Msg_N ("malformed abstract state declaration", State);
                end if;
 
                --  Do not generate a state abstraction entity if it was not
@@ -9946,6 +9950,362 @@ 
             end if;
          end Float_Representation;
 
+         ------------
+         -- Global --
+         ------------
+
+         --  ??? no formal grammar pragma available yet
+
+         when Pragma_Global => Global : declare
+            Subp_Id : Entity_Id;
+
+            Seen : Elist_Id := No_Elist;
+            --  A list containing the entities of all the items processed so
+            --  far. It plays a role in detecting distinct entities.
+
+            --  Flags used to verify the consistency of modes
+
+            Contract_Seen : Boolean := False;
+            In_Out_Seen   : Boolean := False;
+            Input_Seen    : Boolean := False;
+            Output_Seen   : Boolean := False;
+
+            procedure Analyze_Global_List
+              (List        : Node_Id;
+               Global_Mode : Name_Id := Name_Input);
+            --  Verify the legality of a single global list declaration.
+            --  Global_Mode denotes the current mode in effect.
+
+            -------------------------
+            -- Analyze_Global_List --
+            -------------------------
+
+            procedure Analyze_Global_List
+              (List        : Node_Id;
+               Global_Mode : Name_Id := Name_Input)
+            is
+               procedure Analyze_Global_Item
+                 (Item        : Node_Id;
+                  Global_Mode : Name_Id);
+               --  Verify the legality of a single global item declaration.
+               --  Global_Mode denotes the current mode in effect.
+
+               procedure Check_Duplicate_Mode
+                 (Mode   : Node_Id;
+                  Status : in out Boolean);
+               --  Flag Status denotes whether a particular mode has been seen
+               --  while processing a global list. This routine verifies that
+               --  Mode is not a duplicate mode and sets the flag Status.
+
+               procedure Check_Mode_Restriction_In_Function (Mode : Node_Id);
+               --  Mode denotes either In_Out or Output. Depending on the kind
+               --  of the related subprogram, emit an error if those two modes
+               --  apply to a function.
+
+               -------------------------
+               -- Analyze_Global_Item --
+               -------------------------
+
+               procedure Analyze_Global_Item
+                 (Item        : Node_Id;
+                  Global_Mode : Name_Id)
+               is
+                  function Is_Duplicate_Item (Id : Entity_Id) return Boolean;
+                  --  Determine whether Id has already been processed
+
+                  -----------------------
+                  -- Is_Duplicate_Item --
+                  -----------------------
+
+                  function Is_Duplicate_Item (Id : Entity_Id) return Boolean is
+                     Item_Elmt : Elmt_Id;
+
+                  begin
+                     if Present (Seen) then
+                        Item_Elmt := First_Elmt (Seen);
+                        while Present (Item_Elmt) loop
+                           if Node (Item_Elmt) = Id then
+                              return True;
+                           end if;
+
+                           Next_Elmt (Item_Elmt);
+                        end loop;
+                     end if;
+
+                     return False;
+                  end Is_Duplicate_Item;
+
+                  --  Local declarations
+
+                  Id : Entity_Id;
+
+               --  Start of processing for Analyze_Global_Item
+
+               begin
+                  --  Detect one of the following cases
+
+                  --    with Global => (null, Name)
+                  --    with Global => (Name_1, null, Name_2)
+                  --    with Global => (Name, null)
+
+                  if Nkind (Item) = N_Null then
+                     Error_Msg_N
+                       ("cannot mix null and non-null global items", Item);
+                     return;
+                  end if;
+
+                  --  Ensure that the formal parameters are visible when
+                  --  processing an item. This falls out of the general rule
+                  --  of aspects pertaining to subprogram declarations.
+
+                  Push_Scope (Subp_Id);
+                  Install_Formals (Subp_Id);
+                  Analyze (Item);
+                  Pop_Scope;
+
+                  if Is_Entity_Name (Item) then
+                     Id := Entity (Item);
+
+                     --  A global item cannot reference a formal parameter. Do
+                     --  this check first to provide a better error diagnostic.
+
+                     if Is_Formal (Id) then
+                        Error_Msg_N
+                          ("global item cannot reference formal parameter",
+                           Item);
+                        return;
+
+                     --  The only legal references are those to abstract states
+                     --  and variables.
+
+                     elsif not Ekind_In (Entity (Item), E_Abstract_State,
+                                                        E_Variable)
+                     then
+                        Error_Msg_N
+                          ("global item must denote variable or state", Item);
+                        return;
+                     end if;
+
+                  --  Some form of illegal construct masquerading as a name
+
+                  else
+                     Error_Msg_N
+                       ("global item must denote variable or state", Item);
+                     return;
+                  end if;
+
+                  --  The same entity might be referenced through various way.
+                  --  Check the entity of the item rather than the item itself.
+
+                  if Is_Duplicate_Item (Id) then
+                     Error_Msg_N ("duplicate global item", Item);
+
+                  --  Add the entity of the current item to the list of
+                  --  processed items.
+
+                  else
+                     if No (Seen) then
+                        Seen := New_Elmt_List;
+                     end if;
+
+                     Append_Elmt (Id, Seen);
+                  end if;
+
+                  if Ekind (Id) = E_Abstract_State
+                    and then Is_Volatile_State (Id)
+                  then
+                     --  A global item of mode In_Out or Output cannot denote a
+                     --  volatile Input state.
+
+                     if Is_Input_State (Id)
+                       and then (Global_Mode = Name_In_Out
+                                   or else
+                                 Global_Mode = Name_Output)
+                     then
+                        Error_Msg_N
+                          ("global item of mode In_Out or Output cannot " &
+                           "reference Volatile Input state", Item);
+
+                     --  A global item of mode In_Out or Input cannot reference
+                     --  a volatile Output state.
+
+                     elsif Is_Output_State (Id)
+                       and then (Global_Mode = Name_In_Out
+                                   or else
+                                 Global_Mode = Name_Input)
+                     then
+                        Error_Msg_N
+                          ("global item of mode In_Out or Input cannot "
+                           & "reference Volatile Output state", Item);
+                     end if;
+                  end if;
+               end Analyze_Global_Item;
+
+               --------------------------
+               -- Check_Duplicate_Mode --
+               --------------------------
+
+               procedure Check_Duplicate_Mode
+                 (Mode   : Node_Id;
+                  Status : in out Boolean)
+               is
+               begin
+                  if Status then
+                     Error_Msg_N ("duplicate global mode", Mode);
+                  end if;
+
+                  Status := True;
+               end Check_Duplicate_Mode;
+
+               ----------------------------------------
+               -- Check_Mode_Restriction_In_Function --
+               ----------------------------------------
+
+               procedure Check_Mode_Restriction_In_Function (Mode : Node_Id) is
+               begin
+                  if Ekind (Subp_Id) = E_Function then
+                     Error_Msg_Name_1 := Chars (Mode);
+                     Error_Msg_N
+                       ("global mode % not applicable to functions", Mode);
+                  end if;
+               end Check_Mode_Restriction_In_Function;
+
+               --  Local variables
+
+               Assoc : Node_Id;
+               Item  : Node_Id;
+               Mode  : Node_Id;
+
+            --  Start of processing for Analyze_Global_List
+
+            begin
+               --  Single global item declaration
+
+               if Nkind_In (List, N_Identifier, N_Selected_Component) then
+                  Analyze_Global_Item (List, Global_Mode);
+
+               --  Simple global list or moded global list declaration
+
+               elsif Nkind (List) = N_Aggregate then
+
+                  --  The declaration of a simple global list appear as a
+                  --  collection of expressions.
+
+                  if Present (Expressions (List)) then
+                     if Present (Component_Associations (List)) then
+                        Error_Msg_N
+                          ("cannot mix moded and non-moded global lists",
+                           List);
+                     end if;
+
+                     Item := First (Expressions (List));
+                     while Present (Item) loop
+                        Analyze_Global_Item (Item, Global_Mode);
+
+                        Next (Item);
+                     end loop;
+
+                  --  The declaration of a moded global list appears as a
+                  --  collection of component associations where individual
+                  --  choices denote modes.
+
+                  elsif Present (Component_Associations (List)) then
+                     if Present (Expressions (List)) then
+                        Error_Msg_N
+                          ("cannot mix moded and non-moded global lists",
+                           List);
+                     end if;
+
+                     Assoc := First (Component_Associations (List));
+                     while Present (Assoc) loop
+                           Mode := First (Choices (Assoc));
+
+                        if Nkind (Mode) = N_Identifier then
+                           if Chars (Mode) = Name_Contract_In then
+                                 Check_Duplicate_Mode (Mode, Contract_Seen);
+
+                           elsif Chars (Mode) = Name_In_Out then
+                              Check_Duplicate_Mode (Mode, In_Out_Seen);
+                                 Check_Mode_Restriction_In_Function (Mode);
+
+                           elsif Chars (Mode) = Name_Input then
+                                 Check_Duplicate_Mode (Mode, Input_Seen);
+
+                           elsif Chars (Mode) = Name_Output then
+                              Check_Duplicate_Mode (Mode, Output_Seen);
+                                 Check_Mode_Restriction_In_Function (Mode);
+
+                           else
+                              Error_Msg_N ("invalid mode selector", Mode);
+                           end if;
+
+                        else
+                           Error_Msg_N ("invalid mode selector", Mode);
+                        end if;
+
+                        --  Items in a moded list appear as a collection of
+                        --  expressions. Reuse the existing machinery to
+                        --  analyze them.
+
+                        Analyze_Global_List
+                          (List        => Expression (Assoc),
+                           Global_Mode => Chars (Mode));
+
+                        Next (Assoc);
+                     end loop;
+
+                  --  Something went horribly wrong, we have a malformed tree
+
+                  else
+                     raise Program_Error;
+                  end if;
+
+               --  Any other attempt to declare a global item is erroneous
+
+               else
+                  Error_Msg_N ("malformed global list declaration", List);
+               end if;
+            end Analyze_Global_List;
+
+            --  Local variables
+
+            List : Node_Id;
+            Subp : Node_Id;
+
+         --  Start of processing for Global
+
+         begin
+            GNAT_Pragma;
+            S14_Pragma;
+            Check_Arg_Count (1);
+
+            --  Ensure the proper placement of the pragma. Global must be
+            --  associated with a subprogram declaration.
+
+            Subp := Parent (Corresponding_Aspect (N));
+
+            if Nkind (Subp) /= N_Subprogram_Declaration then
+               Pragma_Misplaced;
+               return;
+            end if;
+
+            Subp_Id := Defining_Unit_Name (Specification (Subp));
+            List    := Expression (Arg1);
+
+            --  There is nothing to be done for a null global list
+
+            if Nkind (List) = N_Null then
+               null;
+
+            --  Analyze the various forms of global lists and items. Note that
+            --  some of these may be malformed in which case the analysis emits
+            --  error messages.
+
+            else
+               Analyze_Global_List (List);
+            end if;
+         end Global;
+
          -----------
          -- Ident --
          -----------
@@ -16093,6 +16453,7 @@ 
       Pragma_Fast_Math                      => -1,
       Pragma_Finalize_Storage_Only          =>  0,
       Pragma_Float_Representation           =>  0,
+      Pragma_Global                         => -1,
       Pragma_Ident                          => -1,
       Pragma_Implementation_Defined         => -1,
       Pragma_Implemented                    => -1,
Index: aspects.adb
===================================================================
--- aspects.adb	(revision 194851)
+++ aspects.adb	(working copy)
@@ -269,6 +269,7 @@ 
     Aspect_External_Name                => Aspect_External_Name,
     Aspect_External_Tag                 => Aspect_External_Tag,
     Aspect_Favor_Top_Level              => Aspect_Favor_Top_Level,
+    Aspect_Global                       => Aspect_Global,
     Aspect_Implicit_Dereference         => Aspect_Implicit_Dereference,
     Aspect_Import                       => Aspect_Import,
     Aspect_Independent                  => Aspect_Independent,
Index: aspects.ads
===================================================================
--- aspects.ads	(revision 194851)
+++ aspects.ads	(working copy)
@@ -94,6 +94,7 @@ 
       Aspect_Dynamic_Predicate,
       Aspect_External_Name,
       Aspect_External_Tag,
+      Aspect_Global,                        -- GNAT
       Aspect_Implicit_Dereference,
       Aspect_Input,
       Aspect_Interrupt_Priority,
@@ -231,6 +232,7 @@ 
                              Aspect_Dimension                => True,
                              Aspect_Dimension_System         => True,
                              Aspect_Favor_Top_Level          => True,
+                             Aspect_Global                   => True,
                              Aspect_Inline_Always            => True,
                              Aspect_Lock_Free                => True,
                              Aspect_Object_Size              => True,
@@ -327,6 +329,7 @@ 
                         Aspect_Dynamic_Predicate       => Expression,
                         Aspect_External_Name           => Expression,
                         Aspect_External_Tag            => Expression,
+                        Aspect_Global                  => Expression,
                         Aspect_Implicit_Dereference    => Name,
                         Aspect_Input                   => Name,
                         Aspect_Interrupt_Priority      => Expression,
@@ -404,6 +407,7 @@ 
      Aspect_External_Tag                 => Name_External_Tag,
      Aspect_Export                       => Name_Export,
      Aspect_Favor_Top_Level              => Name_Favor_Top_Level,
+     Aspect_Global                       => Name_Global,
      Aspect_Implicit_Dereference         => Name_Implicit_Dereference,
      Aspect_Import                       => Name_Import,
      Aspect_Independent                  => Name_Independent,
Index: par-prag.adb
===================================================================
--- par-prag.adb	(revision 194851)
+++ par-prag.adb	(working copy)
@@ -1156,6 +1156,7 @@ 
            Pragma_Fast_Math                      |
            Pragma_Finalize_Storage_Only          |
            Pragma_Float_Representation           |
+           Pragma_Global                         |
            Pragma_Ident                          |
            Pragma_Implementation_Defined         |
            Pragma_Implemented                    |
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 194888)
+++ sem_ch13.adb	(working copy)
@@ -1436,7 +1436,7 @@ 
                --  Case 2d : Aspects that correspond to a pragma with one
                --  argument.
 
-               when Aspect_Abstract_State        =>
+               when Aspect_Abstract_State =>
                   Aitem :=
                     Make_Pragma (Loc,
                       Pragma_Identifier            =>
@@ -1447,11 +1447,24 @@ 
 
                   Delay_Required := False;
 
-               when Aspect_Relative_Deadline     =>
+               --  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))));
+
+               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));
@@ -1950,6 +1963,20 @@ 
 
                      Prepend (Aitem, Declarations (N));
 
+                  --  Aspect Abstract_State produces implicit declarations for
+                  --  all state abstraction entities it defines. To emulate
+                  --  this behavior, insert the pragma at the start of the
+                  --  visible declarations of the related package.
+
+                  elsif Nam = Name_Abstract_State
+                    and then Nkind (N) = N_Package_Declaration
+                  then
+                     if No (Visible_Declarations (Specification (N))) then
+                        Set_Visible_Declarations (Specification (N), New_List);
+                     end if;
+
+                     Prepend (Aitem, Visible_Declarations (Specification (N)));
+
                   else
                      if No (Pragmas_After (Aux)) then
                         Set_Pragmas_After (Aux, New_List);
@@ -6887,33 +6914,33 @@ 
               Library_Unit_Aspects =>
             T := Standard_Boolean;
 
+         --  Aspects corresponding to attribute definition clauses
+
+         when Aspect_Address =>
+            T := RTE (RE_Address);
+
          when Aspect_Attach_Handler =>
             T := RTE (RE_Interrupt_ID);
 
+         when Aspect_Bit_Order | Aspect_Scalar_Storage_Order =>
+            T := RTE (RE_Bit_Order);
+
          when Aspect_Convention =>
             return;
 
-         --  Default_Value is resolved with the type entity in question
+         when Aspect_CPU =>
+            T := RTE (RE_CPU_Range);
 
-         when Aspect_Default_Value =>
-            T := Entity (ASN);
-
          --  Default_Component_Value is resolved with the component type
 
          when Aspect_Default_Component_Value =>
             T := Component_Type (Entity (ASN));
 
-         --  Aspects corresponding to attribute definition clauses
+         --  Default_Value is resolved with the type entity in question
 
-         when Aspect_Address =>
-            T := RTE (RE_Address);
+         when Aspect_Default_Value =>
+            T := Entity (ASN);
 
-         when Aspect_Bit_Order | Aspect_Scalar_Storage_Order =>
-            T := RTE (RE_Bit_Order);
-
-         when Aspect_CPU =>
-            T := RTE (RE_CPU_Range);
-
          when Aspect_Dispatching_Domain =>
             T := RTE (RE_Dispatching_Domain);
 
@@ -6923,6 +6950,14 @@ 
          when Aspect_External_Name =>
             T := Standard_String;
 
+         --  Global is a delayed aspect because it may reference names that
+         --  have not been declared yet. There is no action to be taken with
+         --  respect to the aspect itself as the reference checking is done on
+         --  the corresponding pragma.
+
+         when Aspect_Global =>
+            return;
+
          when Aspect_Link_Name =>
             T := Standard_String;
 
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 194852)
+++ snames.ads-tmpl	(working copy)
@@ -494,6 +494,7 @@ 
    Name_Export_Valued_Procedure        : constant Name_Id := N + $; -- GNAT
    Name_External                       : constant Name_Id := N + $; -- GNAT
    Name_Finalize_Storage_Only          : constant Name_Id := N + $; -- GNAT
+   Name_Global                         : constant Name_Id := N + $; -- GNAT
    Name_Ident                          : constant Name_Id := N + $; -- VMS
    Name_Implementation_Defined         : constant Name_Id := N + $; -- GNAT
    Name_Implemented                    : constant Name_Id := N + $; -- Ada 12
@@ -673,6 +674,7 @@ 
    Name_Code                           : constant Name_Id := N + $;
    Name_Component                      : constant Name_Id := N + $;
    Name_Component_Size_4               : constant Name_Id := N + $;
+   Name_Contract_In                    : constant Name_Id := N + $;
    Name_Copy                           : constant Name_Id := N + $;
    Name_D_Float                        : constant Name_Id := N + $;
    Name_Decreases                      : constant Name_Id := N + $;
@@ -695,6 +697,7 @@ 
    Name_GPL                            : constant Name_Id := N + $;
    Name_IEEE_Float                     : constant Name_Id := N + $;
    Name_Ignore                         : constant Name_Id := N + $;
+   Name_In_Out                         : constant Name_Id := N + $;
    Name_Increases                      : constant Name_Id := N + $;
    Name_Info                           : constant Name_Id := N + $;
    Name_Integrity                      : constant Name_Id := N + $;
@@ -1771,6 +1774,7 @@ 
       Pragma_Export_Valued_Procedure,
       Pragma_External,
       Pragma_Finalize_Storage_Only,
+      Pragma_Global,
       Pragma_Ident,
       Pragma_Implementation_Defined,
       Pragma_Implemented,