Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb	(revision 251835)
+++ exp_ch6.adb	(working copy)
@@ -137,7 +137,8 @@
    --  there are no tasks.
 
    function Caller_Known_Size
-     (Func_Call : Node_Id; Result_Subt : Entity_Id) return Boolean;
+     (Func_Call   : Node_Id;
+      Result_Subt : Entity_Id) return Boolean;
    --  True if result subtype is definite, or has a size that does not require
    --  secondary stack usage (i.e. no variant part or components whose type
    --  depends on discriminants). In particular, untagged types with only
@@ -837,11 +838,14 @@
    -----------------------
 
    function Caller_Known_Size
-     (Func_Call : Node_Id; Result_Subt : Entity_Id) return Boolean is
+     (Func_Call   : Node_Id;
+      Result_Subt : Entity_Id) return Boolean
+   is
    begin
-      return (Is_Definite_Subtype (Underlying_Type (Result_Subt))
-              and then No (Controlling_Argument (Func_Call)))
-          or else not Requires_Transient_Scope (Underlying_Type (Result_Subt));
+      return
+          (Is_Definite_Subtype (Underlying_Type (Result_Subt))
+            and then No (Controlling_Argument (Func_Call)))
+        or else not Requires_Transient_Scope (Underlying_Type (Result_Subt));
    end Caller_Known_Size;
 
    --------------------------------
@@ -8081,7 +8085,8 @@
 
       declare
          Definite : constant Boolean :=
-           Caller_Known_Size (Func_Call, Result_Subt);
+                      Caller_Known_Size (Func_Call, Result_Subt);
+
       begin
          --  Create an access type designating the function's result subtype.
          --  We use the type of the original call because it may be a call to
Index: ghost.adb
===================================================================
--- ghost.adb	(revision 251834)
+++ ghost.adb	(working copy)
@@ -281,6 +281,13 @@
                   if Chars (Subp_Id) = Name_uPostconditions then
                      return True;
 
+                  --  The context is the internally built predicate function,
+                  --  which is OK because the real check was done before the
+                  --  predicate function was generated.
+
+                  elsif Is_Predicate_Function (Subp_Id) then
+                     return True;
+
                   else
                      Subp_Decl :=
                        Original_Node (Unit_Declaration_Node (Subp_Id));
@@ -362,10 +369,12 @@
                   return True;
 
                --  An assertion expression pragma is Ghost when it contains a
-               --  reference to a Ghost entity (SPARK RM 6.9(10)).
+               --  reference to a Ghost entity (SPARK RM 6.9(10)), except for
+               --  predicate pragmas (SPARK RM 6.9(11)).
 
-               elsif Assertion_Expression_Pragma (Prag_Id) then
-
+               elsif Assertion_Expression_Pragma (Prag_Id)
+                 and then Prag_Id /= Pragma_Predicate
+               then
                   --  Ensure that the assertion policy and the Ghost policy are
                   --  compatible (SPARK RM 6.9(18)).
 
@@ -464,9 +473,16 @@
                   return True;
 
                --  A reference to a Ghost entity can appear within an aspect
-               --  specification (SPARK RM 6.9(10)).
+               --  specification (SPARK RM 6.9(10)). The precise checking will
+               --  occur when analyzing the corresponding pragma. We make an
+               --  exception for predicate aspects that only allow referencing
+               --  a Ghost entity when the corresponding type declaration is
+               --  Ghost (SPARK RM 6.9(11)).
 
-               elsif Nkind (Par) = N_Aspect_Specification then
+               elsif Nkind (Par) = N_Aspect_Specification
+                 and then not Same_Aspect
+                                (Get_Aspect_Id (Par), Aspect_Predicate)
+               then
                   return True;
 
                elsif Is_OK_Declaration (Par) then
Index: par-ch6.adb
===================================================================
--- par-ch6.adb	(revision 251835)
+++ par-ch6.adb	(working copy)
@@ -855,13 +855,14 @@
 
                   if Is_Non_Empty_List (Aspects) then
                      if Func then
-                        Error_Msg ("aspect specifications must come after "
-                          & "parenthesized expression",
-                            Sloc (First (Aspects)));
+                        Error_Msg
+                          ("aspect specifications must come after "
+                           & "parenthesized expression",
+                           Sloc (First (Aspects)));
                      else
-                        Error_Msg ("aspect specifications must come after "
-                          & "subprogram specification",
-                            Sloc (First (Aspects)));
+                        Error_Msg
+                          ("aspect specifications must come after subprogram "
+                           & "specification", Sloc (First (Aspects)));
                      end if;
                   end if;
 
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 251835)
+++ sem_ch13.adb	(working copy)
@@ -12649,7 +12649,6 @@
    --------------------------------
 
    procedure Resolve_Aspect_Expressions (E : Entity_Id) is
-
       function Resolve_Name (N : Node_Id) return Traverse_Result;
       --  Verify that all identifiers in the expression, with the exception
       --  of references to the current entity, denote visible entities. This
@@ -12668,6 +12667,7 @@
 
       function Resolve_Name (N : Node_Id) return Traverse_Result is
          Dummy : Traverse_Result;
