[multiple changes]

2013-04-11  Johannes Kanig  <kanig@adacore.com>

	* opt.ads New global boolean Frame_Condition_Mode to avoid
	referring to command line switch.
	* gnat1drv.adb (Gnat1drv) set frame condition mode when -gnatd.G
	is present, and disable Code generation in that case. Disable
	ALI file generation when switch is *not* present.

2013-04-11  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Analyze_Expression_Function): Perform the
	pre-analysis on a copy of the expression, to prevent downstream
	visbility issues involving operators and instantiations.

From-SVN: r197758

gcc/ada/ChangeLog

 2013-04-11  Johannes Kanig  <kanig@adacore.com>
 
+	* opt.ads New global boolean Frame_Condition_Mode to avoid
+	referring to command line switch.
+	* gnat1drv.adb (Gnat1drv) set frame condition mode when -gnatd.G
+	is present, and disable Code generation in that case. Disable
+	ALI file generation when switch is *not* present.
+
+2013-04-11  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch6.adb (Analyze_Expression_Function): Perform the
+	pre-analysis on a copy of the expression, to prevent downstream
+	visbility issues involving operators and instantiations.
+
+2013-04-11  Johannes Kanig  <kanig@adacore.com>
+
 	* debug.adb: Reservation and documentation for -gnatd.G switch.
 	* gnat1drv.adb (Adjust_Global_Switches) Take into account -gnatd.G
 	switch, and set ALI file generation accordingly.

gcc/ada/gnat1drv.adb

@@ -302,6 +302,18 @@ procedure Gnat1drv is
             Strict_Alfa_Mode := True;
          end if;
 
+         --  Distinguish between the two modes of gnat2why: frame condition
+         --  generation (generation of ALI files) and translation of Why (no
+         --  ALI files generated). This is done with the switch -gnatd.G,
+         --  which activates frame condition mode. The other changes in
+         --  behavior depending on this switch are done in gnat2why directly.
+
+         if Debug_Flag_Dot_GG then
+            Frame_Condition_Mode := True;
+         else
+            Opt.Disable_ALI_File := True;
+         end if;
+
          --  Turn off inlining, which would confuse formal verification output
          --  and gain nothing.
 
@@ -409,16 +421,6 @@ procedure Gnat1drv is
 
          Tagged_Type_Expansion := False;
 
-         --  Distinguish between the two modes of gnat2why: frame condition
-         --  generation (generation of ALI files) and translation of Why (no
-         --  ALI files generated). This is done with the switch -gnatd.G,
-         --  which activates frame condition mode. The other changes in
-         --  behavior depending on this switch are done in gnat2why directly.
-
-         if not Debug_Flag_Dot_GG then
-            Opt.Disable_ALI_File := True;
-         end if;
-
       end if;
 
       --  Set Configurable_Run_Time mode if system.ads flag set
@@ -1041,10 +1043,11 @@ begin
       elsif Main_Kind in N_Generic_Renaming_Declaration then
          Back_End_Mode := Generate_Object;
 
-      --  It is not an error to analyze (in CodePeer or Alfa modes) a spec
-      --  which requires a body, when the body is not available.
+      --  It is not an error to analyze (in CodePeer mode or Alfa mode with
+      --  generation of Why) a spec which requires a body, when the body is
+      --  not available.
 
-      elsif CodePeer_Mode or Alfa_Mode then
+      elsif CodePeer_Mode or (Alfa_Mode and not Frame_Condition_Mode) then
          Back_End_Mode := Generate_Object;
 
       --  In all other cases (specs which have bodies, generics, and bodies

gcc/ada/opt.ads

@@ -1984,6 +1984,12 @@ package Opt is
    --  generation of Why code for those parts of the input code that belong to
    --  the Alfa subset of Ada. Set by debug flag -gnatd.F.
 
+   Frame_Condition_Mode : Boolean := False;
+   --  Specific mode to be used in combination with Alfa_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.
+
    Strict_Alfa_Mode : Boolean := False;
    --  Interpret compiler permissions as strictly as possible. E.g. base ranges
    --  for integers are limited to the strict minimum with this option. Set by

gcc/ada/sem_ch6.adb

@@ -444,7 +444,12 @@ package body Sem_Ch6 is
             Insert_After (Last (Decls), New_Body);
             Push_Scope (Id);
             Install_Formals (Id);
-            Preanalyze_Spec_Expression (Expression  (Ret), Etype (Id));
+
+            --  Do a preanalysis of the expression on a separate copy, to
+            --  prevent visibility issues later with operators in instances.
+
+            Preanalyze_Spec_Expression
+              (New_Copy_Tree (Expression  (Ret)), Etype (Id));
             End_Scope;
          end;
       end if;