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,
	* sem_prag.adb, sem_res.adb, sem_util.adb Rename SPARK_Mode into
	GNATprove_Mode.
	* sem_ch13.adb: Remove blank.
	* exp_spark.adb, exp_spark.ads (Expand_SPARK_Call): Only replace
	subprograms by alias for renamings, not for inherited primitive
	operations.
	* exp_util.adb (Expand_Subtype_From_Expr): Apply the expansion
	in GNATprove mode.
	(Remove_Side_Effects): Apply the removal in
	GNATprove mode, for the full analysis of expressions.
	* expander.adb (Expand): Call the light SPARK expansion in GNATprove
	mode.
	(Expander_Mode_Restore, Expander_Mode_Save_And_Set): Ignore
	save/restore actions for Expander_Active flag in GNATprove mode,
	similar to what is done in ASIS mode.
	* frontend.adb (Frontend): Generic bodies are instantiated in
	GNATprove mode.
	* gnat1drv.adb (Adjust_Global_Switches): Set operating
	mode to Check_Semantics in GNATprove mode, although a light
	expansion is still performed.
	(Gnat1drv): Set Back_End_Mode to
	Declarations_Only in GNATprove mode, and later on special case
	the GNATprove mode to continue analysis anyway.
	* lib-writ.adb (Write_ALI): Always generate ALI files in
	GNATprove mode.
	* opt.adb, opt.ads (Full_Expander_Active): Make it equivalent to
	Expander_Active.
	(SPARK_Mode): Renamed as GNATprove_Mode.
	* sem_aggr.adb (Aggregate_Constraint_Checks): Add checks in the
	tree in GNATprove_Mode.
	* sem_ch12.adb (Analyze_Package_Instantiation): Always instantiate
	body in GNATprove mode.
	(Need_Subprogram_Instance_Body): Always instantiate body in GNATprove
	mode.
	* sem_ch3.adb (Constrain_Index, Process_Range_Expr_In_Decl):
	Make sure side effects are removed in GNATprove mode.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@206805 138bc75d-0d04-0410-961f-82ee72b054a4

31 files changed, 208 insertions, 169 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index bf0e2994daa..06ed0b9e6b6 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,45 @@
+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,
+	* sem_prag.adb, sem_res.adb, sem_util.adb Rename SPARK_Mode into
+	GNATprove_Mode.
+	* sem_ch13.adb: Remove blank.
+	* exp_spark.adb, exp_spark.ads (Expand_SPARK_Call): Only replace
+	subprograms by alias for renamings, not for inherited primitive
+	operations.
+	* exp_util.adb (Expand_Subtype_From_Expr): Apply the expansion
+	in GNATprove mode.
+	(Remove_Side_Effects): Apply the removal in
+	GNATprove mode, for the full analysis of expressions.
+	* expander.adb (Expand): Call the light SPARK expansion in GNATprove
+	mode.
+	(Expander_Mode_Restore, Expander_Mode_Save_And_Set): Ignore
+	save/restore actions for Expander_Active flag in GNATprove mode,
+	similar to what is done in ASIS mode.
+	* frontend.adb (Frontend): Generic bodies are instantiated in
+	GNATprove mode.
+	* gnat1drv.adb (Adjust_Global_Switches): Set operating
+	mode to Check_Semantics in GNATprove mode, although a light
+	expansion is still performed.
+	(Gnat1drv): Set Back_End_Mode to
+	Declarations_Only in GNATprove mode, and later on special case
+	the GNATprove mode to continue analysis anyway.
+	* lib-writ.adb (Write_ALI): Always generate ALI files in
+	GNATprove mode.
+	* opt.adb, opt.ads (Full_Expander_Active): Make it equivalent to
+	Expander_Active.
+	(SPARK_Mode): Renamed as GNATprove_Mode.
+	* sem_aggr.adb (Aggregate_Constraint_Checks): Add checks in the
+	tree in GNATprove_Mode.
+	* sem_ch12.adb (Analyze_Package_Instantiation): Always instantiate
+	body in GNATprove mode.
+	(Need_Subprogram_Instance_Body): Always instantiate body in GNATprove
+	mode.
+	* sem_ch3.adb (Constrain_Index, Process_Range_Expr_In_Decl):
+	Make sure side effects are removed in GNATprove mode.
+
 2014-01-20  Eric Botcazou  <ebotcazou@adacore.com>
 
 	* gcc-interface/decl.c (gnat_to_gnu_entity) <object>: Robustify tests
diff --git a/gcc/ada/adabkend.adb b/gcc/ada/adabkend.adb
index 4a77920a2d6..4c70a560d8f 100644
--- a/gcc/ada/adabkend.adb
+++ b/gcc/ada/adabkend.adb
@@ -235,12 +235,12 @@ package body Adabkend is
                if Is_Switch (Argv) then
                   Fail ("Object file name missing after -gnatO");
 
-               --  In SPARK_Mode, such an object file is never written, and the
-               --  call to Set_Output_Object_File_Name may fail (e.g. when the
-               --  object file name does not have the expected suffix). So we
-               --  skip that call when SPARK_Mode is set.
+               --  In GNATprove_Mode, such an object file is never written, and
+               --  the call to Set_Output_Object_File_Name may fail (e.g. when
+               --  the object file name does not have the expected suffix). So
+               --  we skip that call when GNATprove_Mode is set.
 
