[multiple changes]

2011-08-05  Yannick Moy  <moy@adacore.com>

	* exp_ch7.adb (Establish_Transient_Scope): in formal verification mode,
	if the node to wrap is a pragma check, this node and enclosed
	expression are not expanded, so do not apply any transformations here.
	* exp_prag.adb (Expand_Pragma_Check): document the need to avoid
	introducing transient scopes.

2011-08-05  Jose Ruiz  <ruiz@adacore.com>

	* adaint.c (__gnat_set_writable, __gnat_set_readable,
	__gnat_set_executable, __gnat_set_non_writable, __gnat_set_non_readable,
	__gnat_copy_attribs): On VxWorks 6.x and later, the required chmod
	routine is available, so we use the default implementation of these
	functions.
	* s-os_lib.ads (Copy_File, Copy_Time_Stamps): Document that there is
	support for copying attributes on VxWorks 6.

2011-08-05  Yannick Moy  <moy@adacore.com>

	* debug.adb: Remove use of -gnatd.D.
	* gnat1drv.adb (Adjust_Global_Switches): adjust switches for ALFA mode
	* opt.ads: Simplify variables for ALFA mode, to keep one only
	* restrict.adb, sem_prag.adb: Adapt treatment done for CodePeer mode
	to ALFA mode.

2011-08-05  Vincent Celier  <celier@adacore.com>

	* prj-conf.adb (Do_Autoconf): Look also for --RTS in
	Builder'Default_Switches.

2011-08-05  Vincent Celier  <celier@adacore.com>

	* makeusg.adb: Add lines for --create-map-file switches.

2011-08-05  Ed Schonberg  <schonberg@adacore.com>

	* freeze.adb (Freeze_Entity): For a subprogram, if a type in the
	profile is incomplete and the full view is available, replace it with
	the full view.
	* sem_ch6.adb (Possible_Freeze): if a type in the profile is
	incomplete, freezing the subprogram is delayed until the full view is
	frozen.
	* sem_type.adb (Disambiguate): an ambiguity between a user-defined
	fixed-point multiplication operator and the predefined operator is
	resolved in favor of the user-defined one.

From-SVN: r177432

15 files changed, 295 insertions, 77 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 6a0b21d..5759eae 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,50 @@
+2011-08-05  Yannick Moy  <moy@adacore.com>
+
+	* exp_ch7.adb (Establish_Transient_Scope): in formal verification mode,
+	if the node to wrap is a pragma check, this node and enclosed
+	expression are not expanded, so do not apply any transformations here.
+	* exp_prag.adb (Expand_Pragma_Check): document the need to avoid
+	introducing transient scopes.
+
+2011-08-05  Jose Ruiz  <ruiz@adacore.com>
+
+	* adaint.c (__gnat_set_writable, __gnat_set_readable,
+	__gnat_set_executable, __gnat_set_non_writable, __gnat_set_non_readable,
+	__gnat_copy_attribs): On VxWorks 6.x and later, the required chmod
+	routine is available, so we use the default implementation of these
+	functions.
+	* s-os_lib.ads (Copy_File, Copy_Time_Stamps): Document that there is
+	support for copying attributes on VxWorks 6.
+
+2011-08-05  Yannick Moy  <moy@adacore.com>
+
+	* debug.adb: Remove use of -gnatd.D.
+	* gnat1drv.adb (Adjust_Global_Switches): adjust switches for ALFA mode
+	* opt.ads: Simplify variables for ALFA mode, to keep one only
+	* restrict.adb, sem_prag.adb: Adapt treatment done for CodePeer mode
+	to ALFA mode.
+
+2011-08-05  Vincent Celier  <celier@adacore.com>
+
+	* prj-conf.adb (Do_Autoconf): Look also for --RTS in
+	Builder'Default_Switches.
+
+2011-08-05  Vincent Celier  <celier@adacore.com>
+
+	* makeusg.adb: Add lines for --create-map-file switches.
+
+2011-08-05  Ed Schonberg  <schonberg@adacore.com>
+
+	* freeze.adb (Freeze_Entity): For a subprogram, if a type in the
+	profile is incomplete and the full view is available, replace it with
+	the full view.
+	* sem_ch6.adb (Possible_Freeze): if a type in the profile is
+	incomplete, freezing the subprogram is delayed until the full view is
+	frozen.
+	* sem_type.adb (Disambiguate): an ambiguity between a user-defined
+	fixed-point multiplication operator and the predefined operator is
+	resolved in favor of the user-defined one.
+
 2011-08-05  Rainer Orth  <ro@CeBiTec.Uni-Bielefeld.DE>
 
 	* init.c [__alpha__ && __osf__] (__gnat_error_handler): Use
