exp_spark.adb (Expand_SPARK_Call): Remove procedure.

2014-01-20  Yannick Moy  <moy@adacore.com>

	* exp_spark.adb (Expand_SPARK_Call): Remove procedure.
	* opt.adb, opt.ads (Full_Expander_Active): Remove function.
	* checks.adb, exp_ch6.adb, exp_ch9.adb, exp_disp.adb, sem_aggr.adb,
	* sem_ch10.adb, sem_ch5.adb, sem_ch6.adb, sem_ch8.adb, sem_ch9.adb,
	* sem_disp.adb, sem_res.adb Replace Full_Expander_Active by
	Expander_Active.

2014-01-20  Yannick Moy  <moy@adacore.com>

	* sinfo.ads Update documentation of GNATprove mode.

From-SVN: r206806

17 files changed, 75 insertions, 122 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 06ed0b9..c40e7e7 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,18 @@
 2014-01-20  Yannick Moy  <moy@adacore.com>
 
+	* exp_spark.adb (Expand_SPARK_Call): Remove procedure.
+	* opt.adb, opt.ads (Full_Expander_Active): Remove function.
+	* checks.adb, exp_ch6.adb, exp_ch9.adb, exp_disp.adb, sem_aggr.adb,
+	* sem_ch10.adb, sem_ch5.adb, sem_ch6.adb, sem_ch8.adb, sem_ch9.adb,
+	* sem_disp.adb, sem_res.adb Replace Full_Expander_Active by
+	Expander_Active.
+
+2014-01-20  Yannick Moy  <moy@adacore.com>
+
+	* sinfo.ads Update documentation of GNATprove mode.
+
+2014-01-20  Yannick Moy  <moy@adacore.com>
+
 	* adabkend.adb, ali-util.adb, errout.adb, exp_ch7.adb,
 	* exp_dbug.adb, freeze.adb, lib-xref.adb, restrict.adb,
 	* sem_attr.adb, sem_ch4.adb, sem_ch5.adb, sem_ch6.adb, sem_ch8.adb,
diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index 328e05e5..4801c12 100644
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -478,7 +478,7 @@ package body Checks is
       --  are cases (e.g. with pragma Debug) where generating the checks
       --  can cause real trouble).
 
-      if not Full_Expander_Active then
+      if not Expander_Active then
          return;
       end if;
 
@@ -960,7 +960,7 @@ package body Checks is
 
          if Backend_Overflow_Checks_On_Target
            or else not Do_Overflow_Check (N)
-           or else not Full_Expander_Active
+           or else not Expander_Active
            or else (Present (Parent (N))
                      and then Nkind (Parent (N)) = N_Type_Conversion
                      and then Integer_Promotion_Possible (Parent (N)))
@@ -1419,7 +1419,7 @@ package body Checks is
       --  Nothing to do if discriminant checks are suppressed or else no code
       --  is to be generated
 
-      if not Full_Expander_Active
+      if not Expander_Active
         or else Discriminant_Checks_Suppressed (T_Typ)
       then
          return;
@@ -1732,7 +1732,7 @@ package body Checks is
 
       --  Proceed here in SUPPRESSED or CHECKED modes
 
-      if Full_Expander_Active
+      if Expander_Active
         and then not Backend_Divide_Checks_On_Target
         and then Check_Needed (Right, Division_Check)
       then
@@ -1803,7 +1803,7 @@ package body Checks is
       Right : constant Node_Id    := Right_Opnd (N);
 
    begin
-      if Full_Expander_Active
+      if Expander_Active
         and then not Backend_Divide_Checks_On_Target
         and then Check_Needed (Right, Division_Check)
       then
@@ -1914,7 +1914,7 @@ package body Checks is
       --  the frontend to expand these checks, which are dealt with directly
       --  in the formal verification backend.
 
-      if not Full_Expander_Active then
+      if not Expander_Active then
          return;
       end if;
 
@@ -2945,7 +2945,7 @@ package body Checks is
          or else (not Length_Checks_Suppressed (Target_Typ));
 
    begin