-               elsif SPARK_Mode then
+               elsif GNATprove_Mode then
                   Output_File_Name_Seen := True;
 
                else
diff --git a/gcc/ada/ali-util.adb b/gcc/ada/ali-util.adb
index 92380f8eb35..98f79bafaeb 100644
--- a/gcc/ada/ali-util.adb
+++ b/gcc/ada/ali-util.adb
@@ -274,11 +274,11 @@ package body ALI.Util is
                      Error_Msg ("{ had errors, must be fixed, and recompiled");
                      Set_Name_Table_Info (Afile, Int (No_Unit_Id));
 
-                  --  In formal verification mode, object files are never
-                  --  generated, so No_Object=True is not considered an error.
+                  --  In GNATprove mode, object files are never generated, so
+                  --  No_Object=True is not considered an error.
 
                   elsif ALIs.Table (Idread).No_Object
-                    and then not SPARK_Mode
+                    and then not GNATprove_Mode
                     and then not Ignore_Errors
                   then
                      Error_Msg_File_1 := Withs.Table (W).Sfile;
diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index 2c783b2bddf..ab4dcfe6fa9 100644
--- a/gcc/ada/errout.adb
+++ b/gcc/ada/errout.adb
@@ -239,7 +239,7 @@ package body Errout is
       --  an error status. These errors are handled in the driver of the
       --  verification process instead.
 
-      elsif SPARK_Mode and not Frame_Condition_Mode then
+      elsif GNATprove_Mode and not Frame_Condition_Mode then
          return False;
 
       else
@@ -2970,7 +2970,7 @@ package body Errout is
          --  Suppress "size too small" errors in CodePeer mode and SPARK mode,
          --  since pragma Pack is also ignored in these configurations.
 
-         if CodePeer_Mode or SPARK_Mode then
+         if CodePeer_Mode or GNATprove_Mode then
             return True;
 
          --  When a size is wrong for a frozen type there is no explicit size
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 8449f6aba1f..a5238585b6c 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -937,7 +937,7 @@ package body Exp_Ch7 is
       --  Do not create finalization masters in SPARK mode because they result
       --  in unwanted expansion.
 
-      elsif SPARK_Mode then
+      elsif GNATprove_Mode then
          return;
       end if;
 
@@ -2813,7 +2813,7 @@ package body Exp_Ch7 is
       --  Do not perform this expansion in SPARK mode because it is not
       --  necessary.
 
-      if SPARK_Mode then
+      if GNATprove_Mode then
          return;
       end if;
 
@@ -2975,7 +2975,7 @@ package body Exp_Ch7 is
       --  Do not perform this expansion in SPARK mode because we do not create
       --  finalizers in the first place.
 
-      if SPARK_Mode then
+      if GNATprove_Mode then
          return;
       end if;
 
@@ -3658,7 +3658,7 @@ package body Exp_Ch7 is
       --  this node and enclosed expression are not expanded, so do not apply
       --  any transformations here.
 
-      elsif SPARK_Mode
+      elsif GNATprove_Mode
         and then Nkind (Wrap_Node) = N_Pragma
         and then Get_Pragma_Id (Wrap_Node) = Pragma_Check
       then
diff --git a/gcc/ada/exp_dbug.adb b/gcc/ada/exp_dbug.adb
index 7dd72069aca..7d74ed13fa4 100644
--- a/gcc/ada/exp_dbug.adb
+++ b/gcc/ada/exp_dbug.adb
@@ -1314,7 +1314,7 @@ package body Exp_Dbug is
       --  name as being qualified, as Qualify_Entity_Name may be called more
       --  than once on the same entity.
 
-      elsif SPARK_Mode then
+      elsif GNATprove_Mode then
          if Has_Homonym (Ent) then
             Get_Name_String (Chars (Ent));
             Append_Homonym_Number (Ent);
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index a4415e837e7..fb7aad23397 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -31,7 +31,6 @@ with Sem_Aux;  use Sem_Aux;
 with Sem_Res;  use Sem_Res;
 with Sem_Util; use Sem_Util;
 with Sinfo;    use Sinfo;
-with Stand;    use Stand;
 
 package body Exp_SPARK is
 
@@ -94,51 +93,28 @@ package body Exp_SPARK is
    -----------------------
 
    procedure Expand_SPARK_Call (N : Node_Id) is
-      Call_Node   : constant Node_Id := N;
-      Parent_Subp : Entity_Id;
-
    begin
-      --  Ignore if previous error
-
-      if Nkind (Call_Node) in N_Has_Etype
-        and then Etype (Call_Node) = Any_Type
-      then
-         return;
-      end if;
-
-      --  Call using access to subprogram with explicit dereference
-
-      if Nkind (Name (Call_Node)) = N_Explicit_Dereference then
-         Parent_Subp := Empty;
-
-      --  Case of call to simple entry, where the Name is a selected component
-      --  whose prefix is the task, and whose selector name is the entry name
-
-      elsif Nkind (Name (Call_Node)) = N_Selected_Component then
-         Parent_Subp := Empty;
-
-      --  Case of call to member of entry family, where Name is an indexed
-      --  component, with the prefix being a selected component giving the
-      --  task and entry family name, and the index being the entry index.
-
-      elsif Nkind (Name (Call_Node)) = N_Indexed_Component then
-         Parent_Subp := Empty;
-
-      --  Normal case
-
-      else
-         Parent_Subp := Alias (Entity (Name (Call_Node)));
-      end if;
-
       --  If the subprogram is a renaming, replace it in the call with the name
