[multiple changes]

2010-01-25  Florian Villoing  <villoing@adacore.com>

	* gnat_ugn.texi: Fix typo.

2010-01-25  Thomas Quinot  <quinot@adacore.com>

	* scos.ads: Update specification.

2010-01-25  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Process_PPCs): If a postcondition is present and the
	enclosing subprogram has no previous spec, attach postcondition
	procedure to the defining entity for the body.

2010-01-25  Ed Schonberg  <schonberg@adacore.com>

	* exp_aggr.adb (Build_Record_Aggr_Code); Do not generate call to
	initialization procedure of the ancestor part of an extension aggregate
	if it is an interface type.

2010-01-25  Vincent Celier  <celier@adacore.com>

	* gnatlink.adb (Process_Binder_File): The directory for the shared
	version of libgcc in the run path options is found in the subdirectory
	indicated by __gnat_default_libgcc_subdir.
	* link.c: Declare new const char * __gnat_default_libgcc_subdir for
	each platform.

2010-01-25  Ed Schonberg  <schonberg@adacore.com>

	* sem_prag.adb: More flexible pragma Annotate.

From-SVN: r156209

8 files changed, 262 insertions, 144 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 073ee10..4b1df4b 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,35 @@
+2010-01-25  Florian Villoing  <villoing@adacore.com>
+
+	* gnat_ugn.texi: Fix typo.
+
+2010-01-25  Thomas Quinot  <quinot@adacore.com>
+
+	* scos.ads: Update specification.
+
+2010-01-25  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch6.adb (Process_PPCs): If a postcondition is present and the
+	enclosing subprogram has no previous spec, attach postcondition
+	procedure to the defining entity for the body.
+
+2010-01-25  Ed Schonberg  <schonberg@adacore.com>
+
+	* exp_aggr.adb (Build_Record_Aggr_Code); Do not generate call to
+	initialization procedure of the ancestor part of an extension aggregate
+	if it is an interface type.
+
+2010-01-25  Vincent Celier  <celier@adacore.com>
+
+	* gnatlink.adb (Process_Binder_File): The directory for the shared
+	version of libgcc in the run path options is found in the subdirectory
+	indicated by __gnat_default_libgcc_subdir.
+	* link.c: Declare new const char * __gnat_default_libgcc_subdir for
+	each platform.
+
+2010-01-25  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_prag.adb: More flexible pragma Annotate.
+
 2010-01-22  Eric Botcazou  <ebotcazou@adacore.com>
 
 	* system-linux-armel.ads (Stack_Check_Probes): Set to True.
diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb
index 0e29af2..49e681b 100644
--- a/gcc/ada/exp_aggr.adb
+++ b/gcc/ada/exp_aggr.adb
@@ -2578,19 +2578,21 @@ package body Exp_Aggr is
                Ref := Convert_To (Init_Typ, New_Copy_Tree (Target));
                Set_Assignment_OK (Ref);
 
-               Append_List_To (L,
-                 Build_Initialization_Call (Loc,
-                   Id_Ref            => Ref,
-                   Typ               => Init_Typ,
-                   In_Init_Proc      => Within_Init_Proc,
-                   With_Default_Init => Has_Default_Init_Comps (N)
-                                          or else
-                                        Has_Task (Base_Type (Init_Typ))));
-
-               if Is_Constrained (Entity (A))
-                 and then Has_Discriminants (Entity (A))
-               then
-                  Check_Ancestor_Discriminants (Entity (A));
+               if not Is_Abstract_Type (Init_Typ) then
+                  Append_List_To (L,
+                    Build_Initialization_Call (Loc,
+                      Id_Ref            => Ref,
+                      Typ               => Init_Typ,
+                      In_Init_Proc      => Within_Init_Proc,
+                      With_Default_Init => Has_Default_Init_Comps (N)
+                                             or else
+                                           Has_Task (Base_Type (Init_Typ))));
+
+                  if Is_Constrained (Entity (A))
+                    and then Has_Discriminants (Entity (A))
+                  then
+                     Check_Ancestor_Discriminants (Entity (A));
+                  end if;
                end if;
 
             --  Handle calls to C++ constructors
diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi
index 78bbf56..42e3b91 100644
--- a/gcc/ada/gnat_ugn.texi
+++ b/gcc/ada/gnat_ugn.texi
@@ -1,4 +1,4 @@
-f\input texinfo   @c -*-texinfo-*-
+\input texinfo   @c -*-texinfo-*-
 @c %**start of header
 
 @c oooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooo
diff --git a/gcc/ada/gnatlink.adb b/gcc/ada/gnatlink.adb
index 708e179..54dbadf 100644
--- a/gcc/ada/gnatlink.adb
+++ b/gcc/ada/gnatlink.adb
@@ -733,6 +733,11 @@ procedure Gnatlink is
       --  specifies the path where the dynamic loader should find shared
       --  libraries. Equal to null string if this system doesn't support it.
 
+      Libgcc_Subdir_Ptr : Interfaces.C.Strings.chars_ptr;
+      pragma Import (C, Libgcc_Subdir_Ptr, "__gnat_default_libgcc_subdir");
+      --  Pointer to string indicating the installation subdirectory where
+      --  a default shared libgcc might be found.
+
       Object_Library_Ext_Ptr : Interfaces.C.Strings.chars_ptr;
       pragma Import
         (C, Object_Library_Ext_Ptr, "__gnat_object_library_extension");
@@ -1210,143 +1215,168 @@ procedure Gnatlink is
                                  --  Also add path to find libgcc_s.so, if
                                  --  relevant.
 
