2012-08-06 Robert Dewar <dewar@adacore.com>

	* aspects.ads: Define Aspect_Id_Exclude_No_Aspect.
	* par-ch13.adb, restrict.adb: Use Aspect_Id_Exclude_No_Aspect to
	simplify code.

2012-08-06  Yannick Moy  <moy@adacore.com>

	* gnat-style.texi: Update style guide for declarations.

2012-08-06  Yannick Moy  <moy@adacore.com>

	* sem_attr.adb (Analyze_Attribute): In the case for 'Old,
	skip a special expansion which is not needed in Alfa mode.

2012-08-06  Yannick Moy  <moy@adacore.com>

	* sem_ch5.adb (Analyze_Iterator_Specification): Do not perform
	an expansion of the iterator in Alfa mode.



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

7 files changed, 65 insertions, 15 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 8f7c9ca2316..7c441939644 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,25 @@
 2012-08-06  Robert Dewar  <dewar@adacore.com>
 
+	* aspects.ads: Define Aspect_Id_Exclude_No_Aspect.
+	* par-ch13.adb, restrict.adb: Use Aspect_Id_Exclude_No_Aspect to
+	simplify code.
+
+2012-08-06  Yannick Moy  <moy@adacore.com>
+
+	* gnat-style.texi: Update style guide for declarations.
+
+2012-08-06  Yannick Moy  <moy@adacore.com>
+
+	* sem_attr.adb (Analyze_Attribute): In the case for 'Old,
+	skip a special expansion which is not needed in Alfa mode.
+
+2012-08-06  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch5.adb (Analyze_Iterator_Specification): Do not perform
+	an expansion of the iterator in Alfa mode.
+
+2012-08-06  Robert Dewar  <dewar@adacore.com>
+
 	* s-oscons-tmplt.c, sem_ch9.adb, osint.adb: Minor reformatting.
 
 2012-08-06  Hristian Kirtchev  <kirtchev@adacore.com>
diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index b21b1e23973..ebe71aec0c3 100644
--- a/gcc/ada/aspects.ads
+++ b/gcc/ada/aspects.ads
@@ -184,6 +184,10 @@ package Aspects is
 
       Aspect_Lock_Free);
 
+   subtype Aspect_Id_Exclude_No_Aspect is
+     Aspect_Id range Aspect_Id'Succ (No_Aspect) .. Aspect_Id'Last;
+   --  Aspect_Id's excluding No_Aspect
+
    --  The following array indicates aspects that accept 'Class
 
    Class_Aspect_OK : constant array (Aspect_Id) of Boolean :=
diff --git a/gcc/ada/gnat-style.texi b/gcc/ada/gnat-style.texi
index 1bba7030935..63882afceca 100644
--- a/gcc/ada/gnat-style.texi
+++ b/gcc/ada/gnat-style.texi
@@ -7,14 +7,14 @@
 @c                                                                            o
 @c                     G N A T   C O D I N G   S T Y L E                      o
 @c                                                                            o