-      --  of the actual subprogram being called.
-
-      if Present (Parent_Subp) then
-         Parent_Subp := Ultimate_Alias (Parent_Subp);
-
-         --  The below setting of Entity is suspect, see F109-018 discussion???
-
-         Set_Entity (Name (Call_Node), Parent_Subp);
+      --  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;
 
diff --git a/gcc/ada/exp_spark.ads b/gcc/ada/exp_spark.ads
index c422bc73e52..750d66b8722 100644
--- a/gcc/ada/exp_spark.ads
+++ b/gcc/ada/exp_spark.ads
@@ -23,10 +23,9 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
---  This package implements a light expansion which is used in formal
---  verification mode (SPARK_Mode = True). Instead of a complete expansion
---  of nodes for code generation, this SPARK expansion targets generation
---  of intermediate code for formal verification.
+--  This package implements a light expansion which is used in GNATprove mode.
+--  Instead of a complete expansion of nodes for code generation, this light
+--  expansion targets generation of intermediate code for formal verification.
 
 --  Expand_SPARK is called directly by Expander.Expand.
 
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index a14b1bc1e19..5bac112681e 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -2034,12 +2034,22 @@ package body Exp_Util is
       --  may be constants that depend on the bounds of a string literal, both
       --  standard string types and more generally arrays of characters.
 
-      if not Expander_Active
+      --  In GNATprove mode, we also need the more precise subtype to be set.
+
+      if not (Expander_Active or GNATprove_Mode)
         and then (No (Etype (Exp)) or else not Is_String_Type (Etype (Exp)))
       then
          return;
       end if;
 
+      --  In GNATprove mode, Unc_Type might not be complete when analyzing
+      --  a generic unit. As generic units are not analyzed directly in
+      --  GNATprove, return here rather than failing later.
+
+      if GNATprove_Mode and then No (Underlying_Type (Unc_Type)) then
+         return;
+      end if;
+
       if Nkind (Exp) = N_Slice then
          declare
             Slice_Type : constant Entity_Id := Etype (First_Index (Exp_Typ));
@@ -6862,9 +6872,11 @@ package body Exp_Util is
    --  Start of processing for Remove_Side_Effects
 
    begin
-      --  Handle cases in which there is nothing to do
+      --  Handle cases in which there is nothing to do. In GNATprove mode,
+      --  removal of side effects is useful for the light expansion of
+      --  renamings.
 
-      if not Expander_Active then
+      if not (Expander_Active or (Full_Analysis and GNATprove_Mode)) then
          return;
       end if;
 
@@ -7074,7 +7086,7 @@ package body Exp_Util is
          --  free if the resulting value is captured by a variable or a
          --  constant.
 
-         if SPARK_Mode
+         if GNATprove_Mode
            and then Nkind (Parent (Exp)) = N_Object_Declaration
          then
             goto Leave;
@@ -7119,7 +7131,7 @@ package body Exp_Util is
          --  types, use a different approach which ignores the secondary stack
          --  and "copies" the returned object.
 
-         if SPARK_Mode then
+         if GNATprove_Mode then
             Res := New_Reference_To (Def_Id, Loc);
             Ref_Type := Exp_Type;
 
@@ -7156,7 +7168,7 @@ package body Exp_Util is
             --  Do not generate a 'reference in SPARK mode since the access
             --  type is not created in the first place.
 
-            if SPARK_Mode then
+            if GNATprove_Mode then
                New_Exp := E;
 
             --  Otherwise generate reference, marking the value as non-null
diff --git a/gcc/ada/expander.adb b/gcc/ada/expander.adb
index a037dd3790c..1fd1bc8a9ed 100644
--- a/gcc/ada/expander.adb
+++ b/gcc/ada/expander.adb
@@ -88,8 +88,9 @@ package body Expander is
       --  The first is when are not generating code. In this mode the
       --  Full_Analysis flag indicates whether we are performing a complete
       --  analysis, in which case Full_Analysis = True or a pre-analysis in
-      --  which case Full_Analysis = False. See the spec of Sem for more
-      --  info on this.
+      --  which case Full_Analysis = False. See the spec of Sem for more info
+      --  on this. Additionally, the GNATprove_Mode flag indicates that a light
+      --  expansion for formal verification should be used.
       --
       --  The second reason for the Expander_Active flag to be False is that
       --  we are performing a pre-analysis. During pre-analysis all expansion
@@ -107,7 +108,7 @@ package body Expander is
       --  given that the expansion actions that would normally process it will
       --  not take place. This prevents cascaded errors due to stack mismatch.
 
-      if not Expander_Active then
+      if not (Expander_Active or (Full_Analysis and GNATprove_Mode)) then
          Set_Analyzed (N, Full_Analysis);
 
          if Serious_Errors_Detected > 0