+
       begin
          if Nkind (N) = N_Selected_Component then
             if Nkind (Prefix (N)) = N_Identifier
@@ -12700,6 +12700,8 @@
 
       procedure Resolve_Aspect_Expression is new Traverse_Proc (Resolve_Name);
 
+      --  Local variables
+
       ASN : Node_Id := First_Rep_Item (E);
 
    --  Start of processing for Resolve_Aspect_Expressions
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 251835)
+++ sem_prag.adb	(working copy)
@@ -1205,126 +1205,173 @@
             Item_Is_Output : out Boolean)
          is
          begin
-            Item_Is_Input  := False;
-            Item_Is_Output := False;
+            case Ekind (Item_Id) is
 
-            --  Abstract states
+               --  Abstract states
 
-            if Ekind (Item_Id) = E_Abstract_State then
+               when E_Abstract_State =>
 
-               --  When pragma Global is present, the mode of the state may be
-               --  further constrained by setting a more restrictive mode.
+                  --  When pragma Global is present it determines the mode of
+                  --  the abstract state.
 
-               if Global_Seen then
-                  if Appears_In (Subp_Inputs, Item_Id) then
-                     Item_Is_Input := True;
-                  end if;
+                  if Global_Seen then
+                     Item_Is_Input  := Appears_In (Subp_Inputs, Item_Id);
+                     Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
 
-                  if Appears_In (Subp_Outputs, Item_Id) then
+                  --  Otherwise the state has a default IN OUT mode, because it
+                  --  behaves as a variable.
+
+                  else
+                     Item_Is_Input  := True;
                      Item_Is_Output := True;
                   end if;
 
-               --  Otherwise the state has a default IN OUT mode
+               --  Constants and IN parameters
 
-               else
-                  Item_Is_Input  := True;
-                  Item_Is_Output := True;
-               end if;
+               when E_Constant
+                  | E_Generic_In_Parameter
+                  | E_In_Parameter
+                  | E_Loop_Parameter
+               =>
+                  --  When pragma Global is present it determines the mode
+                  --  of constant objects as inputs (and such objects cannot
+                  --  appear as outputs in the Global contract).
 
-            --  Constants
+                  if Global_Seen then
+                     Item_Is_Input := Appears_In (Subp_Inputs, Item_Id);
+                  else
+                     Item_Is_Input := True;
+                  end if;
 
-            elsif Ekind_In (Item_Id, E_Constant,
-                                     E_Loop_Parameter)
-            then
-               Item_Is_Input := True;
+                  Item_Is_Output := False;
 
-            --  Parameters
+               --  Variables and IN OUT parameters
 
-            elsif Ekind_In (Item_Id, E_Generic_In_Parameter,
-                                     E_In_Parameter)
-            then
-               Item_Is_Input := True;
+               when E_Generic_In_Out_Parameter
+                  | E_In_Out_Parameter
+                  | E_Variable
+               =>
+                  --  When pragma Global is present it determines the mode of
+                  --  the object.
 
-            elsif Ekind_In (Item_Id, E_Generic_In_Out_Parameter,
-                                     E_In_Out_Parameter)
-            then
-               Item_Is_Input  := True;
-               Item_Is_Output := True;
+                  if Global_Seen then
 
-            elsif Ekind (Item_Id) = E_Out_Parameter then
-               if Scope (Item_Id) = Spec_Id then
+                     --  A variable has mode IN when its type is unconstrained
+                     --  or tagged because array bounds, discriminants or tags
+                     --  can be read.
 
-                  --  An OUT parameter of the related subprogram has mode IN
-                  --  if its type is unconstrained or tagged because array
-                  --  bounds, discriminants or tags can be read.
+                     Item_Is_Input :=
+                       Appears_In (Subp_Inputs, Item_Id)
+                         or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
 
-                  if Is_Unconstrained_Or_Tagged_Item (Item_Id) then
-                     Item_Is_Input := True;
+                     Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
+
+                  --  Otherwise the variable has a default IN OUT mode
+
+                  else
+                     Item_Is_Input  := True;
+                     Item_Is_Output := True;
                   end if;
 
-                  Item_Is_Output := True;
+               when E_Out_Parameter =>
 
-               --  An OUT parameter of an enclosing subprogram behaves as a
-               --  read-write variable in which case the mode is IN OUT.
+                  --  An OUT parameter of the related subprogram; it cannot
+                  --  appear in Global.
 
-               else
-                  Item_Is_Input  := True;
-                  Item_Is_Output := True;
-               end if;
+                  if Scope (Item_Id) = Spec_Id then
 
-            --  Protected types
+                     --  The parameter has mode IN if its type is unconstrained
+                     --  or tagged because array bounds, discriminants or tags
+                     --  can be read.
 
-            elsif Ekind (Item_Id) = E_Protected_Type then
+                     Item_Is_Input :=
+                       Is_Unconstrained_Or_Tagged_Item (Item_Id);
 
-               --  A protected type acts as a formal parameter of mode IN when
-               --  it applies to a protected function.
+                     Item_Is_Output := True;
 