-@c   GNAT is maintained by Ada Core Technologies Inc (http://www.gnat.com).   o
+@c                     Copyright (C) 1992-2012, AdaCore                       o
 @c                                                                            o
 @c oooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooo
 
 @setfilename gnat-style.info
 
 @copying
-Copyright @copyright{} 1992-2008, Free Software Foundation, Inc.
+Copyright @copyright{} 1992-2012, AdaCore
 
 Permission is granted to copy, distribute and/or modify this document
 under the terms of the GNU Free Documentation License, Version 1.3 or
@@ -350,6 +350,24 @@ that give useful information instead.
 Local names can be shorter, because they are used only within
 one context, where comments explain their purpose.
 
+@item
+When starting a default expression on the line that follows the declaration
+line, use 2 characters for indentation.
+
+@smallexample @c adanocomment
+        Entity1 : Integer :=
+          Function_Name (Parameters, For_Call);
+@end smallexample
+
+@item
+If a default expression needs to be continued on subsequent lines, the
+continuations should be indented from the start of the expression.
+
+@smallexample @c adanocomment
+        Entity1   : Integer := Long_Function_Name
+                                 (parameters for call);
+@end smallexample
+
 @end itemize
 
 
diff --git a/gcc/ada/par-ch13.adb b/gcc/ada/par-ch13.adb
index f6927edc68f..72ca041e3c0 100644
--- a/gcc/ada/par-ch13.adb
+++ b/gcc/ada/par-ch13.adb
@@ -187,10 +187,8 @@ package body Ch13 is
 
             --  Check bad spelling
 
-            for J in Aspect_Id loop
-               if J /= No_Aspect and then
-                  Is_Bad_Spelling_Of (Token_Name, Aspect_Names (J))
-               then
+            for J in Aspect_Id_Exclude_No_Aspect loop
+               if Is_Bad_Spelling_Of (Token_Name, Aspect_Names (J)) then
                   Error_Msg_Name_1 := Aspect_Names (J);
                   Error_Msg_SC -- CODEFIX
                     ("\possible misspelling of%");
diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb
index 6b3dc2a0c4c..14ab452b477 100644
--- a/gcc/ada/restrict.adb
+++ b/gcc/ada/restrict.adb
@@ -1259,8 +1259,7 @@ package body Restrict is
      (N       : Node_Id;
       Warning : Boolean)
    is
-      A_Id : constant Aspect_Id := Get_Aspect_Id (Chars (N));
-      pragma Assert (A_Id /= No_Aspect);
+      A_Id : constant Aspect_Id_Exclude_No_Aspect := Get_Aspect_Id (Chars (N));
 
    begin
       No_Specification_Of_Aspects (A_Id) := Sloc (N);
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 782cd984fde..35adaaf6a61 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -4034,7 +4034,13 @@ package body Sem_Attr is
          --  enclosing subprogram. This is properly an expansion activity
          --  but it has to be performed now to prevent out-of-order issues.
 
-         if not Is_Entity_Name (P) then
+         --  This expansion is both harmful and not needed in Alfa mode, since
+         --  the formal verification backend relies on the types of nodes
+         --  (hence is not robust w.r.t. a change to base type here), and does
+         --  not suffer from the out-of-order issue described above. Thus, this
+         --  expansion is skipped in Alfa mode.
+
+         if not Is_Entity_Name (P) and then not Alfa_Mode then
             P_Type := Base_Type (P_Type);
             Set_Etype (N, P_Type);
             Set_Etype (P, P_Type);
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index d2e9d9169d4..f3df8c5c6ab 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -1665,16 +1665,21 @@ package body Sem_Ch5 is
       --  If the domain of iteration is an expression, create a declaration for
       --  it, so that finalization actions are introduced outside of the loop.
       --  The declaration must be a renaming because the body of the loop may
-      --  assign to elements. When the context is a quantified expression, the
-      --  renaming declaration is delayed until the expansion phase.
+      --  assign to elements.
 
       if not Is_Entity_Name (Iter_Name)
+
+        --  When the context is a quantified expression, the renaming
+        --  declaration is delayed until the expansion phase if we are
+        --  doing expansion.
+
         and then (Nkind (Parent (N)) /= N_Quantified_Expression
+                   or else Operating_Mode = Check_Semantics)
 
-                   --  The following two tests need comments ???
+        --  Do not perform this expansion in Alfa mode, since the formal
+        --  verification directly deals with the source form of the iterator.
 
-                   or else Operating_Mode = Check_Semantics
-                   or else Alfa_Mode)
+        and then not Alfa_Mode
       then
          declare
             Id   : constant Entity_Id := Make_Temporary (Loc, 'R', Iter_Name);
@@ -1711,7 +1716,7 @@ package body Sem_Ch5 is
       --  Container is an entity or an array with uncontrolled components, or
       --  else it is a container iterator given by a function call, typically
       --  called Iterate in the case of predefined containers, even though
-      --  Iterate is not a reserved name. What matter is that the return type
+      --  Iterate is not a reserved name. What matters is that the return type
       --  of the function is an iterator type.
 
       elsif Is_Entity_Name (Iter_Name) then