[multiple changes]

2013-04-11  Robert Dewar  <dewar@adacore.com>

	* sem_ch6.adb: Minor reformatting.

2013-04-11  Yannick Moy  <moy@adacore.com>

	* ali-util.adb (Read_Withed_ALIs): Do not consider it an error to
	read ALI files with No_Object=True in Alfa mode.
	* gnat1drv.adb: Set appropriately Back_End_Mode in Alfa mode, whether
	this is during frame condition generation of translation to Why.

2013-04-11  Robert Dewar  <dewar@adacore.com>

	* exp_ch4.adb: Minor code reorganization
	* types.ads: Minor reformatting.

From-SVN: r197759

gcc/ada/ChangeLog

+2013-04-11  Robert Dewar  <dewar@adacore.com>
+
+	* sem_ch6.adb: Minor reformatting.
+
+2013-04-11  Yannick Moy  <moy@adacore.com>
+
+	* ali-util.adb (Read_Withed_ALIs): Do not consider it an error to
+	read ALI files with No_Object=True in Alfa mode.
+	* gnat1drv.adb: Set appropriately Back_End_Mode in Alfa mode, whether
+	this is during frame condition generation of translation to Why.
+
+2013-04-11  Robert Dewar  <dewar@adacore.com>
+
+	* exp_ch4.adb: Minor code reorganization
+	* types.ads: Minor reformatting.
+
 2013-04-11  Johannes Kanig  <kanig@adacore.com>
 
 	* opt.ads New global boolean Frame_Condition_Mode to avoid

gcc/ada/ali-util.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, 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- --
@@ -272,7 +272,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.
+
                   elsif ALIs.Table (Idread).No_Object
+                    and then not Alfa_Mode
                     and then not Ignore_Errors
                   then
                      Error_Msg_File_1 := Withs.Table (W).Sfile;

gcc/ada/gnat1drv.adb

@@ -1043,13 +1043,24 @@ begin
       elsif Main_Kind in N_Generic_Renaming_Declaration then
          Back_End_Mode := Generate_Object;
 
-      --  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.
+      --  It is not an error to analyze in CodePeer mode a spec which requires
+      --  a body, in order to generate SCIL for this spec.
 
-      elsif CodePeer_Mode or (Alfa_Mode and not Frame_Condition_Mode) then
+      elsif CodePeer_Mode then
          Back_End_Mode := Generate_Object;
 
+      --  It is not an error to analyze in Alfa 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 Alfa_Mode then
+         if Frame_Condition_Mode then
+            Back_End_Mode := Declarations_Only;
+         else
+            Back_End_Mode := Generate_Object;
+         end if;
+
       --  In all other cases (specs which have bodies, generics, and bodies
       --  where subunits are missing), we cannot generate code and we generate
       --  a warning message. Note that generic instantiations are gone at this

gcc/ada/sem_ch6.adb

@@ -449,7 +449,7 @@ package body Sem_Ch6 is
             --  prevent visibility issues later with operators in instances.
 
             Preanalyze_Spec_Expression
-              (New_Copy_Tree (Expression  (Ret)), Etype (Id));
+              (New_Copy_Tree (Expression (Ret)), Etype (Id));
             End_Scope;
          end;
       end if;

gcc/ada/types.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, 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- --
@@ -102,8 +102,8 @@ package Types is
    --  Graphic characters, as defined in ARM
 
    subtype Line_Terminator is Character range ASCII.LF .. ASCII.CR;
-   --  Line terminator characters (LF, VT, FF, CR). For further details,
-   --  see the extensive discussion of line termination in the Sinput spec.
+   --  Line terminator characters (LF, VT, FF, CR). For further details, see
+   --  the extensive discussion of line termination in the Sinput spec.
 
    subtype Upper_Half_Character is
      Character range Character'Val (16#80#) .. Character'Val (16#FF#);