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.

From-SVN: r206805

1 files changed, 14 insertions, 12 deletions

diff --git a/gcc/ada/expander.adb b/gcc/ada/expander.adb
index a037dd3..1fd1bc8 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;