-      if not Full_Expander_Active then
+      if not Expander_Active then
          return;
       end if;
 
@@ -3052,7 +3052,7 @@ package body Checks is
          or else (not Range_Checks_Suppressed (Target_Typ));
 
    begin
-      if not Full_Expander_Active or else not Checks_On then
+      if not Expander_Active or else not Checks_On then
          return;
       end if;
 
@@ -6290,7 +6290,7 @@ package body Checks is
       --  enhanced to check for an always True value in the condition and to
       --  generate a compilation warning???
 
-      if not Full_Expander_Active or else not Checks_On then
+      if not Expander_Active or else not Checks_On then
          return;
       end if;
 
@@ -8321,7 +8321,7 @@ package body Checks is
    --  Start of processing for Selected_Length_Checks
 
    begin
-      if not Full_Expander_Active then
+      if not Expander_Active then
          return Ret_Result;
       end if;
 
@@ -8871,7 +8871,7 @@ package body Checks is
    --  Start of processing for Selected_Range_Checks
 
    begin
-      if not Full_Expander_Active then
+      if not Expander_Active then
          return Ret_Result;
       end if;
 
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index adc0987..d43d02b 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -9603,7 +9603,7 @@ package body Exp_Ch6 is
       --  may end up with a call that is neither resolved to an entity, nor
       --  an indirect call.
 
-      if not Full_Expander_Active then
+      if not Expander_Active then
          return False;
       end if;
 
diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb
index 8db80bd..cdc1543 100644
--- a/gcc/ada/exp_ch9.adb
+++ b/gcc/ada/exp_ch9.adb
@@ -5813,7 +5813,7 @@ package body Exp_Ch9 is
       Ldecl2 : Node_Id;
 
    begin
-      if Full_Expander_Active then
+      if Expander_Active then
 
          --  If we have no handled statement sequence, we may need to build
          --  a dummy sequence consisting of a null statement. This can be
@@ -6123,7 +6123,7 @@ package body Exp_Ch9 is
       --  barrier just as a protected function, and discard the protected
       --  version of it because it is never called.
 
-      if Full_Expander_Active then
+      if Expander_Active then
          B_F := Build_Barrier_Function (N, Ent, Prot);
          Func := Barrier_Function (Ent);
          Set_Corresponding_Spec (B_F, Func);
@@ -6161,7 +6161,7 @@ package body Exp_Ch9 is
          --  condition does not reference any of the generated renamings
          --  within the function.
 
-         if Full_Expander_Active and then Scope (Entity (Cond)) /= Func then
+         if Expander_Active and then Scope (Entity (Cond)) /= Func then
             Set_Declarations (B_F, Empty_List);
          end if;
 
@@ -12497,7 +12497,7 @@ package body Exp_Ch9 is
          Error_Msg_CRT ("protected body", N);
          return;
 
-      elsif Full_Expander_Active then
+      elsif Expander_Active then
 
          --  Associate discriminals with the first subprogram or entry body to
          --  be expanded.
diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb
index 8ba4704..b4c56ac 100644
--- a/gcc/ada/exp_disp.adb
+++ b/gcc/ada/exp_disp.adb
@@ -696,7 +696,7 @@ package body Exp_Disp is
       --  Expand_Dispatching_Call is called directly from the semantics,
       --  so we only proceed if the expander is active.
 
-      if not Full_Expander_Active
+      if not Expander_Active
 
         --  And there is no need to expand the call if we are compiling under
         --  restriction No_Dispatching_Calls; the semantic analyzer has
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index fb7aad2..e3e875c 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -27,7 +27,6 @@ with Atree;    use Atree;
 with Einfo;    use Einfo;
 with Exp_Dbug; use Exp_Dbug;
 with Exp_Util; use Exp_Util;
-with Sem_Aux;  use Sem_Aux;
 with Sem_Res;  use Sem_Res;
 with Sem_Util; use Sem_Util;
 with Sinfo;    use Sinfo;