-               if Ekind (Spec_Id) = E_Function then
-                  Item_Is_Input := True;
+                  --  An OUT parameter of an enclosing subprogram; it can
+                  --  appear in Global and behaves as a read-write variable.
 
-               --  Otherwise the protected type acts as a formal of mode IN OUT
+                  else
+                     --  When pragma Global is present it determines the mode
+                     --  of the object.
 
-               else
-                  Item_Is_Input  := True;
-                  Item_Is_Output := True;
-               end if;
+                     if Global_Seen then
 
-            --  Task types
+                        --  A variable has mode IN when its type is
+                        --  unconstrained or tagged because array
+                        --  bounds, discriminants or tags can be read.
 
-            elsif Ekind (Item_Id) = E_Task_Type then
-               Item_Is_Input  := True;
-               Item_Is_Output := True;
+                        Item_Is_Input :=
+                          Appears_In (Subp_Inputs, Item_Id)
+                            or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
 
-            --  Variable case
+                        Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
 
-            else pragma Assert (Ekind (Item_Id) = E_Variable);
+                     --  Otherwise the variable has a default IN OUT mode
 
-               --  When pragma Global is present, the mode of the variable may
-               --  be further constrained by setting a more restrictive mode.
+                     else
+                        Item_Is_Input  := True;
+                        Item_Is_Output := True;
+                     end if;
+                  end if;
 
-               if Global_Seen then
+               --  Protected types
 
-                  --  A variable has mode IN when its type is unconstrained or
-                  --  tagged because array bounds, discriminants or tags can be
-                  --  read.
+               when E_Protected_Type =>
+                  if Global_Seen then
 
-                  if Appears_In (Subp_Inputs, Item_Id)
-                    or else Is_Unconstrained_Or_Tagged_Item (Item_Id)
-                  then
-                     Item_Is_Input := True;
+                     --  A variable has mode IN when its type is unconstrained
+                     --  or tagged because array bounds, discriminants or tags
+                     --  can be read.
+
+                     Item_Is_Input :=
+                       Appears_In (Subp_Inputs, Item_Id)
+                         or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
+
+                     Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
+
+                  else
+                     --  A protected type acts as a formal parameter of mode IN
+                     --  when it applies to a protected function.
+
+                     if Ekind (Spec_Id) = E_Function then
+                        Item_Is_Input  := True;
+                        Item_Is_Output := False;
+
+                     --  Otherwise the protected type acts as a formal of mode
+                     --  IN OUT.
+
+                     else
+                        Item_Is_Input  := True;
+                        Item_Is_Output := True;
+                     end if;
                   end if;
 
-                  if Appears_In (Subp_Outputs, Item_Id) then
+               --  Task types
+
+               when E_Task_Type =>
+
+                  --  When pragma Global is present it determines the mode of
+                  --  the object.
+
+                  if Global_Seen then
+                     Item_Is_Input :=
+                       Appears_In (Subp_Inputs, Item_Id)
+                         or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
+
+                     Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
+
+                  --  Otherwise task types act as IN OUT parameters
+
+                  else
+                     Item_Is_Input  := True;
                      Item_Is_Output := True;
                   end if;
 
-               --  Otherwise the variable has a default IN OUT mode
-
-               else
-                  Item_Is_Input  := True;
-                  Item_Is_Output := True;
-               end if;
-            end if;
+               when others =>
+                  raise Program_Error;
+            end case;
          end Find_Role;
 
          ----------------
@@ -5069,7 +5116,7 @@
                --  pragma is inserted in its declarative part.
 
                elsif From_Aspect_Specification (N)
-                 and then  Ent = Current_Scope
+                 and then Ent = Current_Scope
                  and then
                    Nkind (Unit_Declaration_Node (Ent)) = N_Subprogram_Body
                then
@@ -28300,7 +28347,7 @@
          if Nkind (Clause) = N_Null then
             null;
 
-         --  A dependency cause appears as component association
+         --  A dependency clause appears as component association
 
          elsif Nkind (Clause) = N_Component_Association then
             Collect_Dependency_Item
@@ -28424,21 +28471,15 @@
          Subp_Decl := Unit_Declaration_Node (Subp_Id);
          Spec_Id   := Unique_Defining_Entity (Subp_Decl);
 
-         --  Process all [generic] formal parameters
+         --  Process all formal parameters
 
          Formal := First_Entity (Spec_Id);
          while Present (Formal) loop
-            if Ekind_In (Formal, E_Generic_In_Parameter,
-                                 E_In_Out_Parameter,
-                                 E_In_Parameter)
-            then
+            if Ekind_In (Formal, E_In_Out_Parameter, E_In_Parameter) then
                Append_New_Elmt (Formal, Subp_Inputs);
             end if;
 
-            if Ekind_In (Formal, E_Generic_In_Out_Parameter,
-                                 E_In_Out_Parameter,
-                                 E_Out_Parameter)
-            then
+            if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
                Append_New_Elmt (Formal, Subp_Outputs);
 
                --  Out parameters can act as inputs when the related type is