@@ -127,10 +128,11 @@ package body Expander is
          Debug_A_Entry ("expanding  ", N);
 
          begin
-            --  In SPARK mode we only need a very limited subset of the usual
-            --  expansions. This limited subset is implemented in Expand_SPARK.
+            --  In GNATprove mode we only need a very limited subset of
+            --  the usual expansions. This limited subset is implemented
+            --  in Expand_SPARK.
 
-            if SPARK_Mode then
+            if GNATprove_Mode then
                Expand_SPARK (N);
 
             --  Here for normal non-SPARK mode
@@ -503,10 +505,10 @@ package body Expander is
 
    procedure Expander_Mode_Restore is
    begin
-      --  Not active (has no effect) in ASIS mode (see comments in spec of
-      --  Expander_Mode_Save_And_Set).
+      --  Not active (has no effect) in ASIS and GNATprove modes (see comments
+      --  in spec of Expander_Mode_Save_And_Set).
 
-      if ASIS_Mode then
+      if ASIS_Mode or GNATprove_Mode then
          return;
       end if;
 
@@ -530,10 +532,10 @@ package body Expander is
 
    procedure Expander_Mode_Save_And_Set (Status : Boolean) is
    begin
-      --  Not active (has no effect) in ASIS mode (see comments in spec of
-      --  Expander_Mode_Save_And_Set).
+      --  Not active (has no effect) in ASIS and GNATprove modes (see comments
+      --  in spec of Expander_Mode_Save_And_Set).
 
-      if ASIS_Mode then
+      if ASIS_Mode or GNATprove_Mode then
          return;
       end if;
 
diff --git a/gcc/ada/expander.ads b/gcc/ada/expander.ads
index df59442186a..6c8c649ac0d 100644
--- a/gcc/ada/expander.ads
+++ b/gcc/ada/expander.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2008, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -150,18 +150,20 @@ package Expander is
    --  Saves the current setting of the Expander_Active flag on an internal
    --  stack and then sets the flag to the given value.
    --
-   --  Note: this routine has no effect in ASIS_Mode. In ASIS_Mode, all
-   --  expansion activity is always off, since we want the original semantic
-   --  tree for ASIS purposes without any expansion. This is achieved by
-   --  setting Expander_Active False in ASIS_Mode. In situations such as
-   --  the call to Instantiate_Bodies in Frontend, Expander_Mode_Save_And_Set
-   --  may be called to temporarily turn the expander on, but this will have
-   --  no effect in ASIS mode.
+   --  Note: this routine has no effect in ASIS and GNATprove modes. In ASIS
+   --  mode, all expansion activity is always off, since we want the original
+   --  semantic tree for ASIS purposes without any expansion. In GNATprove
+   --  mode, a very light expansion is performed on specific nodes. Both are
+   --  achieved by setting Expander_Active False in ASIS and GNATprove modes.
+   --  In situations such as the call to Instantiate_Bodies in Frontend,
+   --  Expander_Mode_Save_And_Set may be called to temporarily turn the
+   --  expander on, but this will have no effect in ASIS and GNATprove modes.
 
    procedure Expander_Mode_Restore;
    --  Restores the setting of the Expander_Active flag using the top entry
    --  pushed onto the stack by Expander_Mode_Save_And_Reset, popping the
-   --  stack, except that if any errors have been detected, then the state
-   --  of the flag is left set to False. Disabled for ASIS_Mode (see above).
+   --  stack, except that if any errors have been detected, then the state of
+   --  the flag is left set to False. Disabled for ASIS and GNATprove modes
+   --  (see above).
 
 end Expander;
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index f6c60678143..122d6b23cf6 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -3280,7 +3280,7 @@ package body Freeze is
            --  general, neither CodePeer not GNATprove care about the
            --  internal representation of objects.
 
-           and then not (CodePeer_Mode or SPARK_Mode)
+           and then not (CodePeer_Mode or GNATprove_Mode)
          then
             --  If implicit packing enabled, do it
 
@@ -4230,7 +4230,7 @@ package body Freeze is
                     and then not Is_Limited_Composite (E)
                     and then not Is_Packed (Root_Type (E))
                     and then not Has_Component_Size_Clause (Root_Type (E))
-                    and then not (CodePeer_Mode or SPARK_Mode)
+                    and then not (CodePeer_Mode or GNATprove_Mode)
                   then
                      --  Compute number of elements in array
 
diff --git a/gcc/ada/frontend.adb b/gcc/ada/frontend.adb
index 8a64134d91d..2d5c36f0119 100644
--- a/gcc/ada/frontend.adb
+++ b/gcc/ada/frontend.adb
@@ -362,7 +362,7 @@ begin
 
          if Operating_Mode = Generate_Code
            or else (Operating_Mode = Check_Semantics
-                     and then ASIS_Mode)
+                     and then (ASIS_Mode or GNATprove_Mode))
          then
             Instantiate_Bodies;
          end if;
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 24341acd991..f1bc2f802d6 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -299,15 +299,16 @@ procedure Gnat1drv is
          Formal_Extensions := True;
       end if;
 
-      --  Enable SPARK_Mode when using -gnatd.F switch
+      --  Enable GNATprove_Mode when using -gnatd.F switch
 
       if Debug_Flag_Dot_FF then