+                                 declare
+                                    Path : String (1 .. File_Path'Length + 15);
+                                    Path_Last : constant Natural :=
+                                                  File_Path'Length;
+
+                                 begin
+                                    Path (1 .. File_Path'Length) :=
+                                      File_Path.all;
+
                                  --  To find the location of the shared version
                                  --  of libgcc, we look for "gcc-lib" in the
                                  --  path of the library. However, this
                                  --  subdirectory is no longer present in
-                                 --  in recent version of GCC. So, we look for
+                                 --  recent versions of GCC. So, we look for
                                  --  the last subdirectory "lib" in the path.
 
-                                 GCC_Index :=
-                                   Index (File_Path.all, "gcc-lib");
-
-                                 if GCC_Index /= 0 then
-                                    --  The shared version of libgcc is
-                                    --  located in the parent directory.
+                                    GCC_Index :=
+                                      Index (Path (1 .. Path_Last), "gcc-lib");
 
-                                    GCC_Index := GCC_Index - 1;
+                                    if GCC_Index /= 0 then
+                                       --  The shared version of libgcc is
+                                       --  located in the parent directory.
 
-                                 else
-                                    GCC_Index :=
-                                      Index (File_Path.all, "/lib/");
+                                       GCC_Index := GCC_Index - 1;
 
-                                    if GCC_Index = 0 then
+                                    else
                                        GCC_Index :=
-                                         Index (File_Path.all,
-                                                Directory_Separator &
-                                                "lib" &
-                                                Directory_Separator);
-                                    end if;
-
-                                    --  We have found a subdirectory "lib",
-                                    --  this is where the shared version of
-                                    --  libgcc should be located.
+                                         Index
+                                           (Path (1 .. Path_Last),
+                                            "/lib/");
+
+                                       if GCC_Index = 0 then
+                                          GCC_Index :=
+                                            Index (Path (1 .. Path_Last),
+                                                   Directory_Separator &
+                                                   "lib" &
+                                                   Directory_Separator);
+                                       end if;
 
-                                    if GCC_Index /= 0 then
-                                       GCC_Index := GCC_Index + 3;
+                                       --  If we have found a "lib" subdir in
+                                       --  the path to libgnat, the possible
+                                       --  shared libgcc of interest by default
+                                       --  is in libgcc_subdir at the same
+                                       --  level.
+
+                                       if GCC_Index /= 0 then
+                                          declare
+                                             Subdir : constant String :=
+                                               Value (Libgcc_Subdir_Ptr);
+                                          begin
+                                             Path
+                                               (GCC_Index + 1 ..
+                                                GCC_Index + Subdir'Length) :=
+                                               Subdir;
+                                             GCC_Index :=
+                                               GCC_Index + Subdir'Length;
+                                          end;
+                                       end if;
                                     end if;
-                                 end if;
 
                                  --  Look for an eventual run_path_option in
                                  --  the linker switches.
 
-                                 if Separate_Run_Path_Options then
-                                    Linker_Options.Increment_Last;
-                                    Linker_Options.Table
-                                      (Linker_Options.Last) :=
-                                      new String'
-                                        (Run_Path_Opt
-                                         & File_Path
-                                           (1 .. File_Path'Length
-                                            - File_Name'Length));
-
-                                    if GCC_Index /= 0 then
+                                    if Separate_Run_Path_Options then
                                        Linker_Options.Increment_Last;
                                        Linker_Options.Table
                                          (Linker_Options.Last) :=
                                          new String'
                                            (Run_Path_Opt
-                                            & File_Path (1 .. GCC_Index));
-                                    end if;
-                                 else
-                                    for J in reverse
-                                      1 .. Linker_Options.Last
-                                    loop
-                                       if Linker_Options.Table (J) /= null
-                                         and then
-                                           Linker_Options.Table (J)'Length
-                                           > Run_Path_Opt'Length
-                                         and then
-                                           Linker_Options.Table (J)
-                                           (1 .. Run_Path_Opt'Length) =
-                                           Run_Path_Opt
-                                       then
-                                          --  We have found a already specified
-                                          --  run_path_option: we will add to
-                                          --  this switch, because only one
-                                          --  run_path_option should be
-                                          --  specified.
-
-                                          Run_Path_Opt_Index := J;
-                                          exit;
-                                       end if;
-                                    end loop;
+                                            & File_Path
+                                              (1 .. File_Path'Length
+                                               - File_Name'Length));
 
-                                    --  If there is no run_path_option, we need
-                                    --  to add one.
-
-                                    if Run_Path_Opt_Index = 0 then
-                                       Linker_Options.Increment_Last;
-                                    end if;
-
-                                    if GCC_Index = 0 then
-                                       if Run_Path_Opt_Index = 0 then
+                                       if GCC_Index /= 0 then
+                                          Linker_Options.Increment_Last;
                                           Linker_Options.Table
                                             (Linker_Options.Last) :=
                                             new String'
                                               (Run_Path_Opt
-                                               & File_Path
-                                                 (1 .. File_Path'Length
-                                                  - File_Name'Length));
-
-                                       else
-                                          Linker_Options.Table
-                                            (Run_Path_Opt_Index) :=
-                                            new String'
-                                              (Linker_Options.Table
-                                                   (Run_Path_Opt_Index).all
-                                               & Path_Separator
-                                               & File_Path
-                                                 (1 .. File_Path'Length
-                                                  - File_Name'Length));
+                                               & Path (1 .. GCC_Index));
                                        end if;
-
                                     else
+                                       for J in reverse
+                                         1 .. Linker_Options.Last
+                                       loop
+                                          if Linker_Options.Table (J) /= null
+                                            and then
+                                              Linker_Options.Table (J)'Length
+                                              > Run_Path_Opt'Length
+                                            and then
+                                              Linker_Options.Table (J)
+                                              (1 .. Run_Path_Opt'Length) =
+                                              Run_Path_Opt
+                                          then
+                                             --  We have found a already
+                                             --  specified run_path_option: we
+                                             --  will add to this switch,
+                                             --  because only one
+                                             --  run_path_option should be
+                                             --  specified.
+
+                                             Run_Path_Opt_Index := J;
+                                             exit;
+                                          end if;
+                                       end loop;
+
+                                       --  If there is no run_path_option, we
+                                       --  need to add one.
+
                                        if Run_Path_Opt_Index = 0 then
-                                          Linker_Options.Table
-                                            (Linker_Options.Last) :=
-                                            new String'(Run_Path_Opt
-                                              & File_Path
-                                                (1 .. File_Path'Length
-                                                 - File_Name'Length)
-                                              & Path_Separator
-                                              & File_Path (1 .. GCC_Index));
+                                          Linker_Options.Increment_Last;
+                                       end if;
+
+                                       if GCC_Index = 0 then
+                                          if Run_Path_Opt_Index = 0 then
+                                             Linker_Options.Table
+                                               (Linker_Options.Last) :=
+                                               new String'
+                                                 (Run_Path_Opt
+                                                  & File_Path
+                                                    (1 .. File_Path'Length
+                                                     - File_Name'Length));
+
+                                          else
+                                             Linker_Options.Table
+                                               (Run_Path_Opt_Index) :=
+                                               new String'
+                                                 (Linker_Options.Table
+                                                      (Run_Path_Opt_Index).all
+                                                  & Path_Separator
+                                                  & File_Path
+                                                    (1 .. File_Path'Length
+                                                     - File_Name'Length));
+                                          end if;
 
                                        else
-                                          Linker_Options.Table
-                                            (Run_Path_Opt_Index) :=
-                                            new String'
-                                              (Linker_Options.Table
-                                                   (Run_Path_Opt_Index).all
-                                               & Path_Separator
-                                               & File_Path
-                                                 (1 .. File_Path'Length
-                                                  - File_Name'Length)
-                                               & Path_Separator
-                                               & File_Path (1 .. GCC_Index));
+                                          if Run_Path_Opt_Index = 0 then
+                                             Linker_Options.Table
+                                               (Linker_Options.Last) :=
+                                               new String'(Run_Path_Opt
+                                                 & File_Path
+                                                   (1 .. File_Path'Length
+                                                    - File_Name'Length)
+                                                 & Path_Separator
+                                                 & Path (1 .. GCC_Index));
+
+                                          else
+                                             Linker_Options.Table
+                                               (Run_Path_Opt_Index) :=
+                                               new String'
+                                                 (Linker_Options.Table
+                                                      (Run_Path_Opt_Index).all
+                                                  & Path_Separator
+                                                  & File_Path
+                                                    (1 .. File_Path'Length
+                                                     - File_Name'Length)
+                                                  & Path_Separator
+                                                  & Path (1 .. GCC_Index));
+                                          end if;
                                        end if;
                                     end if;
-                                 end if;
+                                 end;
                               end if;
                            end if;
 
diff --git a/gcc/ada/link.c b/gcc/ada/link.c
index 6ebd329..1cf6cfd 100644
--- a/gcc/ada/link.c
+++ b/gcc/ada/link.c
@@ -71,6 +71,9 @@
 /*  separate_run_path_options is set to 1 when separate "rpath" arguments   */
 /*  must be passed to the linker for each directory in the rpath.           */
 
+/*  default_libgcc_subdir is the subdirectory name (from the installation   */
+/*  root) where we may find a shared libgcc to use by default.              */
+
 /*  RESPONSE FILE & GNU LINKER                                              */
 /*  --------------------------                                              */
 /*  objlist_file_supported and using_gnu_link used together tell gnatlink   */
@@ -96,6 +99,7 @@ char __gnat_shared_libgcc_default = STATIC;
 unsigned char __gnat_using_gnu_linker = 0;
 const char *__gnat_object_library_extension = ".a";
 unsigned char __gnat_separate_run_path_options = 0;
+const char *__gnat_default_libgcc_subdir = "lib";
 
 #elif defined (sgi)
 const char *__gnat_object_file_option = "-Wl,-objectlist,";
@@ -108,6 +112,15 @@ unsigned char __gnat_using_gnu_linker = 0;
 const char *__gnat_object_library_extension = ".a";
 unsigned char __gnat_separate_run_path_options = 0;
 
+/* The libgcc_s locations have changed in GCC 4.  The n32 version used
+   to be in "lib", it moved to "lib32" and "lib" became the home of
+   the o32 version.  We are targetting n32 by default, so ... */
+#if __GNUC__ < 4
+const char *__gnat_default_libgcc_subdir = "lib";
+#else
+const char *__gnat_default_libgcc_subdir = "lib32";
+#endif
+
 #elif defined (__WIN32)
 const char *__gnat_object_file_option = "";
 const char *__gnat_run_path_option = "";
@@ -118,6 +131,7 @@ char __gnat_shared_libgcc_default = STATIC;
 unsigned char __gnat_using_gnu_linker = 1;
 const char *__gnat_object_library_extension = ".a";
 unsigned char __gnat_separate_run_path_options = 0;
+const char *__gnat_default_libgcc_subdir = "lib";
 
 #elif defined (__hpux__)
 const char *__gnat_object_file_option = "-Wl,-c,";
@@ -129,6 +143,7 @@ char __gnat_shared_libgcc_default = STATIC;
 unsigned char __gnat_using_gnu_linker = 0;
 const char *__gnat_object_library_extension = ".a";
 unsigned char __gnat_separate_run_path_options = 0;
+const char *__gnat_default_libgcc_subdir = "lib";
 
 #elif defined (_AIX)
 const char *__gnat_object_file_option = "-Wl,-f,";
@@ -140,6 +155,7 @@ char __gnat_shared_libgcc_default = STATIC;
 unsigned char __gnat_using_gnu_linker = 0;
 const char *__gnat_object_library_extension = ".a";
 unsigned char __gnat_separate_run_path_options = 0;
+const char *__gnat_default_libgcc_subdir = "lib";
 
 #elif defined (VMS)
 const char *__gnat_object_file_option = "";
@@ -151,6 +167,7 @@ unsigned char __gnat_objlist_file_supported = 0;
 unsigned char __gnat_using_gnu_linker = 0;
 const char *__gnat_object_library_extension = ".olb";
 unsigned char __gnat_separate_run_path_options = 0;
+const char *__gnat_default_libgcc_subdir = "lib";
 
 #elif defined (sun)
 const char *__gnat_object_file_option = "";
@@ -162,6 +179,13 @@ unsigned char __gnat_objlist_file_supported = 0;
 unsigned char __gnat_using_gnu_linker = 0;
 const char *__gnat_object_library_extension = ".a";
 unsigned char __gnat_separate_run_path_options = 0;
+#if defined (__sparc_v9__) || defined (__sparcv9)
+const char *__gnat_default_libgcc_subdir = "lib/sparcv9";
+#elif defined (__x86_64)
+const char *__gnat_default_libgcc_subdir = "lib/amd64";
+#else
+const char *__gnat_default_libgcc_subdir = "lib";
+#endif
 
 #elif defined (__FreeBSD__)
 const char *__gnat_object_file_option = "";
@@ -173,6 +197,7 @@ unsigned char __gnat_objlist_file_supported = 1;
 unsigned char __gnat_using_gnu_linker = 1;
 const char *__gnat_object_library_extension = ".a";
 unsigned char __gnat_separate_run_path_options = 0;
+const char *__gnat_default_libgcc_subdir = "lib";
 
 #elif defined (__APPLE__)
 const char *__gnat_object_file_option = "-Wl,-filelist,";
@@ -184,6 +209,7 @@ unsigned char __gnat_objlist_file_supported = 1;
 unsigned char __gnat_using_gnu_linker = 0;
 const char *__gnat_object_library_extension = ".a";
 unsigned char __gnat_separate_run_path_options = 1;
+const char *__gnat_default_libgcc_subdir = "lib";
 
 #elif defined (linux) || defined(__GLIBC__)
 const char *__gnat_object_file_option = "";
@@ -195,6 +221,11 @@ unsigned char __gnat_objlist_file_supported = 1;
 unsigned char __gnat_using_gnu_linker = 1;
 const char *__gnat_object_library_extension = ".a";
 unsigned char __gnat_separate_run_path_options = 0;
+#if defined (__x86_64)
+const char *__gnat_default_libgcc_subdir = "lib64";
+#else
+const char *__gnat_default_libgcc_subdir = "lib";
+#endif
 
 #elif defined (__svr4__) && defined (i386)
 const char *__gnat_object_file_option = "";
@@ -206,6 +237,7 @@ unsigned char __gnat_objlist_file_supported = 0;
 unsigned char __gnat_using_gnu_linker = 0;
 const char *__gnat_object_library_extension = ".a";
 unsigned char __gnat_separate_run_path_options = 0;
+const char *__gnat_default_libgcc_subdir = "lib";
 
 #else
 
@@ -220,4 +252,5 @@ unsigned char __gnat_objlist_file_supported = 0;
 unsigned char __gnat_using_gnu_linker = 0;
 const char *__gnat_object_library_extension = ".a";
 unsigned char __gnat_separate_run_path_options = 0;
+const char *__gnat_default_libgcc_subdir = "lib";
 #endif
diff --git a/gcc/ada/scos.ads b/gcc/ada/scos.ads
index cf2fb90..a726874 100644
--- a/gcc/ada/scos.ads
+++ b/gcc/ada/scos.ads
@@ -115,6 +115,9 @@ package SCOs is
    --        expression (if present) or to the return_subtype_indication (if
    --        no expression)
 
+   --    and any pragma that occurs at a place where a statement or declaration
+   --    is allowed.
+
    --  Statement lines
 
    --    These lines correspond to one or more successive statements (in the
@@ -123,7 +126,9 @@ package SCOs is
 
    --    Entry points to such sequences are:
 
-   --      the first statement of any sequence_of_statements
+   --      the first declaration of any declarative_part
+   --      the first statement of any sequence_of_statements that is not in a
+   --        body or block statement that has a non-empty declarative part
    --      the first statement after a compound statement
    --      the first statement after an EXIT, RAISE or GOTO statement
    --      any statement with a label
@@ -147,21 +152,23 @@ package SCOs is
    --      i  generic instantiation
    --      C  CASE statement
    --      F  FOR loop statement
+   --      P  PRAGMA
    --      R  extended RETURN statement
 
    --    and is omitted for all other cases.
 
    --  Decisions
 
-   --    Note: in the following description, logical operator includes the
-   --    short circuited forms (so can be any of AND, OR, XOR, NOT, AND THEN,
-   --    or OR ELSE).
+   --    Note: in the following description, logical operator includes only the
+   --    short circuited forms (so can be only of NOT, AND THEN, or OR ELSE).
 
    --    Decisions are either simple or complex. A simple decision is a boolean
    --    expresssion that occurs in the context of a control structure in the
-   --    source program, including WHILE, IF, EXIT WHEN. Note that a boolean
-   --    expression in any other context, for example, on the right side of an
-   --    assignment, is not considered to be a simple decision.
+   --    source program, including WHILE, IF, EXIT WHEN, or in an Assert,
+   --    Check, Pre_Condition or Post_Condition pragma. For pragmas, decision
+   --    SCOs are generated only if the corresponding pragma is enabled. Note
+   --    that a boolean expression in any other context, for example as right
+   --    hand side of an assignment, is not considered to be a simple decision.
 
    --    A complex decision is an occurrence of a logical operator which is not
    --    itself an operand of some other logical operator. If any operand of
@@ -191,11 +198,12 @@ package SCOs is
 
    --      I  decision in IF statement or conditional expression
    --      E  decision in EXIT WHEN statement
+   --      P  decision in pragma Assert/Check/Pre_Condition/Post_Condition
    --      W  decision in WHILE iteration scheme
    --      X  decision appearing in some other expression context
 
-   --    For I, E, W, sloc is the source location of the IF, EXIT or WHILE
-   --    token.
+   --    For I, E, P, W, sloc is the source location of the IF, EXIT, PRAGMA or
+   --    WHILE token.
 
    --    For X, sloc is omitted.
 
@@ -206,7 +214,6 @@ package SCOs is
    --      expression ::= term             (if expr is not logical operator)
    --      expression ::= &sloc term term  (if expr is AND or AND THEN)
    --      expression ::= |sloc term term  (if expr is OR or OR ELSE)
-   --      expression ::= ^sloc term term  (if expr is XOR)
    --      expression ::= !sloc term       (if expr is NOT)
 
    --      In the last four cases, sloc is the source location of the AND, OR,
@@ -226,19 +233,15 @@ package SCOs is
    --      where t/f are used to mark a condition that has been recognized by
    --      the compiler as always being true or false.
 
-   --    & indicates either AND or AND THEN connecting two conditions. In the
-   --    context of Couverture we only permit AND THEN in the source in any
-   --    case, so & can always be understood to be AND THEN.
-
-   --    | indicates either OR or OR ELSE connection two conditions. In the
-   --    context of Couverture we only permit OR ELSE in the source in any
-   --    case, so | can always be understood to be OR ELSE.
+   --    & indicates AND THEN connecting two conditions.
 
-   --    ^ indicates XOR connecting two conditions. In the context of
-   --    Couverture, we do not permit XOR, so this will never appear.
+   --    | indicates OR ELSE connecting two conditions.
 
    --    ! indicates NOT applied to the expression.
 
+   --    In the context of Couverture, the No_Direct_Boolean_Opeartors
+   --    restriction is assumed, and no other operator can appear.
+
    ---------------------------------------------------------------------
    -- Internal table used to store Source Coverage Obligations (SCOs) --
    ---------------------------------------------------------------------
@@ -269,8 +272,9 @@ package SCOs is
 
    --    Statements
    --      C1   = 'S' for entry point, 's' otherwise
-   --      C2   = 't', 's', 'o', 'r', 'i', 'C', 'F', 'R', ' '
-   --             (type/subtype/object/renaming/instantiation/CASE/FOR/RETURN)
+   --      C2   = 't', 's', 'o', 'r', 'i', 'C', 'F', 'P', 'R', ' '
+   --             (type/subtype/object/renaming/instantiation/
+   --              CASE/FOR/PRAGMA/RETURN/other)
    --      From = starting source location
    --      To   = ending source location
    --      Last = False for all but the last entry, True for last entry
@@ -282,9 +286,10 @@ package SCOs is
    --    statements on a single CS line.
 
    --    Decision
-   --      C1   = 'I', 'E', 'W', 'X' (if/exit/while/expression)
+   --      C1   = 'I', 'E', 'P', 'W', 'X' (if/exit/pragma/while/expression)
    --      C2   = ' '
-   --      From = location of IF/EXIT/WHILE token, No_Source_Location for X
+   --      From = location of IF/EXIT/PRAGMA/WHILE token,
+   --             No_Source_Location for X
    --      To   = No_Source_Location
    --      Last = unused
 
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 38b3b01..0746ea9 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -8352,10 +8352,15 @@ package body Sem_Ch6 is
                   Make_Handled_Sequence_Of_Statements (Loc,
                     Statements => Plist)));
 
-            --  If this is a procedure, set the Postcondition_Proc attribute
+            --  If this is a procedure, set the Postcondition_Proc attribute on
+            --  the proper defining entity for the subprogram.
 
             if Etype (Subp) = Standard_Void_Type then
-               Set_Postcondition_Proc (Spec_Id, Post_Proc);
+               if Present (Spec_Id) then
+                  Set_Postcondition_Proc (Spec_Id, Post_Proc);
+               else
+                  Set_Postcondition_Proc (Body_Id, Post_Proc);
+               end if;
             end if;
          end;
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index daa08b4..1e742e5 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -5265,8 +5265,19 @@ package body Sem_Prag is
                      if Is_Entity_Name (Exp) then
                         null;
 
+                     --  Determine the string type from the presence
+                     --  Wide (_Wide) characters.
+
                      elsif Nkind (Exp) = N_String_Literal then
-                        Resolve (Exp, Standard_String);
+                        if Has_Wide_Wide_Character (Exp) then
+                           Resolve (Exp, Standard_Wide_Wide_String);
+
+                        elsif Has_Wide_Character (Exp) then
+                           Resolve (Exp, Standard_Wide_String);
+
+                        else
+                           Resolve (Exp, Standard_String);
+                        end if;
 
                      elsif Is_Overloaded (Exp) then
                            Error_Pragma_Arg