@@ -38,10 +37,6 @@ package body Exp_SPARK is
    -- Local Subprograms --
    -----------------------
 
-   procedure Expand_SPARK_Call (N : Node_Id);
-   --  This procedure contains common processing for function and procedure
-   --  calls: replacement of renaming by subprogram renamed
-
    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
    --  Perform name evaluation for a renamed object
 
@@ -71,9 +66,6 @@ package body Exp_SPARK is
               N_Subprogram_Body     =>
             Qualify_Entity_Names (N);
 
-         when N_Subprogram_Call     =>
-            Expand_SPARK_Call (N);
-
          when N_Expanded_Name |
               N_Identifier    =>
             Expand_Potential_Renaming (N);
@@ -88,36 +80,6 @@ package body Exp_SPARK is
       end case;
    end Expand_SPARK;
 
-   -----------------------
-   -- Expand_SPARK_Call --
-   -----------------------
-
-   procedure Expand_SPARK_Call (N : Node_Id) is
-   begin
-      --  If the subprogram is a renaming, replace it in the call with the name
-      --  of the actual subprogram being called. We distinguish renamings from
-      --  inherited primitive operations, which both have an Alias component,
-      --  by looking at the parent node of the entity. The entity for a
-      --  renaming has the function or procedure specification node as
-      --  parent, while an inherited primitive operation has the derived
-      --  type declaration as parent.
-
-      if Nkind (Name (N)) in N_Has_Entity
-        and then Present (Entity (Name (N)))
-      then
-         declare
-            E : constant Entity_Id := Entity (Name (N));
-         begin
-            if Nkind_In (Parent (E), N_Function_Specification,
-                                     N_Procedure_Specification)
-              and then Present (Alias (E))
-            then
-               Set_Entity (Name (N), Ultimate_Alias (E));
-            end if;
-         end;
-      end if;
-   end Expand_SPARK_Call;
-
    ------------------------------------------------
    -- Expand_SPARK_N_Object_Renaming_Declaration --
    ------------------------------------------------
diff --git a/gcc/ada/opt.adb b/gcc/ada/opt.adb
index 298b7e3..0f65614 100644
--- a/gcc/ada/opt.adb
+++ b/gcc/ada/opt.adb
@@ -38,15 +38,6 @@ package body Opt is
    SU : constant := Storage_Unit;
    --  Shorthand for System.Storage_Unit
 
-   --------------------------
-   -- Full_Expander_Active --
-   --------------------------
-
-   function Full_Expander_Active return Boolean is
-   begin
-      return Expander_Active;
-   end Full_Expander_Active;
-
    ----------------------------------
    -- Register_Opt_Config_Switches --
    ----------------------------------
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index ea5f179..2365abd 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -1939,9 +1939,6 @@ package Opt is
    --  this flag, see package Expander. Indeed this flag might more logically
    --  be in the spec of Expander, but it is referenced by Errout, and it
    --  really seems wrong for Errout to depend on Expander.
-   --
-   --  Note: for many purposes, it is more appropriate to test the flag
-   --  Full_Expander_Active, which also checks that SPARK mode is not active.
 
    Static_Dispatch_Tables : Boolean := True;
    --  This flag indicates if the backend supports generation of statically
@@ -2023,15 +2020,6 @@ package Opt is
    --  for integers are limited to the strict minimum with this option. Set by
    --  debug flag -gnatd.D.
 
-   function Full_Expander_Active return Boolean;
-   pragma Inline (Full_Expander_Active);
-   --  Returns the value of (Expander_Active and not SPARK_Mode). This "flag"
-   --  indicates that expansion is fully active, that is, not in the reduced
-   --  mode for SPARK (True) or that expansion is either deactivated, or active
-   --  in the reduced mode for SPARK (False). For more information on full
-   --  expansion, see package Expander. For more information on reduced
-   --  SPARK expansion, see package Exp_SPARK.
-
 private
 
    --  The following type is used to save and restore settings of switches in
diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb
index 6724593..73ebeeb 100644
--- a/gcc/ada/sem_aggr.adb
+++ b/gcc/ada/sem_aggr.adb
@@ -1700,7 +1700,7 @@ package body Sem_Aggr is
             --  performed safely.
 
             if Single_Elmt
-              or else not Full_Expander_Active
+              or else not Expander_Active
               or else In_Spec_Expression
             then
                Analyze_And_Resolve (Expr, Component_Typ);
diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb
index 78520f8..b83bf12 100644
--- a/gcc/ada/sem_ch10.adb
+++ b/gcc/ada/sem_ch10.adb
@@ -2393,7 +2393,7 @@ package body Sem_Ch10 is
          --  expansion is active, because the context may be generic and the
          --  flag not defined yet.
 
-         if Full_Expander_Active then
+         if Expander_Active then
             Insert_After (N,
               Make_Assignment_Statement (Loc,
                 Name =>
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index ec7c12e..b0d59e3 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -2739,7 +2739,7 @@ package body Sem_Ch5 is
 
       if No (Iter)
         or else No (Iterator_Specification (Iter))
-        or else not Full_Expander_Active
+        or else not Expander_Active
       then
          if Present (Iter)
            and then Present (Iterator_Specification (Iter))
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 3f33536..6e1c250 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3200,7 +3200,7 @@ package body Sem_Ch6 is
       --  body may be the rewritting of an expression function, and we need to
       --  verify that the original node is in the source.
 
-      if Full_Expander_Active
+      if Expander_Active
         and then Comes_From_Source (Original_Node (N))
         and then Present (Prot_Typ)
         and then Present (Spec_Id)
@@ -11447,7 +11447,7 @@ package body Sem_Ch6 is
                --  parameter block, and it is this local variable that may
                --  require an actual subtype.
 
-               if Full_Expander_Active then
+               if Expander_Active then
                   Decl := Build_Actual_Subtype (T, Renamed_Object (Formal));
                else
                   Decl := Build_Actual_Subtype (T, Formal);
@@ -11486,7 +11486,7 @@ package body Sem_Ch6 is
             end if;
 
             if Nkind (N) = N_Accept_Statement
-              and then Full_Expander_Active
+              and then Expander_Active
             then
                Set_Actual_Subtype (Renamed_Object (Formal),
                  Defining_Identifier (Decl));
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index 7f60859..98adb1d 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -2203,7 +2203,7 @@ package body Sem_Ch8 is
 
          if Is_Actual
            and then Is_Abstract_Subprogram (Formal_Spec)
-           and then Full_Expander_Active
+           and then Expander_Active
          then
             declare
                Stream_Prim : Entity_Id;
diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb
index b7374ba..316a163 100644
--- a/gcc/ada/sem_ch9.adb
+++ b/gcc/ada/sem_ch9.adb
@@ -1326,7 +1326,7 @@ package body Sem_Ch9 is
       --  for the discriminals and privals and finally a declaration for the
       --  entry family index (if applicable).
 
-      if Full_Expander_Active
+      if Expander_Active
         and then Is_Protected_Type (P_Type)
       then
          Install_Private_Data_Declarations
@@ -2142,7 +2142,7 @@ package body Sem_Ch9 is
 
            --  Also skip if expander is not active
 
-           and then Full_Expander_Active
+           and then Expander_Active
          then
             Expand_N_Protected_Type_Declaration (N);
             Process_Full_View (N, T, Def_Id);
@@ -2990,7 +2990,7 @@ package body Sem_Ch9 is
 
            --  Also skip if expander is not active
 
-           and then Full_Expander_Active
+           and then Expander_Active
          then
             Expand_N_Task_Type_Declaration (N);
             Process_Full_View (N, T, Def_Id);
diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb
index 7b81581..bf4fa8f 100644
--- a/gcc/ada/sem_disp.adb
+++ b/gcc/ada/sem_disp.adb
@@ -1264,7 +1264,7 @@ package body Sem_Disp is
             --  emitted after those tables are built, to prevent access before
             --  elaboration in gigi.
 
-            if Body_Is_Last_Primitive and then Full_Expander_Active then
+            if Body_Is_Last_Primitive and then Expander_Active then
                declare
                   Subp_Body : constant Node_Id := Unit_Declaration_Node (Subp);
                   Elmt      : Elmt_Id;
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 12d9d31..9ebb0bc 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -1762,7 +1762,7 @@ package body Sem_Res is
    --  Start of processing for Replace_Actual_Discriminants
 
    begin
-      if not Full_Expander_Active then
+      if not Expander_Active then
          return;
       end if;
 
@@ -2033,7 +2033,7 @@ package body Sem_Res is
                   --  If we are generating code in distributed mode, perform
                   --  semantic checks against corresponding remote entities.
 
-                  if Full_Expander_Active
+                  if Expander_Active
                     and then Get_PCS_Name /= Name_No_DSA
                   then
                      Check_Subtype_Conformant
@@ -3608,7 +3608,7 @@ package body Sem_Res is
             elsif Nkind (A) = N_Function_Call
               and then Is_Limited_Record (Etype (F))
               and then not Is_Constrained (Etype (F))
-              and then Full_Expander_Active
+              and then Expander_Active
               and then (Is_Controlled (Etype (F)) or else Has_Task (Etype (F)))
             then
                Establish_Transient_Scope (A, Sec_Stack => False);
@@ -3624,7 +3624,7 @@ package body Sem_Res is
 
             elsif Nkind (A) = N_Op_Concat
               and then Nkind (N) = N_Procedure_Call_Statement
-              and then Full_Expander_Active
+              and then Expander_Active
               and then
                 not (Is_Intrinsic_Subprogram (Nam)
                       and then Chars (Nam) = Name_Asm)
@@ -3687,7 +3687,7 @@ package body Sem_Res is
                      --  be removed in the expansion of the wrapped construct.
 
                      if (Is_Controlled (DDT) or else Has_Task (DDT))
-                       and then Full_Expander_Active
+                       and then Expander_Active
                      then
                         Establish_Transient_Scope (A, Sec_Stack => False);
                      end if;
@@ -5756,7 +5756,7 @@ package body Sem_Res is
       then
          null;
 
-      elsif Full_Expander_Active
+      elsif Expander_Active
         and then Is_Type (Etype (Nam))
         and then Requires_Transient_Scope (Etype (Nam))
         and then
@@ -6836,7 +6836,7 @@ package body Sem_Res is
       --  Protected functions can return on the secondary stack, in which
       --  case we must trigger the transient scope mechanism.
 
-      elsif Full_Expander_Active
+      elsif Expander_Active
         and then Requires_Transient_Scope (Etype (Nam))
       then
          Establish_Transient_Scope (N, Sec_Stack => True);
@@ -7139,7 +7139,7 @@ package body Sem_Res is
 
          --  Why the Expander_Active test here ???
 
-         if Full_Expander_Active
+         if Expander_Active
            and then
              (Ekind_In (T, E_Anonymous_Access_Type,
                            E_Anonymous_Access_Subprogram_Type)
@@ -7551,7 +7551,7 @@ package body Sem_Res is
       --  We must preserve the original entity in a generic setting, so that
       --  the legality of the operation can be verified in an instance.
 
-      if not Full_Expander_Active then
+      if not Expander_Active then
          return;
       end if;
 
@@ -8670,7 +8670,7 @@ package body Sem_Res is
       --  transformation while analyzing generic units, as type information
       --  would be lost when reanalyzing the constant node in the instance.
 
-      if Is_Discrete_Type (Typ) and then Full_Expander_Active then
+      if Is_Discrete_Type (Typ) and then Expander_Active then
          if Is_OK_Static_Expression (L) then
             Fold_Uint  (L, Expr_Value (L), Is_Static_Expression (L));
          end if;
@@ -9022,7 +9022,7 @@ package body Sem_Res is
       --  helpful for coverage analysis. However this should not happen in
       --  generics.
 
-      if Full_Expander_Active then
+      if Expander_Active then
          declare
             Reloc_L : constant Node_Id := Relocate_Node (L);
          begin
@@ -9877,7 +9877,7 @@ package body Sem_Res is
       --  expression coincides with the target type.
 
       if Ada_Version >= Ada_2005
-        and then Full_Expander_Active
+        and then Expander_Active
         and then Operand_Typ /= Target_Typ
       then
          declare
@@ -10387,7 +10387,7 @@ package body Sem_Res is
       --  premature (e.g. if the slice is within a transient scope). This needs
       --  to be done only if expansion is enabled.
 
-      elsif Full_Expander_Active then
+      elsif Expander_Active then
          Ensure_Defined (Typ => Slice_Subtype, N => N);
       end if;
    end Set_Slice_Subtype;
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index a54ef6a..173ae54 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -508,18 +508,18 @@ package Sinfo is
    --      simply ignore these nodes, since they are not relevant to the task
    --      of back annotating representation information.
 
-   ----------------
-   -- SPARK Mode --
-   ----------------
+   --------------------
+   -- GNATprove Mode --
+   --------------------
 
-   --  When a file is compiled in SPARK mode (-gnatd.F), a very light expansion
-   --  is performed and the analysis must generate a tree in a form that meets
-   --  additional requirements.
+   --  When a file is compiled in GNATprove mode (-gnatd.F), a very light
+   --  expansion is performed and the analysis must generate a tree in a
+   --  form that meets additional requirements.
 
-   --  The SPARK expansion does two transformations of the tree, that cannot be
-   --  postponed after the frontend semantic analysis:
+   --  This light expansion does two transformations of the tree, that cannot
+   --  be postponed after the frontend semantic analysis:
 
-   --    1. Replace renamings by renamed (object/subprogram). This requires
+   --    1. Replace object renamings by renamed object. This requires
    --       introducing temporaries at the point of the renaming, which must be
    --       properly analyzed.
 
@@ -527,16 +527,16 @@ package Sinfo is
    --       local effects/call-graphs in ALI files, with the completely
    --       qualified names (in particular the suffix to distinguish homonyms).
 
-   --  The tree after SPARK expansion should be fully analyzed semantically,
-   --  which sometimes requires the insertion of semantic pre-analysis, for
-   --  example for subprogram contracts and pragma check/assert. In particular,
-   --  all expression must have their proper type, and semantic links should be
-   --  set between tree nodes (partial to full view, etc.) Some kinds of nodes
-   --  should be either absent, or can be ignored by the formal verification
-   --  backend:
+   --  The tree after this light expansion should be fully analyzed
+   --  semantically, which sometimes requires the insertion of semantic
+   --  pre-analysis, for example for subprogram contracts and pragma
+   --  check/assert. In particular, all expression must have their proper type,
+   --  and semantic links should be set between tree nodes (partial to full
+   --  view, etc.) Some kinds of nodes should be either absent, or can be
+   --  ignored by the formal verification backend:
 
    --      N_Object_Renaming_Declaration: can be ignored safely
-   --      N_Expression_Function:         absent (rewitten)
+   --      N_Expression_Function:         absent (rewritten)
    --      N_Expression_With_Actions:     absent (not generated)
 
    --  SPARK cross-references are generated from the regular cross-references
@@ -544,11 +544,10 @@ package Sinfo is
    --  collected during semantic analysis, in particular on all dereferences.
    --  These SPARK cross-references are output in a separate section of ALI
    --  files, as described in spark_xrefs.adb. They are the basis for the
-   --  computation of data dependences in the formal verification backend.
-   --  This implies that all cross-references should be generated in this mode,
-   --  even those that would not make sense from a user point-of-view, and that
-   --  cross-references that do not lead to data dependences for subprograms
-   --  can be safely ignored.
+   --  computation of data dependences in GNATprove. This implies that all
+   --  cross-references should be generated in this mode, even those that would
+   --  not make sense from a user point-of-view, and that cross-references that
+   --  do not lead to data dependences for subprograms can be safely ignored.
 
    ------------------------
    -- Common Flag Fields --