-         SPARK_Mode := True;
+         GNATprove_Mode := True;
       end if;
 
-      --  SPARK_Mode is also activated by default in the gnat2why executable
+      --  GNATprove_Mode is also activated by default in the gnat2why
+      --  executable.
 
-      if SPARK_Mode then
+      if GNATprove_Mode then
 
          --  Set strict standard interpretation of compiler permissions
 
@@ -384,11 +385,10 @@ procedure Gnat1drv is
 
          Polling_Required := False;
 
-         --  Set operating mode to Generate_Code, but full front-end expansion
-         --  is not desirable in SPARK mode, so a light expansion is performed
-         --  instead.
+         --  Set operating mode to Check_Semantics, but a light front-end
+         --  expansion is still performed.
 
-         Operating_Mode := Generate_Code;
+         Operating_Mode := Check_Semantics;
 
          --  Skip call to gigi
 
@@ -1054,17 +1054,13 @@ begin
       elsif CodePeer_Mode then
          Back_End_Mode := Generate_Object;
 
-      --  It is not an error to analyze in SPARK mode a spec which requires a
-      --  body, when the body is not available. During frame condition
+      --  It is not an error to analyze in GNATprove mode a spec which requires
+      --  a body, when the body is not available. During frame condition
       --  generation, the corresponding ALI file is generated. During
       --  translation to Why, Why code is generated for the spec.
 
-      elsif SPARK_Mode then
-         if Frame_Condition_Mode then
-            Back_End_Mode := Declarations_Only;
-         else
-            Back_End_Mode := Generate_Object;
-         end if;
+      elsif GNATprove_Mode then
+         Back_End_Mode := Declarations_Only;
 
       --  In all other cases (specs which have bodies, generics, and bodies
       --  where subunits are missing), we cannot generate code and we generate
@@ -1168,10 +1164,11 @@ begin
       --  since representations are largely symbolic there.
 
       if Back_End_Mode = Declarations_Only
-        and then (not (Back_Annotate_Rep_Info or Generate_SCIL)
-                   or else Main_Kind = N_Subunit
-                   or else Targparm.Frontend_Layout_On_Target
-                   or else Targparm.VM_Target /= No_VM)
+           and then
+         (not (Back_Annotate_Rep_Info or Generate_SCIL or GNATprove_Mode)
+           or else Main_Kind = N_Subunit
+           or else Targparm.Frontend_Layout_On_Target
+           or else Targparm.VM_Target /= No_VM)
       then
          Sem_Ch13.Validate_Unchecked_Conversions;
          Sem_Ch13.Validate_Address_Clauses;
diff --git a/gcc/ada/lib-writ.adb b/gcc/ada/lib-writ.adb
index f794162e20b..015c628b87b 100644
--- a/gcc/ada/lib-writ.adb
+++ b/gcc/ada/lib-writ.adb
@@ -841,7 +841,7 @@ package body Lib.Writ is
               --  files, which are required to compute frame conditions
               --  of subprograms.
 
-              or else SPARK_Mode
+              or else GNATprove_Mode
             then
                Write_Info_Tab (25);
 
@@ -973,9 +973,10 @@ package body Lib.Writ is
 
       --  If we are not generating code, and there is an up to date ALI file
       --  file accessible, read it, and acquire the compilation arguments from
-      --  this file.
+      --  this file. In GNATprove mode, always generate the ALI file, which
+      --  contains a special section for formal verification.
 
-      if Operating_Mode /= Generate_Code then
+      if Operating_Mode /= Generate_Code and then not GNATprove_Mode then
          if Up_To_Date_ALI_File_Exists then
             Update_Tables_From_ALI_File;
             return;
@@ -1488,7 +1489,7 @@ package body Lib.Writ is
 
       --  Output SPARK cross-reference information if needed
 
-      if Opt.Xref_Active and then SPARK_Mode then
+      if Opt.Xref_Active and then GNATprove_Mode then
          SPARK_Specific.Collect_SPARK_Xrefs (Sdep_Table => Sdep_Table,
                                              Num_Sdep   => Num_Sdep);
          SPARK_Specific.Output_SPARK_Xrefs;
diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb
index 972d9637b74..4cf52c9bd2b 100644
--- a/gcc/ada/lib-xref.adb
+++ b/gcc/ada/lib-xref.adb
@@ -644,7 +644,7 @@ package body Lib.Xref is
             --  in SPARK mode when the related context comes from an instance.
 
            or else
-             (SPARK_Mode
+             (GNATprove_Mode
                 and then In_Extended_Main_Code_Unit (N)
                 and then (Typ = 'm' or else Typ = 'r' or else Typ = 's'))
          then
@@ -899,7 +899,7 @@ package body Lib.Xref is
          and then
            (Instantiation_Location (Sloc (N)) = No_Location
              or else Typ = 'i'
-             or else SPARK_Mode)
+             or else GNATprove_Mode)
 
         --  Ignore dummy references
 
@@ -986,7 +986,7 @@ package body Lib.Xref is
          --  the renaming, which is needed to compute a valid set of effects
          --  (reads, writes) for the enclosing subprogram.
 
