[multiple changes]

2013-04-11  Matthew Heaney  <heaney@adacore.com>

	* a-cdlili.adb, a-cidlli.adb, a-cbdlli.adb ("="): Increment
	lock counts before entering loop.
	(Find): Ditto.
	(Is_Sorted, Merge, Sort): Ditto.
	(Reverse_Find): Ditto.
	(Splice_Internal): Internal operation to refactor splicing logic.
	(Splice): Some logic moved into Splice_Internal.

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

	* adabkend.adb (Scan_Compiler_Arguments): Do not call
	Set_Output_Object_File_Name in Alfa_Mode
	* gnat1drv.adb (Adjust_Global_Switches): Take Alfa_Mode into account.
	* opt.ads: Fix documentation.

From-SVN: r197771

gcc/ada/ChangeLog

+2013-04-11  Matthew Heaney  <heaney@adacore.com>
+
+	* a-cdlili.adb, a-cidlli.adb, a-cbdlli.adb ("="): Increment
+	lock counts before entering loop.
+	(Find): Ditto.
+	(Is_Sorted, Merge, Sort): Ditto.
+	(Reverse_Find): Ditto.
+	(Splice_Internal): Internal operation to refactor splicing logic.
+	(Splice): Some logic moved into Splice_Internal.
+
+2013-04-11  Johannes Kanig  <kanig@adacore.com>
+
+	* adabkend.adb (Scan_Compiler_Arguments): Do not call
+	Set_Output_Object_File_Name in Alfa_Mode
+	* gnat1drv.adb (Adjust_Global_Switches): Take Alfa_Mode into account.
+	* opt.ads: Fix documentation.
+
 2013-04-11  Robert Dewar  <dewar@adacore.com>
 
 	* sem_res.adb: Minor code reorganization and comment fixes.

gcc/ada/adabkend.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---                     Copyright (C) 2001-2011, AdaCore                     --
+--                     Copyright (C) 2001-2013, AdaCore                     --
 --                                                                          --
 -- 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- --
@@ -234,6 +234,8 @@ package body Adabkend is
             then
                if Is_Switch (Argv) then
                   Fail ("Object file name missing after -gnatO");
+               elsif Alfa_Mode then
+                  Output_File_Name_Seen := True;
                else
                   Set_Output_Object_File_Name (Argv);
                   Output_File_Name_Seen := True;

gcc/ada/gnat1drv.adb

@@ -293,7 +293,10 @@ procedure Gnat1drv is
          Formal_Extensions := True;
       end if;
 
-      if Debug_Flag_Dot_FF then
+      --  Alfa_Mode is activated by default in the gnat2why executable, but
+      --  can also be activated using the -gnatd.F switch.
+
+      if Debug_Flag_Dot_FF or else Alfa_Mode then
          Alfa_Mode := True;
 
          --  Set strict standard interpretation of compiler permissions

gcc/ada/opt.ads

@@ -1982,7 +1982,7 @@ package Opt is
    Alfa_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 Alfa subset of Ada. Set by debug flag -gnatd.F.
+   --  the Alfa subset of Ada. Set by the gnat2why executable.
 
    Frame_Condition_Mode : Boolean := False;
    --  Specific mode to be used in combination with Alfa_Mode. If set to