diff --git a/gcc/ada/adaint.c b/gcc/ada/adaint.c
index ab8446d..556101d 100644
--- a/gcc/ada/adaint.c
+++ b/gcc/ada/adaint.c
@@ -56,6 +56,10 @@ extern "C" {
 #include <vxCpuLib.h>
 #endif /* _WRS_CONFIG_SMP */
 
+/* We need to know the VxWorks version because some file operations
+   (such as chmod) are only available on VxWorks 6.  */
+#include "version.h"
+
 #endif /* VxWorks */
 
 #if (defined (__mips) && defined (__sgi)) || defined (__APPLE__)
@@ -84,6 +88,17 @@ extern "C" {
 #include <unixio.h>
 #endif
 
+#ifdef __vxworks
+/* S_IREAD and S_IWRITE are not defined in VxWorks */
+#ifndef S_IREAD
+#define S_IREAD  (S_IRUSR | S_IRGRP | S_IROTH)
+#endif
+
+#ifndef S_IWRITE
+#define S_IWRITE (S_IWUSR)
+#endif
+#endif
+
 /* We don't have libiberty, so use malloc.  */
 #define xmalloc(S) malloc (S)
 #define xrealloc(V,S) realloc (V,S)
@@ -2191,7 +2206,8 @@ __gnat_set_writable (char *name)
 
   SetFileAttributes
     (wname, GetFileAttributes (wname) & ~FILE_ATTRIBUTE_READONLY);
-#elif ! defined (__vxworks) && ! defined(__nucleus__)
+#elif ! (defined (__vxworks) && _WRS_VXWORKS_MAJOR < 6) && \
+  ! defined(__nucleus__)
   GNAT_STRUCT_STAT statbuf;
 
   if (GNAT_STAT (name, &statbuf) == 0)
@@ -2213,7 +2229,8 @@ __gnat_set_executable (char *name)
   if (__gnat_can_use_acl (wname))
     __gnat_set_OWNER_ACL (wname, GRANT_ACCESS, FILE_GENERIC_EXECUTE);
 
-#elif ! defined (__vxworks) && ! defined(__nucleus__)
+#elif ! (defined (__vxworks) && _WRS_VXWORKS_MAJOR < 6) && \
+  ! defined(__nucleus__)
   GNAT_STRUCT_STAT statbuf;
 
   if (GNAT_STAT (name, &statbuf) == 0)
@@ -2240,7 +2257,8 @@ __gnat_set_non_writable (char *name)
 
   SetFileAttributes
     (wname, GetFileAttributes (wname) | FILE_ATTRIBUTE_READONLY);
-#elif ! defined (__vxworks) && ! defined(__nucleus__)
+#elif ! (defined (__vxworks) && _WRS_VXWORKS_MAJOR < 6) && \
+  ! defined(__nucleus__)
   GNAT_STRUCT_STAT statbuf;
 
   if (GNAT_STAT (name, &statbuf) == 0)
@@ -2262,7 +2280,8 @@ __gnat_set_readable (char *name)
   if (__gnat_can_use_acl (wname))
     __gnat_set_OWNER_ACL (wname, GRANT_ACCESS, FILE_GENERIC_READ);
 
-#elif ! defined (__vxworks) && ! defined(__nucleus__)
+#elif ! (defined (__vxworks) && _WRS_VXWORKS_MAJOR < 6) && \
+  ! defined(__nucleus__)
   GNAT_STRUCT_STAT statbuf;
 
   if (GNAT_STAT (name, &statbuf) == 0)
@@ -2283,7 +2302,8 @@ __gnat_set_non_readable (char *name)
   if (__gnat_can_use_acl (wname))
     __gnat_set_OWNER_ACL (wname, DENY_ACCESS, FILE_GENERIC_READ);
 
-#elif ! defined (__vxworks) && ! defined(__nucleus__)
+#elif ! (defined (__vxworks) && _WRS_VXWORKS_MAJOR < 6) && \
+  ! defined(__nucleus__)
   GNAT_STRUCT_STAT statbuf;
 
   if (GNAT_STAT (name, &statbuf) == 0)
@@ -3555,7 +3575,8 @@ char __gnat_environment_char = '$';
 int
 __gnat_copy_attribs (char *from, char *to, int mode)
 {
-#if defined (VMS) || defined (__vxworks) || defined (__nucleus__)
+#if defined (VMS) || (defined (__vxworks) && _WRS_VXWORKS_MAJOR < 6) || \
+  defined (__nucleus__)
   return -1;
 
 #elif defined (_WIN32) && !defined (RTX)
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index e024927..329e687 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -122,8 +122,8 @@ package body Debug is
    --  d.B
    --  d.C  Generate concatenation call, do not generate inline code
    --  d.D
-   --  d.E  SPARK generation mode
-   --  d.F  Why generation mode
+   --  d.E
+   --  d.F  ALFA mode
    --  d.G
    --  d.H
    --  d.I  SCIL generation mode
@@ -580,11 +580,9 @@ package body Debug is
    --  d.C  Generate call to System.Concat_n.Str_Concat_n routines in cases
    --       where we would normally generate inline concatenation code.
 
-   --  d.E  SPARK generation mode. Generate intermediate code for the sake of
-   --       formal verification through SPARK and the SPARK toolset.
-
-   --  d.F  Why generation mode. Generate intermediate code for the sake of
-   --       formal verification through Why and the Why VC generator.
+   --  d.F  ALFA mode. Generate AST in a form suitable for formal verification,
+   --       as well as additional cross reference information in ALI files to
+   --       compute effects of subprograms.
 
    --  d.I  Generate SCIL mode. Generate intermediate code for the sake of
    --       of static analysis tools, and ensure additional tree consistency
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 9138442..443c6ff 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -3532,6 +3532,16 @@ package body Exp_Ch7 is
       elsif Nkind (Wrap_Node) = N_Iteration_Scheme then
          null;
 
+      --  In formal verification mode, if the node to wrap is a pragma check,
+      --  this node and enclosed expression are not expanded, so do not apply
+      --  any transformations here.
+
+      elsif ALFA_Mode
+        and then Nkind (Wrap_Node) = N_Pragma
+        and then Get_Pragma_Id (Wrap_Node) = Pragma_Check
+      then
+         null;
+
       else
          Push_Scope (New_Internal_Entity (E_Block, Current_Scope, Loc, 'B'));
          Set_Scope_Is_Transient;
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index b1900a9..5c3d2ca 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -321,7 +321,10 @@ package body Exp_Prag is
       --  be an explicit conditional in the source, not an implicit if, so we
       --  do not call Make_Implicit_If_Statement.
 
-      --  In formal verification mode, we keep the pragma check in the code
+      --  In formal verification mode, we keep the pragma check in the code,
+      --  and its enclosed expression is not expanded. This requires that no
+      --  transient scope is introduced for pragma check in this mode in
+      --  Exp_Ch7.Establish_Transient_Scope.
 
       if ALFA_Mode then
          return;
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index a31e647..9bd0e9c 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -2461,6 +2461,18 @@ package body Freeze is
                   Formal := First_Formal (E);
                   while Present (Formal) loop
                      F_Type := Etype (Formal);
+
+                     --  AI05-0151 : incomplete types can appear in a profile.
+                     --  By the time the entity is frozen, the full view must
+                     --  be available, unless it is a limited view.
+
+                     if Is_Incomplete_Type (F_Type)
+                       and then Present (Full_View (F_Type))
+                     then
+                        F_Type := Full_View (F_Type);
+                        Set_Etype (Formal, F_Type);
+                     end if;
+
                      Freeze_And_Append (F_Type, N, Result);
 
                      if Is_Private_Type (F_Type)
@@ -2631,6 +2643,17 @@ package body Freeze is
                      --  Freeze return type
 
                      R_Type := Etype (E);
+
+                     --  AI05-0151: the return type may have been incomplete
+                     --  at the point of declaration.
+
+                     if Ekind (R_Type) = E_Incomplete_Type
+                       and then Present (Full_View (R_Type))
+                     then
+                        R_Type := Full_View (R_Type);
+                        Set_Etype (E, R_Type);
+                     end if;
+
                      Freeze_And_Append (R_Type, N, Result);
 
                      --  Check suspicious return type for C function
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index eabf112..be04785 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -390,17 +390,86 @@ procedure Gnat1drv is
          Back_End_Handles_Limited_Types := False;
       end if;
 
-      --  Set switches for formal verification modes
-
-      if Debug_Flag_Dot_EE then
-         ALFA_Through_SPARK_Mode := True;
-      end if;
+      --  Set switches for formal verification mode
 
       if Debug_Flag_Dot_FF then
-         ALFA_Through_Why_Mode := True;
-      end if;
 
-      ALFA_Mode := ALFA_Through_SPARK_Mode or ALFA_Through_Why_Mode;
+         ALFA_Mode := True;
+
+         --  Turn off inlining, which would confuse formal verification output
+         --  and gain nothing.
+
+         Front_End_Inlining := False;
+         Inline_Active      := False;
+
+         --  Disable front-end optimizations, to keep the tree as close to the
+         --  source code as possible, and also to avoid inconsistencies between
+         --  trees when using different optimization switches.
+
+         Optimization_Level := 0;
+
+         --  Enable some restrictions systematically to simplify the generated
+         --  code (and ease analysis). Note that restriction checks are also
+         --  disabled in ALFA mode, see Restrict.Check_Restriction, and user
+         --  specified Restrictions pragmas are ignored, see
+         --  Sem_Prag.Process_Restrictions_Or_Restriction_Warnings.
+
+         Restrict.Restrictions.Set (No_Initialize_Scalars) := True;
+
+         --  Suppress all language checks since they are handled implicitly by
+         --  the formal verification backend.
+         --  Turn off dynamic elaboration checks.
+         --  Turn off alignment checks.
+         --  Turn off validity checking.
+
+         Suppress_Options := (others => True);
+         Enable_Overflow_Checks := False;
+         Dynamic_Elaboration_Checks := False;
+         Reset_Validity_Check_Options;
+
+         --  Kill debug of generated code, since it messes up sloc values
+
+         Debug_Generated_Code := False;
+
+         --  Turn cross-referencing on in case it was disabled (e.g. by -gnatD)
+
+         Xref_Active := True;
+
+         --  Polling mode forced off, since it generates confusing junk
+
+         Polling_Required := False;
+
+         --  Set operating mode to Generate_Code to benefit from full front-end
+         --  expansion (e.g. default arguments).
+
+         Operating_Mode := Generate_Code;
+
+         --  Skip call to gigi
+
+         Debug_Flag_HH := True;
+
+         --  Enable assertions and debug pragmas, since they give valuable
+         --  extra information for formal verification.
+
+         Assertions_Enabled    := True;
+         Debug_Pragmas_Enabled := True;
+
+         --  Turn off style check options since we are not interested in any
+         --  front-end warnings when we are getting ALFA output.
+
+         Reset_Style_Check_Options;
+
+         --  Suppress compiler warnings, since what we are
+         --  interested in here is what formal verification can find out.
+
+         Warning_Mode := Suppress;
+
+         --  Always perform semantics and generate ALI files in ALFA mode,
+         --  so that a gnatmake -c -k will proceed further when possible.
+
+         Force_ALI_Tree_File := True;
+         Try_Semantics := True;
+      end if;
    end Adjust_Global_Switches;
 
    --------------------
diff --git a/gcc/ada/makeusg.adb b/gcc/ada/makeusg.adb
index bc34387..f2889a2 100644
--- a/gcc/ada/makeusg.adb
+++ b/gcc/ada/makeusg.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -249,6 +249,14 @@ begin
    Write_Eol;
    Write_Eol;
 
+   Write_Str ("  --create-map-file   Create map file mainprog.map");
+   Write_Eol;
+
+   Write_Str ("  --create-map-file=mapfile");
+   Write_Eol;
+   Write_Str ("                      Create map file mapfile");
+   Write_Eol;
+
    Write_Str ("  --GCC=command       Use this gcc command");
    Write_Eol;
 
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index d4d0373..55e57c4 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -1855,24 +1855,16 @@ package Opt is
    --  Used to store the ASIS version number read from a tree file to check if
    --  it is the same as stored in the ASIS version number in Tree_IO.
 
-   -----------------------------------
-   -- Modes for Formal Verification --
-   -----------------------------------
+   ----------------------------------
+   -- Mode for Formal Verification --
+   ----------------------------------
 
-   --  These modes are currently defined through debug flags
+   --  This mode is currently defined through a debug flag
 
    ALFA_Mode : Boolean := False;
-   --  Set True if ALFA_Through_SPARK_Mode or else ALFA_Through_Why_Mode
-
-   ALFA_Through_SPARK_Mode : Boolean := False;
-   --  Specific compiling mode targeting formal verification through
-   --  the generation of SPARK code for those parts of the input code that
-   --  belong to the ALFA subset of Ada. Set by debug flag -gnatd.E.
-
-   ALFA_Through_Why_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 debuf flag -gnatd.F.
+   --  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 debuf flag -gnatd.F.
 
 private
 
diff --git a/gcc/ada/prj-conf.adb b/gcc/ada/prj-conf.adb
index 2df6693..ab297e5 100644
--- a/gcc/ada/prj-conf.adb
+++ b/gcc/ada/prj-conf.adb
@@ -976,23 +976,24 @@ package body Prj.Conf is
                   Builder : constant Package_Id :=
                     Value_Of (Name_Builder, Project.Decl.Packages, Shared);
                   Switch_Array_Id : Array_Element_Id;
-                  Switch_Array : Array_Element;
 
-                  Switch_List   : String_List_Id := Nil_String;
-                  Switch : String_Element;
+                  procedure Check_RTS_Switches;
+                  --  Take into account eventual switches --RTS in
+                  --  Switch_Array_Id.
 
-                  Lang      : Name_Id;
-                  Lang_Last : Positive;
+                  ------------------------
+                  -- Check_RTS_SWitches --
+                  ------------------------
 
-               begin
-                  if Builder /= No_Package then
-                     Switch_Array_Id :=
-                       Value_Of
-                         (Name      => Name_Switches,
-                          In_Arrays =>
-                            Shared.Packages.Table (Builder).Decl.Arrays,
-                          Shared    => Shared);
+                  procedure Check_RTS_Switches is
+                     Switch_Array : Array_Element;
+
+                     Switch_List   : String_List_Id := Nil_String;
+                     Switch : String_Element;
 
+                     Lang      : Name_Id;
+                     Lang_Last : Positive;
+                  begin
                      while Switch_Array_Id /= No_Array_Element loop
                         Switch_Array :=
                           Shared.Array_Elements.Table (Switch_Array_Id);
@@ -1057,6 +1058,25 @@ package body Prj.Conf is
 
                         Switch_Array_Id := Switch_Array.Next;
                      end loop;
+                  end Check_RTS_Switches;
+
+               begin
+                  if Builder /= No_Package then
+                     Switch_Array_Id :=
+                       Value_Of
+                         (Name      => Name_Switches,
+                          In_Arrays =>
+                            Shared.Packages.Table (Builder).Decl.Arrays,
+                          Shared    => Shared);
+                     Check_RTS_Switches;
+
+                     Switch_Array_Id :=
+                       Value_Of
+                         (Name      => Name_Default_Switches,
+                          In_Arrays =>
+                            Shared.Packages.Table (Builder).Decl.Arrays,
+                          Shared    => Shared);
+                     Check_RTS_Switches;
                   end if;
                end;
             end if;
diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb
index 44e3b5f..a8dcff6 100644
--- a/gcc/ada/restrict.adb
+++ b/gcc/ada/restrict.adb
@@ -375,11 +375,12 @@ package body Restrict is
    begin
       Msg_Issued := False;
 
-      --  In CodePeer mode, we do not want to check for any restriction, or set
-      --  additional restrictions other than those already set in gnat1drv.adb
-      --  so that we have consistency between each compilation.
+      --  In CodePeer and ALFA mode, we do not want to check for any
+      --  restriction, or set additional restrictions other than those already
+      --  set in gnat1drv.adb so that we have consistency between each
+      --  compilation.
 
-      if CodePeer_Mode then
+      if CodePeer_Mode or else ALFA_Mode then
          return;
       end if;
 
diff --git a/gcc/ada/s-os_lib.ads b/gcc/ada/s-os_lib.ads
index a6418de..85e77eb 100755
--- a/gcc/ada/s-os_lib.ads
+++ b/gcc/ada/s-os_lib.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1995-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1995-2011, 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- --
@@ -343,7 +343,7 @@ package System.OS_Lib is
    --  effect of "cp -p" on Unix systems, and None corresponds to the typical
    --  effect of "cp" on Unix systems.
 
-   --  Note: Time_Stamps and Full are not supported on VMS and VxWorks
+   --  Note: Time_Stamps and Full are not supported on VMS and VxWorks 5
 
    procedure Copy_File
      (Name     : String;
@@ -371,7 +371,7 @@ package System.OS_Lib is
    --  furthermore Dest must be writable. Success will be set to True if the
    --  operation was successful and False otherwise.
    --
-   --  Note: this procedure is not supported on VMS and VxWorks. On these
+   --  Note: this procedure is not supported on VMS and VxWorks 5. On these
    --  platforms, Success is always set to False.
 
    function Read
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 986a1e8..537aa02 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -4527,6 +4527,14 @@ package body Sem_Ch6 is
 
          elsif Ekind (T) = E_Incomplete_Type and then From_With_Type (T) then
             Set_Has_Delayed_Freeze (Designator);
+
+         --  AI05-0151 : incomplete types can now appear in the profile of a
+         --  subprogram or entry declaration.
+
+         elsif Ekind (T) = E_Incomplete_Type
+           and then Ada_Version >= Ada_2012
+         then
+            Set_Has_Delayed_Freeze (Designator);
          end if;
 
       end Possible_Freeze;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index fe9cb2e..de3e307 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -5059,9 +5059,9 @@ package body Sem_Prag is
       --  Start of processing for Process_Restrictions_Or_Restriction_Warnings
 
       begin
-         --  Ignore all Restrictions pragma in CodePeer mode
+         --  Ignore all Restrictions pragma in CodePeer and ALFA modes
 
-         if CodePeer_Mode then
+         if CodePeer_Mode or else ALFA_Mode then
             return;
          end if;
 
@@ -5283,10 +5283,13 @@ package body Sem_Prag is
       --  Start of processing for Process_Suppress_Unsuppress
 
       begin
-         --  Ignore pragma Suppress/Unsuppress in codepeer mode on user code:
-         --  we want to generate checks for analysis purposes, as set by -gnatC
+         --  Ignore pragma Suppress/Unsuppress in CodePeer and ALFA modes on
+         --  user code: we want to generate checks for analysis purposes, as
+         --  set respectively by -gnatC and -gnatd.F
 
-         if CodePeer_Mode and then Comes_From_Source (N) then
+         if (CodePeer_Mode or else ALFA_Mode)
+           and then Comes_From_Source (N)
+         then
             return;
          end if;
 
@@ -9444,11 +9447,12 @@ package body Sem_Prag is
             Check_Valid_Configuration_Pragma;
             Check_Restriction (No_Initialize_Scalars, N);
 
-            --  Initialize_Scalars creates false positives in CodePeer,
-            --  so ignore this pragma in this mode.
+            --  Initialize_Scalars creates false positives in CodePeer, and
+            --  incorrect negative results in ALFA mode, so ignore this pragma
+            --  in these modes.
 
             if not Restriction_Active (No_Initialize_Scalars)
-              and then not CodePeer_Mode
+              and then not (CodePeer_Mode or else ALFA_Mode)
             then
                Init_Or_Norm_Scalars := True;
                Initialize_Scalars := True;
@@ -9475,10 +9479,10 @@ package body Sem_Prag is
          when Pragma_Inline_Always =>
             GNAT_Pragma;
 
-            --  Pragma always active unless in CodePeer mode, since this causes
-            --  walk order issues.
+            --  Pragma always active unless in CodePeer or ALFA mode, since
+            --  this causes walk order issues.
 
-            if not CodePeer_Mode then
+            if not (CodePeer_Mode or else ALFA_Mode) then
                Process_Inline (True);
             end if;
 
@@ -10917,10 +10921,11 @@ package body Sem_Prag is
             Check_Arg_Count (0);
             Check_Valid_Configuration_Pragma;
 
-            --  Normalize_Scalars creates false positives in CodePeer, so
-            --  ignore this pragma in this mode.
+            --  Normalize_Scalars creates false positives in CodePeer, and
+            --  incorrect negative results in ALFA mode, so ignore this pragma
+            --  in these modes.
 
-            if not CodePeer_Mode then
+            if not (CodePeer_Mode or else ALFA_Mode) then
                Normalize_Scalars := True;
                Init_Or_Norm_Scalars := True;
             end if;
@@ -11287,9 +11292,9 @@ package body Sem_Prag is
 
                   --  In the context of static code analysis, we do not need
                   --  complex front-end expansions related to pragma Pack,
-                  --  so disable handling of pragma Pack in this case.
+                  --  so disable handling of pragma Pack in these cases.
 
-                  if CodePeer_Mode then
+                  if CodePeer_Mode or else ALFA_Mode then
                      null;
 
                   --  Don't attempt any packing for VM targets. We possibly
diff --git a/gcc/ada/sem_type.adb b/gcc/ada/sem_type.adb
index 12f3913..1474677 100644
--- a/gcc/ada/sem_type.adb
+++ b/gcc/ada/sem_type.adb
@@ -1932,11 +1932,18 @@ package body Sem_Type is
          end if;
 
       --  Otherwise, the predefined operator has precedence, or if the user-
-      --  defined operation is directly visible we have a true ambiguity. If
-      --  this is a fixed-point multiplication and division in Ada83 mode,
+      --  defined operation is directly visible we have a true ambiguity.
+
+      --  If this is a fixed-point multiplication and division in Ada83 mode,
       --  exclude the universal_fixed operator, which often causes ambiguities
       --  in legacy code.
 
+      --  Ditto in Ada2012, where an ambiguity may arise for an operation on
+      --  a partial view that is completed with a fixed point type. See
+      --  AI05-0020 and AI05-0209. The ambiguity is resolved in favor of the
+      --  user-defined subprogram so that a client of the package has the
+      --  same resulution as the body of the package.
+
       else
          if (In_Open_Scopes (Scope (User_Subp))
            or else Is_Potentially_Use_Visible (User_Subp))
@@ -1945,7 +1952,13 @@ package body Sem_Type is
             if Is_Fixed_Point_Type (Typ)
               and then (Chars (Nam1) = Name_Op_Multiply
                           or else Chars (Nam1) = Name_Op_Divide)
-              and then Ada_Version = Ada_83
+              and then
+                (Ada_Version = Ada_83
+                  or else
+                   (Ada_Version >= Ada_2012
+                      and then
+                        In_Same_Declaration_List
+                          (Typ, Unit_Declaration_Node (User_Subp))))
             then
                if It2.Nam = Predef_Subp then
                   return It1;