-         if SPARK_Mode then
+         if GNATprove_Mode then
             Ent := Get_Through_Renamings (Ent);
 
             --  If no enclosing object, then it could be a reference to any
@@ -1015,7 +1015,7 @@ package body Lib.Xref is
             Actual_Typ := 'P';
          end if;
 
-         if SPARK_Mode then
+         if GNATprove_Mode then
             Ref := Sloc (Nod);
             Def := Sloc (Ent);
 
diff --git a/gcc/ada/opt.adb b/gcc/ada/opt.adb
index 9f1f2d84a80..298b7e3413f 100644
--- a/gcc/ada/opt.adb
+++ b/gcc/ada/opt.adb
@@ -44,7 +44,7 @@ package body Opt is
 
    function Full_Expander_Active return Boolean is
    begin
-      return Expander_Active and not SPARK_Mode;
+      return Expander_Active;
    end Full_Expander_Active;
 
    ----------------------------------
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 06d9a4bcbab..ea5f1796eb5 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -1996,7 +1996,7 @@ package Opt is
    -----------------------------------
 
    Frame_Condition_Mode : Boolean := False;
-   --  Specific mode to be used in combination with SPARK_Mode. If set to
+   --  Specific mode to be used in combination with GNATprove_Mode. If set to
    --  true, ALI files containing the frame conditions (global effects) are
    --  generated, and Why files are *not* generated. If not true, Why files
    --  are generated. Set by debug flag -gnatd.G.
@@ -2010,7 +2010,7 @@ package Opt is
    --  The mode applicable to the whole compilation. The global mode can be set
    --  in a configuration file such as gnat.adc.
 
-   SPARK_Mode : Boolean := False;
+   GNATprove_Mode : Boolean := False;
    --  Specific compiling mode targeting formal verification through the
    --  generation of Why code for those parts of the input code that belong to
    --  the SPARK 2014 subset of Ada. Set True by the gnat2why executable or by
diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb
index 668c4440d8d..ff2d7eb93a6 100644
--- a/gcc/ada/restrict.adb
+++ b/gcc/ada/restrict.adb
@@ -538,7 +538,7 @@ package body Restrict is
       --  set in gnat1drv.adb so that we have consistency between each
       --  compilation.
 
-      if CodePeer_Mode or SPARK_Mode then
+      if CodePeer_Mode or GNATprove_Mode then
          return;
       end if;
 
diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb
index 5aec38a32d0..672459307f6 100644
--- a/gcc/ada/sem_aggr.adb
+++ b/gcc/ada/sem_aggr.adb
@@ -454,10 +454,14 @@ package body Sem_Aggr is
          Check_Unset_Reference (Exp);
       end if;
 
-      --  This is really expansion activity, so make sure that expansion
-      --  is on and is allowed.
+      --  This is really expansion activity, so make sure that expansion is
+      --  on and is allowed. In GNATprove mode, we also want check flags to be
+      --  added in the tree, so that the formal verification can rely on those
+      --  to be present.
 
-      if not Expander_Active or else In_Spec_Expression then
+      if not (Expander_Active or GNATprove_Mode)
+        or In_Spec_Expression
+      then
          return;
       end if;
 
@@ -996,10 +1000,10 @@ package body Sem_Aggr is
       --  frozen so that initialization procedures can properly be called
       --  in the resolution that follows.  The replacement of boxes with
       --  initialization calls is properly an expansion activity but it must
-      --  be done during revolution.
+      --  be done during resolution.
 
       if Expander_Active
-        and then  Present (Component_Associations (N))
+        and then Present (Component_Associations (N))
       then
          declare
             Comp : Node_Id;
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 231d0b2e296..d6ca5972734 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -4499,7 +4499,7 @@ package body Sem_Attr is
          --  not suffer from the out-of-order issue described above. Thus, this
          --  expansion is skipped in SPARK mode.
 
-         if not Is_Entity_Name (P) and then not SPARK_Mode then
+         if not Is_Entity_Name (P) and then not GNATprove_Mode then
             P_Type := Base_Type (P_Type);
             Set_Etype (N, P_Type);
             Set_Etype (P, P_Type);
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 1572e4ff6dc..f509ba460ca 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -3616,7 +3616,7 @@ package body Sem_Ch12 is
 
          --  We instantiate the body if we are generating code, if we are
          --  generating cross-reference information, or if we are building
-         --  trees for ASIS use.
+         --  trees for ASIS use or GNATprove use.
 
          declare
             Enclosing_Body_Present : Boolean := False;
@@ -3724,7 +3724,7 @@ package body Sem_Ch12 is
                 and then not Inline_Now
                 and then (Operating_Mode = Generate_Code
                            or else (Operating_Mode = Check_Semantics
-                                     and then ASIS_Mode));
+                                     and then (ASIS_Mode or GNATprove_Mode)));
 
             --  If front_end_inlining is enabled, do not instantiate body if
             --  within a generic context.
@@ -4390,17 +4390,18 @@ package body Sem_Ch12 is
            or else Is_Inlined (Subp)
            or else Is_Inlined (Alias (Subp)))
 
-        --  Must be generating code or analyzing code in ASIS mode
+        --  Must be generating code or analyzing code in ASIS mode or GNATprove
+        --  mode.
 
         and then (Operating_Mode = Generate_Code
                    or else (Operating_Mode = Check_Semantics
-                             and then ASIS_Mode))
+                             and then (ASIS_Mode or GNATprove_Mode)))
 
         --  The body is needed when generating code (full expansion), in ASIS
-        --  mode for other tools, and in SPARK mode (special expansion) for
+        --  mode for other tools, and in GNATprove mode (special expansion) for
         --  formal verification of the body itself.
 
-        and then (Expander_Active or ASIS_Mode)
+        and then (Expander_Active or ASIS_Mode or GNATprove_Mode)
 
         --  No point in inlining if ABE is inevitable
 
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 15862442175..fa5ed8d2290 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -2718,7 +2718,7 @@ package body Sem_Ch13 is
                      Prepend (Aitem,
                        Visible_Declarations (Specification (N)));
 
-                  elsif Nkind (N) =  N_Package_Instantiation then
+                  elsif Nkind (N) = N_Package_Instantiation then
                      declare
                         Spec : constant Node_Id :=
                                  Specification (Instance_Spec (N));
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 01d6dddd102..86e233bbe52 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -10084,7 +10084,7 @@ package body Sem_Ch3 is
                --  SPARK mode. Since this is legal code with respect to theorem
                --  proving, do not emit the error.
 
-               if SPARK_Mode
+               if GNATprove_Mode
                  and then Nkind (Exp) = N_Function_Call
                  and then Nkind (Parent (Exp)) = N_Object_Declaration
                  and then not Comes_From_Source
@@ -12223,12 +12223,12 @@ package body Sem_Ch3 is
          --  needed, since checks may cause duplication of the expressions
          --  which must not be reevaluated.
 
-         --  The forced evaluation removes side effects from expressions,
-         --  which should occur also in SPARK mode. Otherwise, we end up with
+         --  The forced evaluation removes side effects from expressions, which
+         --  should occur also in GNATprove mode. Otherwise, we end up with
          --  unexpected insertions of actions at places where this is not
          --  supposed to occur, e.g. on default parameters of a call.
 
-         if Expander_Active then
+         if Expander_Active or GNATprove_Mode then
             Force_Evaluation (Low_Bound (R));
             Force_Evaluation (High_Bound (R));
          end if;
@@ -18865,11 +18865,11 @@ package body Sem_Ch3 is
             --  duplication of the expression without forcing evaluation.
 
             --  The forced evaluation removes side effects from expressions,
-            --  which should occur also in SPARK mode. Otherwise, we end up
+            --  which should occur also in GNATprove mode. Otherwise, we end up
             --  with unexpected insertions of actions at places where this is
             --  not supposed to occur, e.g. on default parameters of a call.
 
-            if Expander_Active then
+            if Expander_Active or GNATprove_Mode then
                Force_Evaluation (Lo);
                Force_Evaluation (Hi);
             end if;
@@ -18980,11 +18980,11 @@ package body Sem_Ch3 is
       --  Case of other than an explicit N_Range node
 
       --  The forced evaluation removes side effects from expressions, which
-      --  should occur also in SPARK mode. Otherwise, we end up with unexpected
-      --  insertions of actions at places where this is not supposed to occur,
-      --  e.g. on default parameters of a call.
+      --  should occur also in GNATprove mode. Otherwise, we end up with
+      --  unexpected insertions of actions at places where this is not
+      --  supposed to occur, e.g. on default parameters of a call.
 
-      elsif Expander_Active then
+      elsif Expander_Active or GNATprove_Mode then
          Get_Index_Bounds (R, Lo, Hi);
          Force_Evaluation (Lo);
          Force_Evaluation (Hi);
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 52aa233746b..d458192c63b 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -1823,7 +1823,7 @@ package body Sem_Ch4 is
       --  In formal verification mode, keep track of all reads and writes
       --  through explicit dereferences.
 
-      if SPARK_Mode then
+      if GNATprove_Mode then
          SPARK_Specific.Generate_Dereference (N);
       end if;
 
@@ -4613,7 +4613,7 @@ package body Sem_Ch4 is
                      --  In SPARK mode, this is made into an error to simplify
                      --  the processing of the formal verification backend.
 
-                     if SPARK_Mode then
+                     if GNATprove_Mode then
                         Apply_Compile_Time_Constraint_Error
                           (N, "component not present in }",
                            CE_Discriminant_Check_Failed,
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index a29aece272c..ec7c12e8df6 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -1712,7 +1712,7 @@ package body Sem_Ch5 is
         --  Do not perform this expansion in SPARK mode, since the formal
         --  verification directly deals with the source form of the iterator.
 
-        and then not SPARK_Mode
+        and then not GNATprove_Mode
       then
          declare
             Id   : constant Entity_Id := Make_Temporary (Loc, 'R', Iter_Name);
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 3b5eee1680b..3f335360573 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -1151,7 +1151,7 @@ package body Sem_Ch6 is
          --  prepares the contract assertions for generic subprograms or for
          --  ASIS. Do not generate contract checks in SPARK mode.
 
-         if not SPARK_Mode then
+         if not GNATprove_Mode then
             Expand_Subprogram_Contract (N, Gen_Id, Body_Id);
          end if;
 
@@ -3188,7 +3188,7 @@ package body Sem_Ch6 is
       --  prepares the contract assertions for generic subprograms or for ASIS.
       --  Do not generate contract checks in SPARK mode.
 
-      if not SPARK_Mode then
+      if not GNATprove_Mode then
          Expand_Subprogram_Contract (N, Spec_Id, Body_Id);
       end if;
 
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index 61d97667840..7f60859a79b 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -5079,7 +5079,7 @@ package body Sem_Ch8 is
 
             if Is_Object (E)
               and then Present (Renamed_Object (E))
-              and then not SPARK_Mode
+              and then not GNATprove_Mode
             then
                Generate_Reference (E, N);
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 19d88778715..d08f13319b3 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -4556,7 +4556,7 @@ package body Sem_Prag is
             --  N_Contract node.
 
             if Acts_As_Spec (PO)
-              and then (SPARK_Mode or Formal_Extensions)
+              and then (GNATprove_Mode or Formal_Extensions)
             then
                declare
                   Prag : constant Node_Id := New_Copy_Tree (N);
@@ -4596,7 +4596,7 @@ package body Sem_Prag is
             --  where there is no later point at which the aspect will be
             --  analyzed.
 
-            if SPARK_Mode or else ASIS_Mode then
+            if GNATprove_Mode or else ASIS_Mode then
                Analyze_Pre_Post_Condition_In_Decl_Part
                  (N, Defining_Entity (Unit (Parent (PO))));
             end if;
@@ -8345,7 +8345,9 @@ package body Sem_Prag is
          --  user code: we want to generate checks for analysis purposes, as
          --  set respectively by -gnatC and -gnatd.F
 
-         if (CodePeer_Mode or SPARK_Mode) and then Comes_From_Source (N) then
+         if (CodePeer_Mode or GNATprove_Mode)
+           and then Comes_From_Source (N)
+         then
             return;
          end if;
 
@@ -13700,7 +13702,7 @@ package body Sem_Prag is
             --  in these modes.
 
             if not Restriction_Active (No_Initialize_Scalars)
-              and then not (CodePeer_Mode or SPARK_Mode)
+              and then not (CodePeer_Mode or GNATprove_Mode)
             then
                Init_Or_Norm_Scalars := True;
                Initialize_Scalars := True;
@@ -13819,7 +13821,7 @@ package body Sem_Prag is
             --  Pragma always active unless in CodePeer or SPARK mode, since
             --  this causes walk order issues.
 
-            if not (CodePeer_Mode or SPARK_Mode) then
+            if not (CodePeer_Mode or GNATprove_Mode) then
                Process_Inline (Enabled);
             end if;
 
@@ -15460,7 +15462,7 @@ package body Sem_Prag is
             --  incorrect negative results in SPARK mode, so ignore this pragma
             --  in these modes.
 
-            if not (CodePeer_Mode or SPARK_Mode) then
+            if not (CodePeer_Mode or GNATprove_Mode) then
                Normalize_Scalars := True;
                Init_Or_Norm_Scalars := True;
             end if;
@@ -15921,7 +15923,7 @@ package body Sem_Prag is
                   --  complex front-end expansions related to pragma Pack,
                   --  so disable handling of pragma Pack in these cases.
 
-                  if CodePeer_Mode or SPARK_Mode then
+                  if CodePeer_Mode or GNATprove_Mode then
                      null;
 
                   --  Don't attempt any packing for VM targets. We possibly
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 9a76e04adf6..12d9d316811 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -1693,7 +1693,7 @@ package body Sem_Res is
       --  case of Ada 2012 constructs such as quantified expressions, which are
       --  expanded in two separate steps.
 
-      if SPARK_Mode then
+      if GNATprove_Mode then
          Analyze_And_Resolve (N, T);
       else
          Analyze_And_Resolve (N, T, Suppress => All_Checks);
@@ -4206,7 +4206,7 @@ package body Sem_Res is
               --  in scope at the point of reference, so the reference should
               --  be ignored for computing effects of subprograms.
 
-              and then not SPARK_Mode
+              and then not GNATprove_Mode
             then
                Set_Entity (Selector_Name (Parent (A)), F);
                Generate_Reference (F, Selector_Name (Parent (A)));
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 08acd702caf..7a1920c6c0a 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -12802,7 +12802,7 @@ package body Sem_Util is
                --  In formal verification mode, keep track of all reads and
                --  writes through explicit dereferences.
 
-               if SPARK_Mode then
+               if GNATprove_Mode then
                   SPARK_Specific.Generate_Dereference (N, 'm');
                end if;
 
@@ -12897,11 +12897,12 @@ package body Sem_Util is
 
                --  Generate a reference only if the assignment comes from
                --  source. This excludes, for example, calls to a dispatching
-               --  assignment operation when the left-hand side is tagged.
+               --  assignment operation when the left-hand side is tagged. In
+               --  GNATprove mode, we need those references also on generated
+               --  code, as these are used to compute the local effects of
+               --  subprograms.
 
-               --  Why is SPARK mode different here ???
-
-               if Modification_Comes_From_Source or SPARK_Mode then
+               if Modification_Comes_From_Source or GNATprove_Mode then
                   Generate_Reference (Ent, Exp, 'm');
 
                   --  If the target of the assignment is the bound variable