From: Arnaud Charlet <charlet@gcc.gnu.org>
Date: Mon, 20 Jan 2014 16:01:22 +0000 (+0100)
Subject: [multiple changes]
X-Git-Tag: releases/gcc-4.9.0~1524
X-Git-Url: http://git.ipfire.org/gitweb.cgi?a=commitdiff_plain;h=4a28b181a6164561a56bf02dfa1fd568e3d0ec5b;p=thirdparty%2Fgcc.git

[multiple changes]

2014-01-20  Robert Dewar  <dewar@adacore.com>

	* checks.adb: Make warnings on exceptions into errors in GNATprove mode.
	* errout.adb: Implement [ and ] insertion characters.
	* errout.ads: Document new [ and ] insertion characters.
	* sem_ch12.adb, restrict.adb, frontend.adb, exp_ch7.adb: Minor
	addition of ??? comment.
	* lib-xref.adb, exp_util.adb, gnat1drv.adb: Minor reformatting
	* exp_ch4.adb, sem_ch3.adb, sem_ch4.adb, sem_ch6.adb, sem_elab.adb,
	sem_eval.adb, sem_res.adb, sem_util.adb, sem_attr.adb, sem_aggr.adb:
	Make warnings on exceptions into errors in GNATprove mode.
	* sem_dim.adb: Minor reformatting throughout Quote [ and ]
	in error messages.

2014-01-20  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch13.adb: Code clean up.

From-SVN: r206841
---

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index d73b2ee40e67..fec727aab4f3 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,21 @@
+2014-01-20  Robert Dewar  <dewar@adacore.com>
+
+	* checks.adb: Make warnings on exceptions into errors in GNATprove mode.
+	* errout.adb: Implement [ and ] insertion characters.
+	* errout.ads: Document new [ and ] insertion characters.
+	* sem_ch12.adb, restrict.adb, frontend.adb, exp_ch7.adb: Minor
+	addition of ??? comment.
+	* lib-xref.adb, exp_util.adb, gnat1drv.adb: Minor reformatting
+	* exp_ch4.adb, sem_ch3.adb, sem_ch4.adb, sem_ch6.adb, sem_elab.adb,
+	sem_eval.adb, sem_res.adb, sem_util.adb, sem_attr.adb, sem_aggr.adb:
+	Make warnings on exceptions into errors in GNATprove mode.
+	* sem_dim.adb: Minor reformatting throughout Quote [ and ]
+	in error messages.
+
+2014-01-20  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch13.adb: Code clean up.
+
 2014-01-20  Robert Dewar  <dewar@adacore.com>
 
 	* errout.ads, errout.adb: Implement >? >x? >X? sequences in error
diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index 1e4cff810c56..eb6c5b74343f 100644
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -2956,9 +2956,12 @@ package body Checks is
       Loc         : constant Source_Ptr := Sloc (Ck_Node);
       Checks_On   : constant Boolean :=
         (not Index_Checks_Suppressed (Target_Typ))
-         or else (not Length_Checks_Suppressed (Target_Typ));
+          or else (not Length_Checks_Suppressed (Target_Typ));
 
    begin
+      --  Note: this means that we lose some useful warnings if the expander
+      --  is not active, and we also lose these warnings in SPARK mode ???
+
       if not Expander_Active then
          return;
       end if;
@@ -3694,15 +3697,30 @@ package body Checks is
       --  Here we have the optimizable case, warn if not short-circuited
 
       if K = N_Op_And or else K = N_Op_Or then
+         Error_Msg_Warn := not GNATprove_Mode;
+
          case Check is
             when Access_Check =>
-               Error_Msg_N
-                 ("Constraint_Error may be raised (access check)??",
-                  Parent (Nod));
+               if GNATprove_Mode then
+                  Error_Msg_N
+                    ("Constraint_Error might have been raised (access check)",
+                     Parent (Nod));
+               else
+                  Error_Msg_N
+                    ("Constraint_Error may be raised (access check)??",
+                     Parent (Nod));
+               end if;
+
             when Division_Check =>
-               Error_Msg_N
-                 ("Constraint_Error may be raised (zero divide)??",
-                  Parent (Nod));
+               if GNATprove_Mode then
+                  Error_Msg_N
+                    ("Constraint_Error might have been raised (zero divide)",
+                     Parent (Nod));
+               else
+                  Error_Msg_N
+                    ("Constraint_Error may be raised (zero divide)??",
+                     Parent (Nod));
+               end if;
 
             when others =>
                raise Program_Error;
@@ -3870,22 +3888,22 @@ package body Checks is
                     N_Discriminant_Specification =>
                   Apply_Compile_Time_Constraint_Error
                     (N      => Expr,
-                     Msg    => "(Ada 2005) null not allowed " &
-                               "in null-excluding components??",
+                     Msg    => "(Ada 2005) null not allowed "
+                               & "in null-excluding components??",
                      Reason => CE_Null_Not_Allowed);
 
                when N_Object_Declaration =>
                   Apply_Compile_Time_Constraint_Error
                     (N      => Expr,
-                     Msg    => "(Ada 2005) null not allowed " &
-                               "in null-excluding objects?",
+                     Msg    => "(Ada 2005) null not allowed "
+                               & "in null-excluding objects?",
                      Reason => CE_Null_Not_Allowed);
 
                when N_Parameter_Specification =>
                   Apply_Compile_Time_Constraint_Error
                     (N      => Expr,
-                     Msg    => "(Ada 2005) null not allowed " &
-                               "in null-excluding formals??",
+                     Msg    => "(Ada 2005) null not allowed "
+                               & "in null-excluding formals??",
                      Reason => CE_Null_Not_Allowed);
 
                when others =>
@@ -6682,9 +6700,7 @@ package body Checks is
 
          if not Inside_Init_Proc then
             Apply_Compile_Time_Constraint_Error
-              (N,
-               "null value not allowed here??",
-               CE_Access_Check_Failed);
+              (N, "null value not allowed here??", CE_Access_Check_Failed);
          else
             Insert_Action (N,
               Make_Raise_Constraint_Error (Loc,
diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index 6679d6a1d282..6372fea3895e 100644
--- a/gcc/ada/errout.adb
+++ b/gcc/ada/errout.adb
@@ -2712,19 +2712,20 @@ package body Errout is
       C : Character;   -- Current character
       P : Natural;     -- Current index;
 
-      procedure Set_Msg_Insertion_Warning;
-      --  Deal with ? ?? ?x? ?X? insertion sequences (also < <? <x? <X?). The
-      --  caller has already bumped the pointer past the initial ? or <.
+      procedure Set_Msg_Insertion_Warning (C : Character);
+      --  Deal with ? ?? ?x? ?X? insertion sequences (also < << <x< <X<). The
+      --  caller has already bumped the pointer past the initial ? or < and C
+      --  is set to this initial character (? or <).
 
       -------------------------------
       -- Set_Msg_Insertion_Warning --
       -------------------------------
 
-      procedure Set_Msg_Insertion_Warning is
+      procedure Set_Msg_Insertion_Warning (C : Character) is
       begin
          Warning_Msg_Char := ' ';
 
-         if P <= Text'Last and then Text (P) = '?' then
+         if P <= Text'Last and then Text (P) = C then
             if Warning_Doc_Switch then
                Warning_Msg_Char := '?';
             end if;
@@ -2735,7 +2736,7 @@ package body Errout is
            and then (Text (P) in 'a' .. 'z'
                       or else
                      Text (P) in 'A' .. 'Z')
-           and then Text (P + 1) = '?'
+           and then Text (P + 1) = C
          then
             if Warning_Doc_Switch then
                Warning_Msg_Char := Text (P);
@@ -2816,7 +2817,7 @@ package body Errout is
                null; -- already dealt with
 
             when '?' =>
-               Set_Msg_Insertion_Warning;
+               Set_Msg_Insertion_Warning ('?');
 
             when '<' =>
 
@@ -2825,7 +2826,7 @@ package body Errout is
                --  is False, the call to Set_Msg_Insertion_Warning here does
                --  no harm, since Warning_Msg_Char is ignored in that case.
 
-               Set_Msg_Insertion_Warning;
+               Set_Msg_Insertion_Warning ('<');
 
             when '|' =>
                null; -- already dealt with
@@ -2853,6 +2854,24 @@ package body Errout is
                   Set_Msg_Char (C);
                end if;
 
+            --  '[' (will be/would have been raised at run time)
+
+            when '[' =>
+               if Is_Warning_Msg then
+                  Set_Msg_Str ("will be raised at run time");
+               else
+                  Set_Msg_Str ("would have been raised at run time");
+               end if;
+
+            --   ']' (may be/might have been raised at run time)
+
+            when ']' =>
+               if Is_Warning_Msg then
+                  Set_Msg_Str ("may be raised at run time");
+               else
+                  Set_Msg_Str ("might have been raised at run time");
+               end if;
+
             --  Normal character with no special treatment
 
             when others =>
@@ -2960,6 +2979,9 @@ package body Errout is
          --  Suppress "size too small" errors in CodePeer mode and SPARK mode,
          --  since pragma Pack is also ignored in these configurations.
 
+         --  At least the comment is bogus, since you can have this message
+         --  with no pragma Pack in sight! ???
+
          if CodePeer_Mode or GNATprove_Mode then
             return True;
 
diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads
index 4ae39044f1c5..8e5874b139b1 100644
--- a/gcc/ada/errout.ads
+++ b/gcc/ada/errout.ads
@@ -304,9 +304,9 @@ package Errout is
    --    Insertion character < (Less Than: conditional warning message)
    --      The character < appearing anywhere in a message is used for a
    --      conditional error message. If Error_Msg_Warn is True, then the
-   --      effect is the same as ? described above, and in particular <? and
-   --      <X? have the effect of ?? and ?X? respectively. If Error_Msg_Warn
-   --      is False, then the < <? or <X? sequence is ignored and the message
+   --      effect is the same as ? described above, and in particular << and
+   --      <X< have the effect of ?? and ?X? respectively. If Error_Msg_Warn
+   --      is False, then the < << or <X< sequence is ignored and the message
    --      is treated as a error rather than a warning.
 
    --    Insertion character A-Z (Upper case letter: Ada reserved word)
@@ -355,6 +355,31 @@ package Errout is
    --      inserted to replace the ~ character. The string is inserted in the
    --      literal form it appears, without any action on special characters.
 
+   --    Insertion character [ (Left bracket: will/would be raised at run time)
+   --      This is used in messages about exceptions being raised at run-time.
+   --      If the current message is a warning message, then if the code is
+   --      executed, the exception will be raised, and [ inserts:
+   --
+   --        will be raised at run time
+   --
+   --      If the current message is an error message, then it is an error
+   --      because the exception would have been raised and [ inserts:
+   --
+   --        would have been raised at run time
+   --
+   --      Typically the message contains a < insertion which means that the
+   --      message is a warning or error depending on Error_Msg_Warn. This is
+   --      most typically used in the context of messages which are normally
+   --      warnings, but are errors in GNATprove mode, corresponding to the
+   --      permission in the definition of SPARK that allows an implementation
+   --      to reject a program as illegal if a situation arises in which the
+   --      compiler can determine that it is certain that a run-time check
+   --      would have fail if the statement was executed.
+
+   --    Insertion character ] (Right bracket: may/might be raised at run time)
+   --      This is like [ except that the insertion messages say may/might,
+   --      instead of will/would.
+
    ----------------------------------------
    -- Specialization of Messages for VMS --
    ----------------------------------------
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index 16ff6250588b..b154a6f6e3fa 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -9654,15 +9654,14 @@ package body Exp_Ch4 is
 
       procedure Raise_Accessibility_Error is
       begin
+         Error_Msg_Warn := not GNATprove_Mode;
          Rewrite (N,
            Make_Raise_Program_Error (Sloc (N),
              Reason => PE_Accessibility_Check_Failed));
          Set_Etype (N, Target_Type);
 
-         Error_Msg_N
-           ("??accessibility check failure", N);
-         Error_Msg_NE
-           ("\??& will be raised at run time", N, Standard_Program_Error);
+         Error_Msg_N ("<<accessibility check failure", N);
+         Error_Msg_NE ("\<<& [", N, Standard_Program_Error);
       end Raise_Accessibility_Error;
 
       ----------------------
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 9739cad53132..591606e6d845 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -937,6 +937,8 @@ package body Exp_Ch7 is
       --  Do not create finalization masters in SPARK mode because they result
       --  in unwanted expansion.
 
+      --  More detail would be useful here ???
+
       elsif GNATprove_Mode then
          return;
       end if;
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 5bac112681ed..cc5d3949791a 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -2034,7 +2034,7 @@ package body Exp_Util is
       --  may be constants that depend on the bounds of a string literal, both
       --  standard string types and more generally arrays of characters.
 
-      --  In GNATprove mode, we also need the more precise subtype to be set.
+      --  In GNATprove mode, we also need the more precise subtype to be set
 
       if not (Expander_Active or GNATprove_Mode)
         and then (No (Etype (Exp)) or else not Is_String_Type (Etype (Exp)))
diff --git a/gcc/ada/frontend.adb b/gcc/ada/frontend.adb
index 2d5c36f01196..20a92f47980b 100644
--- a/gcc/ada/frontend.adb
+++ b/gcc/ada/frontend.adb
@@ -360,6 +360,8 @@ begin
 
          --  Cleanup processing after completing main analysis
 
+         --  Comment needed for ASIS mode test and GNATprove mode test???
+
          if Operating_Mode = Generate_Code
            or else (Operating_Mode = Check_Semantics
                      and then (ASIS_Mode or GNATprove_Mode))
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index fd5063268c97..0816e8962275 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -341,6 +341,8 @@ procedure Gnat1drv is
          --  trees between specs compiled as part of a main unit or as part of
          --  a with-clause.
 
+         --  Comment is incomplete, SPARK semantics rely on static mode no???
+
          Dynamic_Elaboration_Checks := False;
 
          --  Set STRICT mode for overflow checks if not set explicitly. This
@@ -373,6 +375,8 @@ procedure Gnat1drv is
 
          --  Skip call to gigi
 
+         --  This debug flag is not documented, AARGH! ???
+
          Debug_Flag_HH := True;
 
          --  Enable assertions, since they give valuable extra information for
@@ -1145,11 +1149,11 @@ begin
       --  since representations are largely symbolic there.
 
       if Back_End_Mode = Declarations_Only
-           and then
-         (not (Back_Annotate_Rep_Info or Generate_SCIL or GNATprove_Mode)
-           or else Main_Kind = N_Subunit
-           or else Targparm.Frontend_Layout_On_Target
-           or else Targparm.VM_Target /= No_VM)
+        and then
+          (not (Back_Annotate_Rep_Info or Generate_SCIL or GNATprove_Mode)
+            or else Main_Kind = N_Subunit
+            or else Targparm.Frontend_Layout_On_Target
+            or else Targparm.VM_Target /= No_VM)
       then
          Sem_Ch13.Validate_Unchecked_Conversions;
          Sem_Ch13.Validate_Address_Clauses;
diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb
index 4cf52c9bd2b7..14462ce93eba 100644
--- a/gcc/ada/lib-xref.adb
+++ b/gcc/ada/lib-xref.adb
@@ -645,8 +645,8 @@ package body Lib.Xref is
 
            or else
              (GNATprove_Mode
-                and then In_Extended_Main_Code_Unit (N)
-                and then (Typ = 'm' or else Typ = 'r' or else Typ = 's'))
+               and then In_Extended_Main_Code_Unit (N)
+               and then (Typ = 'm' or else Typ = 'r' or else Typ = 's'))
          then
             null;
          else
@@ -1015,6 +1015,8 @@ package body Lib.Xref is
             Actual_Typ := 'P';
          end if;
 
+         --  Comment needed here for special SPARK code ???
+
          if GNATprove_Mode then
             Ref := Sloc (Nod);
             Def := Sloc (Ent);
diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb
index ff2d7eb93a6d..e244526389d1 100644
--- a/gcc/ada/restrict.adb
+++ b/gcc/ada/restrict.adb
@@ -538,6 +538,8 @@ package body Restrict is
       --  set in gnat1drv.adb so that we have consistency between each
       --  compilation.
 
+      --  Just checking, SPARK does not allow restrictions to be set ???
+
       if CodePeer_Mode or GNATprove_Mode then
          return;
       end if;
diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb
index 8593d025786e..7096aae5bed6 100644
--- a/gcc/ada/sem_aggr.adb
+++ b/gcc/ada/sem_aggr.adb
@@ -597,9 +597,9 @@ package body Sem_Aggr is
 
                elsif Expr_Value (This_Low) /= Expr_Value (Aggr_Low (Dim)) then
                   Set_Raises_Constraint_Error (N);
-                  Error_Msg_N ("sub-aggregate low bound mismatch??", N);
-                  Error_Msg_N
-                     ("\Constraint_Error will be raised at run time??", N);
+                  Error_Msg_Warn := not GNATprove_Mode;
+                  Error_Msg_N ("sub-aggregate low bound mismatch<<", N);
+                  Error_Msg_N ("\Constraint_Error [<<", N);
                end if;
             end if;
 
@@ -611,9 +611,9 @@ package body Sem_Aggr is
                  Expr_Value (This_High) /= Expr_Value (Aggr_High (Dim))
                then
                   Set_Raises_Constraint_Error (N);
-                  Error_Msg_N ("sub-aggregate high bound mismatch??", N);
-                  Error_Msg_N
-                     ("\Constraint_Error will be raised at run time??", N);
+                  Error_Msg_Warn := not GNATprove_Mode;
+                  Error_Msg_N ("sub-aggregate high bound mismatch<<", N);
+                  Error_Msg_N ("\Constraint_Error [<<", N);
                end if;
             end if;
          end if;
@@ -1456,8 +1456,9 @@ package body Sem_Aggr is
 
          if OK_BH and then OK_AH and then Val_BH < Val_AH then
             Set_Raises_Constraint_Error (N);
-            Error_Msg_N ("upper bound out of range??", AH);
-            Error_Msg_N ("\Constraint_Error will be raised at run time??", AH);
+            Error_Msg_Warn := not GNATprove_Mode;
+            Error_Msg_N ("upper bound out of range<<", AH);
+            Error_Msg_N ("\Constraint_Error [<<", AH);
 
             --  You need to set AH to BH or else in the case of enumerations
             --  indexes we will not be able to resolve the aggregate bounds.
@@ -1499,14 +1500,16 @@ package body Sem_Aggr is
 
          if OK_L and then Val_L > Val_AL then
             Set_Raises_Constraint_Error (N);
-            Error_Msg_N ("lower bound of aggregate out of range??", N);
-            Error_Msg_N ("\Constraint_Error will be raised at run time??", N);
+            Error_Msg_Warn := not GNATprove_Mode;
+            Error_Msg_N ("lower bound of aggregate out of range<<", N);
+            Error_Msg_N ("\Constraint_Error [<<", N);
          end if;
 
          if OK_H and then Val_H < Val_AH then
             Set_Raises_Constraint_Error (N);
-            Error_Msg_N ("upper bound of aggregate out of range??", N);
-            Error_Msg_N ("\Constraint_Error will be raised at run time??", N);
+            Error_Msg_Warn := not GNATprove_Mode;
+            Error_Msg_N ("upper bound of aggregate out of range<<", N);
+            Error_Msg_N ("\Constraint_Error [<<", N);
          end if;
       end Check_Bounds;
 
@@ -1545,8 +1548,9 @@ package body Sem_Aggr is
 
          if Range_Len < Len then
             Set_Raises_Constraint_Error (N);
-            Error_Msg_N ("too many elements??", N);
-            Error_Msg_N ("\Constraint_Error will be raised at run time??", N);
+            Error_Msg_Warn := not GNATprove_Mode;
+            Error_Msg_N ("too many elements<<", N);
+            Error_Msg_N ("\Constraint_Error [<<", N);
          end if;
       end Check_Length;
 
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 8f1a1eef225e..5ff96d7843ed 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -5396,10 +5396,10 @@ package body Sem_Attr is
                                            Name_Simple_Storage_Pool_Type))
                then
                   Error_Msg_Name_1 := Aname;
+                     Error_Msg_Warn := not GNATprove_Mode;
                   Error_Msg_N ("cannot use % attribute for type with simple "
-                               & "storage pool??", N);
-                  Error_Msg_N
-                     ("\Program_Error will be raised at run time??", N);
+                               & "storage pool<<", N);
+                  Error_Msg_N ("\Program_Error [<<", N);
 
                   Rewrite
                     (N, Make_Raise_Program_Error
@@ -9311,10 +9311,10 @@ package body Sem_Attr is
          --  know will fail, so generate an appropriate warning.
 
          if In_Instance_Body then
+            Error_Msg_Warn := not GNATprove_Mode;
             Error_Msg_F
-              ("??non-local pointer cannot point to local object", P);
-            Error_Msg_F
-              ("\??Program_Error will be raised at run time", P);
+              ("non-local pointer cannot point to local object<<", P);
+            Error_Msg_F ("\Program_Error [<<", P);
             Rewrite (N,
               Make_Raise_Program_Error (Loc,
                 Reason => PE_Accessibility_Check_Failed));
@@ -9792,10 +9792,11 @@ package body Sem_Attr is
                   --  know will fail, so generate an appropriate warning.
 
                   if In_Instance_Body then
+                     Error_Msg_Warn := not GNATprove_Mode;
                      Error_Msg_F
-                       ("??non-local pointer cannot point to local object", P);
-                     Error_Msg_F
-                       ("\??Program_Error will be raised at run time", P);
+                       ("non-local pointer cannot point to local object<<", P);
+                     Error_Msg_F ("\Program_Error [<<", P);
+
                      Rewrite (N,
                        Make_Raise_Program_Error (Loc,
                          Reason => PE_Accessibility_Check_Failed));
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index e0276a6be593..5388f63ca970 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -3722,6 +3722,9 @@ package body Sem_Ch12 is
                 and then not Is_Actual_Pack
                 and then not Inline_Now
                 and then (Operating_Mode = Generate_Code
+
+                           --  Need comment for this check ???
+
                            or else (Operating_Mode = Check_Semantics
                                      and then (ASIS_Mode or GNATprove_Mode)));
 
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 67dfd8d924bf..9d452b13ea57 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -6047,6 +6047,20 @@ package body Sem_Ch13 is
                Set_Parent (Exp, N);
                Preanalyze_Assert_Expression (Exp, Standard_Boolean);
 
+               --  In ASIS mode, even if assertions are not enabled, we must
+               --  analyze the original expression in the aspect specification
+               --  because it is part of the original tree.
+
+               if ASIS_Mode then
+                  declare
+                     Inv : constant Node_Id :=
+                             Expression (Corresponding_Aspect (Ritem));
+                  begin
+                     Replace_Type_References (Inv, Chars (T));
+                     Preanalyze_Assert_Expression (Inv, Standard_Boolean);
+                  end;
+               end if;
+
                --  Build first two arguments for Check pragma
 
                Assoc := New_List (
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 483e2be03bce..68cffb6ba37f 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -3797,10 +3797,10 @@ package body Sem_Ch3 is
                     and then Present (Get_Attribute_Definition_Clause
                                         (E, Attribute_Address))
                   then
+                     Error_Msg_Warn := not GNATprove_Mode;
                      Error_Msg_N
-                       ("??more than one task with same entry address", N);
-                     Error_Msg_N
-                       ("\??Program_Error will be raised at run time", N);
+                       ("more than one task with same entry address<<", N);
+                     Error_Msg_N ("\Program_Error [<<", N);
                      Insert_Action (N,
                        Make_Raise_Program_Error (Loc,
                          Reason => PE_Duplicated_Entry_Address));
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 1a87557ac431..a95aea9e4707 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -4627,23 +4627,17 @@ package body Sem_Ch4 is
                      Set_Etype (Sel, Etype (Comp));
                      Set_Etype (N,   Etype (Comp));
 
-                     --  Emit appropriate message. Gigi will replace the
-                     --  node subsequently with the appropriate Raise.
+                     --  Emit appropriate message. Gigi will replace the node
+                     --  subsequently with the appropriate Raise.
 
                      --  In SPARK mode, this is made into an error to simplify
                      --  the processing of the formal verification backend.
 
-                     if GNATprove_Mode then
-                        Apply_Compile_Time_Constraint_Error
-                          (N, "component not present in }",
-                           CE_Discriminant_Check_Failed,
-                           Ent => Prefix_Type, Rep => False);
-                     else
-                        Apply_Compile_Time_Constraint_Error
-                          (N, "component not present in }??",
-                           CE_Discriminant_Check_Failed,
-                           Ent => Prefix_Type, Rep => False);
-                     end if;
+                     Error_Msg_Warn := not GNATprove_Mode;
+                     Apply_Compile_Time_Constraint_Error
+                       (N, "component not present in }<<",
+                        CE_Discriminant_Check_Failed,
+                        Ent => Prefix_Type, Rep => False);
 
                      Set_Raises_Constraint_Error (N);
                      return;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 3105ac141d34..22b661a21baf 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -983,11 +983,9 @@ package body Sem_Ch6 is
                    Reason => PE_Accessibility_Check_Failed));
                Analyze (N);
 
-               Error_Msg_N
-                 ("cannot return a local value by reference??", N);
-               Error_Msg_NE
-                 ("\& will be raised at run time??",
-                   N, Standard_Program_Error);
+               Error_Msg_Warn := not GNATprove_Mode;
+               Error_Msg_N ("cannot return a local value by reference<<", N);
+               Error_Msg_NE ("\& [<<", N, Standard_Program_Error);
             end if;
          end if;
 
@@ -7225,21 +7223,12 @@ package body Sem_Ch6 is
 
                --  In GNATprove mode, it is an error to have a missing return
 
-               if GNATprove_Mode then
-                  Error_Msg_N
-                    ("RETURN statement missing following this statement!",
-                     Last_Stm);
-
-               --  Otherwise normal case of warning (RM insists this is legal)
-
-               else
-                  Error_Msg_N
-                    ("RETURN statement missing following this statement??!",
-                     Last_Stm);
-                  Error_Msg_N
-                    ("\Program_Error may be raised at run time??!",
-                     Last_Stm);
-               end if;
+               Error_Msg_Warn := not GNATprove_Mode;
+               Error_Msg_N
+                 ("RETURN statement missing following this statement<<!",
+                  Last_Stm);
+               Error_Msg_N
+                 ("\Program_Error ]<<!", Last_Stm);
             end if;
 
             --  Note: we set Err even though we have not issued a warning
@@ -7253,13 +7242,19 @@ package body Sem_Ch6 is
 
          else
             if not Raise_Exception_Call then
-               Error_Msg_N
-                 ("implied return after this statement " &
-                  "will raise Program_Error??",
-                  Last_Stm);
+               if GNATprove_Mode then
+                  Error_Msg_N
+                    ("implied return after this statement "
+                     & "would have raised Program_Error", Last_Stm);
+               else
+                  Error_Msg_N
+                    ("implied return after this statement "
+                     & "will raise Program_Error??", Last_Stm);
+               end if;
+
+               Error_Msg_Warn := not GNATprove_Mode;
                Error_Msg_NE
-                 ("\procedure & is marked as No_Return??!",
-                  Last_Stm, Proc);
+                 ("\procedure & is marked as No_Return<<!", Last_Stm, Proc);
             end if;
 
             declare
diff --git a/gcc/ada/sem_dim.adb b/gcc/ada/sem_dim.adb
index 233e30168a23..4e4f248c9c52 100644
--- a/gcc/ada/sem_dim.adb
+++ b/gcc/ada/sem_dim.adb
@@ -107,14 +107,14 @@ package body Sem_Dim is
    type Name_Array is
      array (Dimension_Position range
               Low_Position_Bound .. High_Position_Bound) of Name_Id;
-   --  A data structure used to store the names of all units within a system
+   --  Store the names of all units within a system
 
    No_Names : constant Name_Array := (others => No_Name);
 
    type Symbol_Array is
      array (Dimension_Position range
               Low_Position_Bound ..  High_Position_Bound) of String_Id;
-   --  A data structure used to store the symbols of all units within a system
+   --  Store the symbols of all units within a system
 
    No_Symbols : constant Symbol_Array := (others => No_String);
 
@@ -291,12 +291,12 @@ package body Sem_Dim is
       (N                  : Node_Id;
        Description_Needed : Boolean := False) return String;
    --  Given a node N, return the dimension symbols of N, preceded by "has
-   --  dimension" if Description_Needed. if N is dimensionless, return "[]", or
-   --  "is dimensionless" if Description_Needed.
+   --  dimension" if Description_Needed. if N is dimensionless, return "'[']",
+   --  or "is dimensionless" if Description_Needed.
 
    procedure Dim_Warning_For_Numeric_Literal (N : Node_Id; Typ : Entity_Id);
-   --  Issue a warning on the given numeric literal N to indicate the
-   --  compilateur made the assumption that the literal is not dimensionless
+   --  Issue a warning on the given numeric literal N to indicate that the
+   --  compiler made the assumption that the literal is not dimensionless
    --  but has the dimension of Typ.
 
    procedure Eval_Op_Expon_With_Rational_Exponent
@@ -320,7 +320,7 @@ package body Sem_Dim is
    --  Given a dimension vector and a dimension system, return the proper
    --  string of dimension symbols. If In_Error_Msg is True (i.e. the String_Id
    --  will be used to issue an error message) then this routine has a special
-   --  handling for the insertion character asterisk * which must be precede by
+   --  handling for the insertion characters * or [ which must be preceded by
    --  a quote ' to to be placed literally into the message.
 
    function From_Dim_To_Str_Of_Unit_Symbols
@@ -365,15 +365,14 @@ package body Sem_Dim is
 
    function "+" (Right : Whole) return Rational is
    begin
-      return Rational'(Numerator =>   Right,
-                       Denominator => 1);
+      return Rational'(Numerator => Right, Denominator => 1);
    end "+";
 
    function "+" (Left, Right : Rational) return Rational is
       R : constant Rational :=
-            Rational'(Numerator =>   Left.Numerator * Right.Denominator +
-                                       Left.Denominator * Right.Numerator,
-                      Denominator => Left.Denominator * Right.Denominator);
+            Rational'(Numerator   =>  Left.Numerator   * Right.Denominator +
+                                      Left.Denominator * Right.Numerator,
+                      Denominator => Left.Denominator  * Right.Denominator);
    begin
       return Reduce (R);
    end "+";
@@ -384,14 +383,14 @@ package body Sem_Dim is
 
    function "-" (Right : Rational) return Rational is
    begin
-      return Rational'(Numerator =>   -Right.Numerator,
+      return Rational'(Numerator   => -Right.Numerator,
                        Denominator => Right.Denominator);
    end "-";
 
    function "-" (Left, Right : Rational) return Rational is
       R : constant Rational :=
-            Rational'(Numerator =>   Left.Numerator * Right.Denominator -
-                                       Left.Denominator * Right.Numerator,
+            Rational'(Numerator   => Left.Numerator   * Right.Denominator -
+                                     Left.Denominator * Right.Numerator,
                       Denominator => Left.Denominator * Right.Denominator);
 
    begin
@@ -404,7 +403,7 @@ package body Sem_Dim is
 
    function "*" (Left, Right : Rational) return Rational is
       R : constant Rational :=
-            Rational'(Numerator =>   Left.Numerator * Right.Numerator,
+            Rational'(Numerator   => Left.Numerator   * Right.Numerator,
                       Denominator => Left.Denominator * Right.Denominator);
    begin
       return Reduce (R);
@@ -423,7 +422,7 @@ package body Sem_Dim is
          L.Numerator := Whole (-Integer (L.Numerator));
       end if;
 
-      return Reduce (Rational'(Numerator =>   L.Numerator * R.Denominator,
+      return Reduce (Rational'(Numerator   => L.Numerator   * R.Denominator,
                                Denominator => L.Denominator * R.Numerator));
    end "/";
 
@@ -433,7 +432,7 @@ package body Sem_Dim is
 
    function "abs" (Right : Rational) return Rational is
    begin
-      return Rational'(Numerator =>   abs Right.Numerator,
+      return Rational'(Numerator   => abs Right.Numerator,
                        Denominator => Right.Denominator);
    end "abs";
 
@@ -493,6 +492,7 @@ package body Sem_Dim is
          --  Integer case
 
          if Is_Integer_Type (Def_Id) then
+
             --  Dimension value must be an integer literal
 
             if Nkind (Expr) = N_Integer_Literal then
@@ -644,8 +644,8 @@ package body Sem_Dim is
                                                    N_String_Literal)
                then
                   Num_Choices := Num_Choices + 1;
-                  Error_Msg_N ("optional component Symbol expected, found&",
-                               Choice);
+                  Error_Msg_N
+                    ("optional component Symbol expected, found&", Choice);
                end if;
             end if;
          end if;
@@ -790,7 +790,7 @@ package body Sem_Dim is
 
       if Present (First (Expressions (Aggr)))
         and then (First (Expressions (Aggr)) /= Symbol_Expr
-                    or else Present (Next (Symbol_Expr)))
+                   or else Present (Next (Symbol_Expr)))
         and then (Num_Choices > 1
                    or else (Num_Choices = 1 and then not Others_Seen))
       then
@@ -931,8 +931,7 @@ package body Sem_Dim is
          Position := Position + 1;
 
          if Position > High_Position_Bound then
-            Error_Msg_N
-              ("too many dimensions in system", Aggr);
+            Error_Msg_N ("too many dimensions in system", Aggr);
             exit;
          end if;
 
@@ -953,7 +952,7 @@ package body Sem_Dim is
               and then List_Length (Expressions (Dim_Aggr)) /= 3
             then
                Error_Msg_N
-                  ("three components expected in aggregate", Dim_Aggr);
+                 ("three components expected in aggregate", Dim_Aggr);
 
             else
                --  Named dimension aggregate
@@ -1000,7 +999,6 @@ package body Sem_Dim is
                     or else Nkind (Choice) /= N_Identifier
                   then
                      Error_Msg_NE ("wrong syntax for aspect&", Choice, Id);
-
                   elsif Chars (Choice) /= Name_Dim_Symbol then
                      Error_Msg_N ("expected Dim_Symbol, found&", Choice);
                   end if;
@@ -1083,8 +1081,7 @@ package body Sem_Dim is
                   --  Verify that the string is not empty
 
                   if String_Length (Dim_Symbols (Position)) = 0 then
-                     Error_Msg_N
-                       ("empty string not allowed here", Dim_Symbol);
+                     Error_Msg_N ("empty string not allowed here", Dim_Symbol);
                   end if;
                end if;
             end if;
@@ -1242,11 +1239,8 @@ package body Sem_Dim is
             end if;
 
             Error_Msg_N
-              ("\expected dimension "
-                & Dimensions_Msg_Of (Comp_Typ)
-                & ", found "
-                & Dimensions_Msg_Of (Expr),
-               Expr);
+              ("\expected dimension " & Dimensions_Msg_Of (Comp_Typ)
+               & ", found " & Dimensions_Msg_Of (Expr), Expr);
          end if;
 
          --  Look at the named components right after the positional components
@@ -1321,10 +1315,9 @@ package body Sem_Dim is
 
       procedure Error_Dim_Msg_For_Binary_Op (N, L, R : Node_Id) is
       begin
-         Error_Msg_NE ("both operands for operation& must have same " &
-                       "dimensions",
-                       N,
-                       Entity (N));
+         Error_Msg_NE
+           ("both operands for operation& must have same dimensions",
+            N, Entity (N));
          Error_Msg_N ("\left operand "  & Dimensions_Msg_Of (L, True), N);
          Error_Msg_N ("\right operand " & Dimensions_Msg_Of (R, True), N);
       end Error_Dim_Msg_For_Binary_Op;
@@ -1337,13 +1330,13 @@ package body Sem_Dim is
         or else N_Kind in N_Op_Compare
       then
          declare
-            L                : constant Node_Id := Left_Opnd (N);
+            L                : constant Node_Id        := Left_Opnd (N);
             Dims_Of_L        : constant Dimension_Type := Dimensions_Of (L);
-            L_Has_Dimensions : constant Boolean := Exists (Dims_Of_L);
-            R                : constant Node_Id := Right_Opnd (N);
+            L_Has_Dimensions : constant Boolean        := Exists (Dims_Of_L);
+            R                : constant Node_Id        := Right_Opnd (N);
             Dims_Of_R        : constant Dimension_Type := Dimensions_Of (R);
-            R_Has_Dimensions : constant Boolean := Exists (Dims_Of_R);
-            Dims_Of_N        : Dimension_Type := Null_Dimension;
+            R_Has_Dimensions : constant Boolean        := Exists (Dims_Of_R);
+            Dims_Of_N        : Dimension_Type          := Null_Dimension;
 
          begin
             --  N_Op_Add, N_Op_Mod, N_Op_Rem or N_Op_Subtract case
@@ -1408,8 +1401,9 @@ package body Sem_Dim is
 
                if L_Has_Dimensions then
                   if not Compile_Time_Known_Value (R) then
-                     Error_Msg_N ("exponent of dimensioned operand must be " &
-                                  "known at compile time", N);
+                     Error_Msg_N
+                       ("exponent of dimensioned operand must be "
+                        & "known at compile time", N);
                   end if;
 
                   declare
@@ -1584,14 +1578,15 @@ package body Sem_Dim is
                            --  Check if error has already been encountered
 
                            if not Error_Detected then
-                              Error_Msg_NE ("dimensions mismatch in call of&",
-                                            N, Name (N));
+                              Error_Msg_NE
+                                ("dimensions mismatch in call of&",
+                                 N, Name (N));
                               Error_Detected := True;
                            end if;
 
-                           Error_Msg_N ("\expected dimension [], found " &
-                                        Dimensions_Msg_Of (Actual),
-                                        Actual);
+                           Error_Msg_N
+                             ("\expected dimension '['], found "
+                              & Dimensions_Msg_Of (Actual), Actual);
                         end if;
 
                         Next_Actual (Actual);
@@ -1610,7 +1605,6 @@ package body Sem_Dim is
 
          Actual := First_Actual (N);
          Formal := First_Formal (Nam);
-
          while Present (Formal) loop
 
             --  A missing corresponding actual indicates that the analysis of
@@ -1682,11 +1676,9 @@ package body Sem_Dim is
          Expr : Node_Id) is
       begin
          Error_Msg_N ("dimensions mismatch in component declaration", N);
-         Error_Msg_N ("\expected dimension "
-                       & Dimensions_Msg_Of (Etyp)
-                       & ", found "
-                       & Dimensions_Msg_Of (Expr),
-                      Expr);
+         Error_Msg_N
+           ("\expected dimension " & Dimensions_Msg_Of (Etyp) & ", found "
+            & Dimensions_Msg_Of (Expr), Expr);
       end Error_Dim_Msg_For_Component_Declaration;
 
    --  Start of processing for Analyze_Dimension_Component_Declaration
@@ -1700,6 +1692,7 @@ package body Sem_Dim is
          --  Check dimensions match
 
          if Dims_Of_Etyp /= Dims_Of_Expr then
+
             --  Numeric literal case. Issue a warning if the object type is not
             --  dimensionless to indicate the literal is treated as if its
             --  dimension matches the type dimension.
@@ -1725,7 +1718,7 @@ package body Sem_Dim is
    procedure Analyze_Dimension_Extended_Return_Statement (N : Node_Id) is
       Return_Ent       : constant Entity_Id := Return_Statement_Entity (N);
       Return_Etyp      : constant Entity_Id :=
-        Etype (Return_Applies_To (Return_Ent));
+                           Etype (Return_Applies_To (Return_Ent));
       Return_Obj_Decls : constant List_Id := Return_Object_Declarations (N);
       Return_Obj_Decl  : Node_Id;
       Return_Obj_Id    : Entity_Id;
@@ -1735,9 +1728,8 @@ package body Sem_Dim is
         (N              : Node_Id;
          Return_Etyp    : Entity_Id;
          Return_Obj_Typ : Entity_Id);
-      --  Error using Error_Msg_N at node N. Output the dimensions of the
-      --  returned type Return_Etyp and the returned object type Return_Obj_Typ
-      --  of N.
+      --  Error using Error_Msg_N at node N. Output dimensions of the returned
+      --  type Return_Etyp and the returned object type Return_Obj_Typ of N.
 
       -------------------------------------------------
       -- Error_Dim_Msg_For_Extended_Return_Statement --
@@ -1750,11 +1742,9 @@ package body Sem_Dim is
       is
       begin
          Error_Msg_N ("dimensions mismatch in extended return statement", N);
-         Error_Msg_N ("\expected dimension "
-                       & Dimensions_Msg_Of (Return_Etyp)
-                       & ", found "
-                       & Dimensions_Msg_Of (Return_Obj_Typ),
-                      N);
+         Error_Msg_N
+           ("\expected dimension " & Dimensions_Msg_Of (Return_Etyp)
+            & ", found " & Dimensions_Msg_Of (Return_Obj_Typ), N);
       end Error_Dim_Msg_For_Extended_Return_Statement;
 
    --  Start of processing for Analyze_Dimension_Extended_Return_Statement
@@ -1845,11 +1835,8 @@ package body Sem_Dim is
                end if;
 
                Error_Msg_N
-                 ("\expected dimension "
-                   & Dimensions_Msg_Of (Comp_Typ)
-                   & ", found "
-                   & Dimensions_Msg_Of (Expr),
-                  Comp);
+                 ("\expected dimension " & Dimensions_Msg_Of (Comp_Typ)
+                  & ", found " & Dimensions_Msg_Of (Expr), Comp);
             end if;
          end if;
 
@@ -1951,7 +1938,6 @@ package body Sem_Dim is
             declare
                Expr  : Node_Id;
                Exprs : constant List_Id := Expressions (N);
-
             begin
                if Present (Exprs) then
                   Expr := First (Exprs);
@@ -2003,11 +1989,8 @@ package body Sem_Dim is
       begin
          Error_Msg_N ("dimensions mismatch in object declaration", N);
          Error_Msg_N
-           ("\expected dimension "
-             & Dimensions_Msg_Of (Etyp)
-             & ", found "
-             & Dimensions_Msg_Of (Expr),
-            Expr);
+           ("\expected dimension " & Dimensions_Msg_Of (Etyp) & ", found "
+            & Dimensions_Msg_Of (Expr), Expr);
       end Error_Dim_Msg_For_Object_Declaration;
 
    --  Start of processing for Analyze_Dimension_Object_Declaration
@@ -2078,11 +2061,8 @@ package body Sem_Dim is
       begin
          Error_Msg_N ("dimensions mismatch in object renaming declaration", N);
          Error_Msg_N
-           ("\expected dimension "
-             & Dimensions_Msg_Of (Sub_Mark)
-             & ", found "
-             & Dimensions_Msg_Of (Renamed_Name),
-            Renamed_Name);
+           ("\expected dimension " & Dimensions_Msg_Of (Sub_Mark) & ", found "
+            & Dimensions_Msg_Of (Renamed_Name), Renamed_Name);
       end Error_Dim_Msg_For_Object_Renaming_Declaration;
 
    --  Start of processing for Analyze_Dimension_Object_Renaming_Declaration
@@ -2126,11 +2106,8 @@ package body Sem_Dim is
       begin
          Error_Msg_N ("dimensions mismatch in return statement", N);
          Error_Msg_N
-           ("\expected dimension "
-             & Dimensions_Msg_Of (Return_Etyp)
-             & ", found "
-             & Dimensions_Msg_Of (Expr),
-            Expr);
+           ("\expected dimension " & Dimensions_Msg_Of (Return_Etyp)
+            & ", found " & Dimensions_Msg_Of (Expr), Expr);
       end Error_Dim_Msg_For_Simple_Return_Statement;
 
    --  Start of processing for Analyze_Dimension_Simple_Return_Statement
@@ -2167,7 +2144,6 @@ package body Sem_Dim is
             if Exists (Dims_Of_Id) then
                Error_Msg_N
                  ("subtype& already" & Dimensions_Msg_Of (Id, True), N);
-
             else
                Set_Dimensions (Id, Dims_Of_Etyp);
                Set_Symbol (Id, Symbol_Of (Etyp));
@@ -2195,12 +2171,12 @@ package body Sem_Dim is
    begin
       case Nkind (N) is
          when N_Op_Plus | N_Op_Minus | N_Op_Abs =>
+
+            --  Propagate the dimension if the operand is not dimensionless
+
             declare
                R : constant Node_Id := Right_Opnd (N);
-
             begin
-               --  Propagate the dimension if the operand is not dimensionless
-
                Move_Dimensions (R, N);
             end;
 
@@ -2298,10 +2274,11 @@ package body Sem_Dim is
          Right_Rat : Rational;
 
       begin
-         --  Both left and right operands are an integer literal
+         --  Both left and right operands are integer literals
 
          if Nkind (Left) = N_Integer_Literal
-           and then Nkind (Right) = N_Integer_Literal
+              and then
+            Nkind (Right) = N_Integer_Literal
          then
             Left_Rat := Process_Literal (Left);
             Right_Rat := Process_Literal (Right);
@@ -2407,10 +2384,10 @@ package body Sem_Dim is
       elsif Description_Needed then
          Add_Str_To_Name_Buffer ("is dimensionless");
 
-      --  Otherwise, return "[]"
+      --  Otherwise, return "'[']"
 
       else
-         Add_Str_To_Name_Buffer ("[]");
+         Add_Str_To_Name_Buffer ("'[']");
       end if;
 
       Dimensions_Msg := Name_Find;
@@ -2441,12 +2418,12 @@ package body Sem_Dim is
       Add_String_To_Name_Buffer (String_From_Numeric_Literal (N));
 
       --  Insert a blank between the literal and the symbol
-      Add_Str_To_Name_Buffer    (" ");
 
+      Add_Str_To_Name_Buffer (" ");
       Add_String_To_Name_Buffer (Symbol_Of (Typ));
 
       Error_Msg_Name_1 := Name_Find;
-      Error_Msg_N ("??assumed to be%%", N);
+      Error_Msg_N ("assumed to be%%??", N);
    end Dim_Warning_For_Numeric_Literal;
 
    ----------------------------------------
@@ -2492,11 +2469,11 @@ package body Sem_Dim is
      (N              : Node_Id;
       Exponent_Value : Rational)
    is
+      Loc                   : constant Source_Ptr     := Sloc (N);
       Dims_Of_N             : constant Dimension_Type := Dimensions_Of (N);
-      L                     : constant Node_Id := Left_Opnd (N);
-      Etyp_Of_L             : constant Entity_Id := Etype (L);
-      Btyp_Of_L             : constant Entity_Id := Base_Type (Etyp_Of_L);
-      Loc                   : constant Source_Ptr := Sloc (N);
+      L                     : constant Node_Id        := Left_Opnd (N);
+      Etyp_Of_L             : constant Entity_Id      := Etype (L);
+      Btyp_Of_L             : constant Entity_Id      := Base_Type (Etyp_Of_L);
       Actual_1              : Node_Id;
       Actual_2              : Node_Id;
       Dim_Power             : Rational;
@@ -2544,18 +2521,16 @@ package body Sem_Dim is
          --  Step 1: Generate the new aggregate for the aspect Dimension
 
          New_Aspects  := Empty_List;
-         List_Of_Dims := New_List;
 
+         List_Of_Dims := New_List;
          for Position in Dims_Of_N'First ..  System.Count loop
             Dim_Power := Dims_Of_N (Position);
             Append_To (List_Of_Dims,
                Make_Op_Divide (Loc,
                  Left_Opnd  =>
-                   Make_Integer_Literal (Loc,
-                     Int (Dim_Power.Numerator)),
+                   Make_Integer_Literal (Loc, Int (Dim_Power.Numerator)),
                  Right_Opnd =>
-                   Make_Integer_Literal (Loc,
-                     Int (Dim_Power.Denominator))));
+                   Make_Integer_Literal (Loc, Int (Dim_Power.Denominator))));
          end loop;
 
          --  Step 2: Create the new Aspect Specification for Aspect Dimension
@@ -2625,7 +2600,7 @@ package body Sem_Dim is
       New_N :=
          Make_Type_Conversion (Loc,
            Subtype_Mark => New_Reference_To (New_Id, Loc),
-           Expression =>
+           Expression   =>
              Make_Function_Call (Loc,
                Name => New_Reference_To (RTE (RE_Expon_LLF), Loc),
                Parameter_Associations => New_List (
@@ -2749,10 +2724,9 @@ package body Sem_Dim is
          Actual_Str : Node_Id;
 
       begin
-         Actual := First (Actuals);
-
          --  Look for a symbols parameter association in the list of actuals
 
+         Actual := First (Actuals);
          while Present (Actual) loop
 
             --  Positional parameter association case when the actual is a
@@ -3034,7 +3008,11 @@ package body Sem_Dim is
 
       --  Store the dimension symbols inside boxes
 
-      Store_String_Char ('[');
+      if In_Error_Msg then
+         Store_String_Chars ("'[");
+      else
+         Store_String_Char ('[');
+      end if;
 
       for Position in Dimension_Type'Range loop
          Dim_Power := Dims (Position);
@@ -3051,6 +3029,7 @@ package body Sem_Dim is
             --  Positive dimension case
 
             if Dim_Power.Numerator > 0 then
+
                --  Integer case
 
                if Dim_Power.Denominator = 1 then
@@ -3094,7 +3073,12 @@ package body Sem_Dim is
          end if;
       end loop;
 
-      Store_String_Char (']');
+      if In_Error_Msg then
+         Store_String_Chars ("']");
+      else
+         Store_String_Char (']');
+      end if;
+
       return End_String;
    end From_Dim_To_Str_Of_Dim_Symbols;
 
@@ -3128,7 +3112,6 @@ package body Sem_Dim is
          Dim_Power := Dims (Position);
 
          if Dim_Power /= Zero then
-
             if First_Dim then
                First_Dim := False;
             else
@@ -3289,7 +3272,7 @@ package body Sem_Dim is
       declare
          G : constant Int := GCD (X.Numerator, X.Denominator);
       begin
-         return Rational'(Numerator =>   Whole (Int (X.Numerator) / G),
+         return Rational'(Numerator =>   Whole (Int (X.Numerator)   / G),
                           Denominator => Whole (Int (X.Denominator) / G));
       end;
    end Reduce;
@@ -3369,8 +3352,9 @@ package body Sem_Dim is
       Sbuffer : constant Source_Buffer_Ptr :=
                   Source_Text (Get_Source_File_Index (Loc));
       Src_Ptr : Source_Ptr := Loc;
-      C       : Character  := Sbuffer (Src_Ptr);
-         --  Current source program character
+
+      C : Character  := Sbuffer (Src_Ptr);
+      --  Current source program character
 
       function Belong_To_Numeric_Literal (C : Character) return Boolean;
       --  Return True if C belongs to a numeric literal
diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index 6d941025c0de..0c789c202116 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -1138,13 +1138,14 @@ package body Sem_Elab is
 
       --  Here we definitely have a bad instantiation
 
-      Error_Msg_NE ("??cannot instantiate& before body seen", N, Ent);
+      Error_Msg_Warn := not GNATprove_Mode;
+      Error_Msg_NE ("cannot instantiate& before body seen<<", N, Ent);
 
       if Present (Instance_Spec (N)) then
          Supply_Bodies (Instance_Spec (N));
       end if;
 
-      Error_Msg_N ("\??Program_Error will be raised at run time", N);
+      Error_Msg_N ("\Program_Error [<<", N);
       Insert_Elab_Check (N);
       Set_ABE_Is_Certain (N);
    end Check_Bad_Instantiation;
@@ -2178,14 +2179,17 @@ package body Sem_Elab is
       --  level, and the ABE is bound to occur.
 
       if Elab_Call.Last = 0 then
+         Error_Msg_Warn := not GNATprove_Mode;
+
          if Inst_Case then
             Error_Msg_NE
-              ("??cannot instantiate& before body seen", N, Orig_Ent);
+              ("cannot instantiate& before body seen<<", N, Orig_Ent);
          else
-            Error_Msg_NE ("??cannot call& before body seen", N, Orig_Ent);
+            Error_Msg_NE
+              ("cannot call& before body seen<<", N, Orig_Ent);
          end if;
 
-         Error_Msg_N ("\??Program_Error will be raised at run time", N);
+         Error_Msg_N ("\Program_Error [<<", N);
          Insert_Elab_Check (N);
 
       --  Call is not at outer level
@@ -2259,17 +2263,19 @@ package body Sem_Elab is
            and then (Nkind (Original_Node (N)) /= N_Function_Call
                       or else not In_Assertion_Expression (Original_Node (N)))
          then
+            Error_Msg_Warn := not GNATprove_Mode;
+
             if Inst_Case then
                Error_Msg_NE
-                 ("instantiation of& may occur before body is seen??",
+                 ("instantiation of& may occur before body is seen<<",
                   N, Orig_Ent);
             else
                Error_Msg_NE
-                 ("call to& may occur before body is seen??", N, Orig_Ent);
+                 ("call to& may occur before body is seen<<", N, Orig_Ent);
             end if;
 
             Error_Msg_N
-              ("\Program_Error may be raised at run time??", N);
+              ("\Program_Error ]<<", N);
 
             Output_Calls (N);
          end if;
@@ -2364,11 +2370,11 @@ package body Sem_Elab is
                       or else
                     Scope (Proc) = Scope (Defining_Identifier (Decl)))
                then
+                  Error_Msg_Warn := not GNATprove_Mode;
                   Error_Msg_N
-                    ("task will be activated before elaboration of its body??",
+                    ("task will be activated before elaboration of its body<<",
                       Decl);
-                  Error_Msg_N
-                    ("\Program_Error will be raised at run time??", Decl);
+                  Error_Msg_N ("\Program_Error [<<", Decl);
 
                elsif
                  Present (Corresponding_Body (Unit_Declaration_Node (Proc)))
diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb
index 99b6e775218b..5ee8ecc0cc63 100644
--- a/gcc/ada/sem_eval.adb
+++ b/gcc/ada/sem_eval.adb
@@ -369,7 +369,7 @@ package body Sem_Eval is
            Intval (N) > Expr_Value (Type_High_Bound (Universal_Integer)))
       then
          Apply_Compile_Time_Constraint_Error
-           (N, "non-static universal integer value out of range??",
+           (N, "non-static universal integer value out of range<<",
             CE_Range_Check_Failed);
 
       --  Check out of range of base type
@@ -390,7 +390,7 @@ package body Sem_Eval is
 
          elsif Is_Out_Of_Range (N, T, Assume_Valid => True) then
             Apply_Compile_Time_Constraint_Error
-              (N, "value not in range of}??", CE_Range_Check_Failed);
+              (N, "value not in range of}<<", CE_Range_Check_Failed);
 
          elsif Checks_On then
             Enable_Range_Check (N);
@@ -5225,6 +5225,8 @@ package body Sem_Eval is
       Stat := False;
       Fold := False;
 
+      --  Inhibit folding if -gnatd.f flag set
+
       if Debug_Flag_Dot_F and then In_Extended_Main_Source_Unit (N) then
          return;
       end if;
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index e9d62a48188b..1b0037725789 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -769,8 +769,9 @@ package body Sem_Res is
               and then Nkind (Parent (P)) = N_Subprogram_Body
               and then Is_Empty_List (Declarations (Parent (P)))
             then
-               Error_Msg_N ("!??infinite recursion", N);
-               Error_Msg_N ("\!??Storage_Error will be raised at run time", N);
+               Error_Msg_Warn := not GNATprove_Mode;
+               Error_Msg_N ("!infinite recursion<<", N);
+               Error_Msg_N ("\!Storage_Error [<<", N);
                Insert_Action (N,
                  Make_Raise_Storage_Error (Sloc (N),
                    Reason => SE_Infinite_Recursion));
@@ -867,8 +868,9 @@ package body Sem_Res is
          end if;
       end loop;
 
-      Error_Msg_N ("!??possible infinite recursion", N);
-      Error_Msg_N ("\!??Storage_Error may be raised at run time", N);
+      Error_Msg_Warn := not GNATprove_Mode;
+      Error_Msg_N ("!possible infinite recursion<<", N);
+      Error_Msg_N ("\!??Storage_Error ]<<", N);
 
       return True;
    end Check_Infinite_Recursion;
@@ -4553,11 +4555,11 @@ package body Sem_Res is
                  Deepest_Type_Access_Level (Typ)
             then
                if In_Instance_Body then
+                  Error_Msg_Warn := not GNATprove_Mode;
                   Error_Msg_N
-                    ("??type in allocator has deeper level than "
-                     & "designated class-wide type", E);
-                  Error_Msg_N
-                    ("\??Program_Error will be raised at run time", E);
+                    ("type in allocator has deeper level than "
+                     & "designated class-wide type<<", E);
+                  Error_Msg_N ("\Program_Error [<<", E);
                   Rewrite (N,
                     Make_Raise_Program_Error (Sloc (N),
                       Reason => PE_Accessibility_Check_Failed));
@@ -4664,8 +4666,9 @@ package body Sem_Res is
         and then Ekind (Current_Scope) = E_Package
         and then not In_Package_Body (Current_Scope)
       then
-         Error_Msg_N ("??cannot activate task before body seen", N);
-         Error_Msg_N ("\??Program_Error will be raised at run time", N);
+         Error_Msg_Warn := not GNATprove_Mode;
+         Error_Msg_N ("cannot activate task before body seen<<", N);
+         Error_Msg_N ("\Program_Error [<<", N);
       end if;
 
       --  Ada 2012 (AI05-0111-3): Detect an attempt to allocate a task or a
@@ -4677,8 +4680,9 @@ package body Sem_Res is
         and then Present (Subpool_Handle_Name (N))
         and then Has_Task (Desig_T)
       then
-         Error_Msg_N ("??cannot allocate task on subpool", N);
-         Error_Msg_N ("\??Program_Error will be raised at run time", N);
+         Error_Msg_Warn := not GNATprove_Mode;
+         Error_Msg_N ("cannot allocate task on subpool<<", N);
+         Error_Msg_N ("\Program_Error [<<", N);
 
          Rewrite (N,
            Make_Raise_Program_Error (Sloc (N),
@@ -5392,11 +5396,11 @@ package body Sem_Res is
                            and then Is_Entry_Barrier_Function (P))
                then
                   Rtype := Etype (N);
+                  Error_Msg_Warn := not GNATprove_Mode;
                   Error_Msg_NE
-                    ("??& should not be used in entry body (RM C.7(17))",
+                    ("& should not be used in entry body (RM C.7(17))<<",
                      N, Nam);
-                  Error_Msg_NE
-                    ("\Program_Error will be raised at run time??", N, Nam);
+                  Error_Msg_NE ("\Program_Error [<<", N, Nam);
                   Rewrite (N,
                     Make_Raise_Program_Error (Loc,
                       Reason => PE_Current_Task_In_Entry_Body));
@@ -5693,10 +5697,9 @@ package body Sem_Res is
                      --  Here warning is to be issued
 
                      Set_Has_Recursive_Call (Nam);
-                     Error_Msg_N
-                       ("??possible infinite recursion!", N);
-                     Error_Msg_N
-                       ("\??Storage_Error may be raised at run time!", N);
+                     Error_Msg_Warn := not GNATprove_Mode;
+                     Error_Msg_N ("possible infinite recursion<<!", N);
+                     Error_Msg_N ("\Storage_Error ]<<!", N);
                   end if;
 
                   exit Scope_Loop;
@@ -6008,8 +6011,9 @@ package body Sem_Res is
             end loop;
 
             if not Call_OK then
-               Error_Msg_N ("!?? cannot determine tag of result", N);
-               Error_Msg_N ("!?? Program_Error will be raised", N);
+               Error_Msg_Warn := not GNATprove_Mode;
+               Error_Msg_N ("!cannot determine tag of result<<", N);
+               Error_Msg_N ("\Program_Error [<<!", N);
                Insert_Action (N,
                  Make_Raise_Program_Error (Sloc (N),
                     Reason => PE_Explicit_Raise));
@@ -10873,12 +10877,11 @@ package body Sem_Res is
                     Deepest_Type_Access_Level (Opnd_Type)
                then
                   if In_Instance_Body then
+                     Error_Msg_Warn := not GNATprove_Mode;
                      Conversion_Error_N
-                       ("??source array type has deeper accessibility "
-                        & "level than target", Operand);
-                     Conversion_Error_N
-                       ("\??Program_Error will be raised at run time",
-                        Operand);
+                       ("source array type has deeper accessibility "
+                        & "level than target<<", Operand);
+                     Conversion_Error_N ("\Program_Error [<<", Operand);
                      Rewrite (N,
                        Make_Raise_Program_Error (Sloc (N),
                          Reason => PE_Accessibility_Check_Failed));
@@ -11183,11 +11186,11 @@ package body Sem_Res is
                --  will be generated by Expand_N_Type_Conversion.
 
                if In_Instance_Body then
+                  Error_Msg_Warn := not GNATprove_Mode;
                   Conversion_Error_N
-                    ("??cannot convert local pointer to non-local access type",
+                    ("cannot convert local pointer to non-local access type<<",
                      Operand);
-                  Conversion_Error_N
-                    ("\??Program_Error will be raised at run time", Operand);
+                  Conversion_Error_N ("\Program_Error [<<", Operand);
 
                else
                   Conversion_Error_N
@@ -11216,12 +11219,14 @@ package body Sem_Res is
                   --  will be generated by Expand_N_Type_Conversion.
 
                   if In_Instance_Body then
+                     Error_Msg_Warn := not GNATprove_Mode;
                      Conversion_Error_N
-                       ("??cannot convert access discriminant to non-local "
-                        & "access type", Operand);
-                     Conversion_Error_N
-                       ("\??Program_Error will be raised at run time",
-                        Operand);
+                       ("cannot convert access discriminant to non-local "
+                        & "access type<<", Operand);
+                     Conversion_Error_N ("\Program_Error [<<", Operand);
+
+                  --  Real error if not in instance body
+
                   else
                      Conversion_Error_N
                        ("cannot convert access discriminant to non-local "
@@ -11361,11 +11366,13 @@ package body Sem_Res is
                --  will be generated by Expand_N_Type_Conversion.
 
                if In_Instance_Body then
+                  Error_Msg_Warn := not GNATprove_Mode;
                   Conversion_Error_N
-                    ("??cannot convert local pointer to non-local access type",
+                    ("cannot convert local pointer to non-local access type<<",
                      Operand);
-                  Conversion_Error_N
-                    ("\??Program_Error will be raised at run time", Operand);
+                  Conversion_Error_N ("\Program_Error [<<", Operand);
+
+               --  If not in an instance body, this is a real error
 
                else
                   --  Avoid generation of spurious error message
@@ -11399,12 +11406,13 @@ package body Sem_Res is
                   --  will be generated by Expand_N_Type_Conversion.
 
                   if In_Instance_Body then
+                     Error_Msg_Warn := not GNATprove_Mode;
                      Conversion_Error_N
-                       ("??cannot convert access discriminant to non-local "
-                        & "access type", Operand);
-                     Conversion_Error_N
-                       ("\??Program_Error will be raised at run time",
-                        Operand);
+                       ("cannot convert access discriminant to non-local "
+                        & "access type<<", Operand);
+                     Conversion_Error_N ("\Program_Error [<<", Operand);
+
+                  --  If not in an instance body, this is a real error
 
                   else
                      Conversion_Error_N
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 7664e60659d2..cce45be570a7 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -578,8 +578,9 @@ package body Sem_Util is
    begin
       if Has_Predicates (Typ) then
          if Is_Generic_Actual_Type (Typ) then
-            Error_Msg_FE (Msg & "??", N, Typ);
-            Error_Msg_F ("\Program_Error will be raised at run time??", N);
+            Error_Msg_Warn := not GNATprove_Mode;
+            Error_Msg_FE (Msg & "<<", N, Typ);
+            Error_Msg_F ("\Program_Error [<<", N);
             Insert_Action (N,
               Make_Raise_Program_Error (Sloc (N),
                 Reason => PE_Bad_Predicated_Generic_Type));
@@ -3257,7 +3258,7 @@ package body Sem_Util is
       Warn : Boolean    := False) return Node_Id
    is
       Msgc : String (1 .. Msg'Length + 3);
-      --  Copy of message, with room for possible ?? and ! at end
+      --  Copy of message, with room for possible ?? or << and ! at end
 
       Msgl : Natural;
       Wmsg : Boolean;
@@ -3267,6 +3268,12 @@ package body Sem_Util is
       Eloc : Source_Ptr;
 
    begin
+      --  If this is a warning, convert it into an error if we are operating
+      --  in GNATprove mode, because in SPARK, we are allowed to consider
+      --  such warnings as illegalities, and we choose to do so!
+
+      Error_Msg_Warn := not GNATprove_Mode;
+
       --  A static constraint error in an instance body is not a fatal error.
       --  we choose to inhibit the message altogether, because there is no
       --  obvious node (for now) on which to post it. On the other hand the
@@ -3281,12 +3288,22 @@ package body Sem_Util is
             Eloc := Sloc (N);
          end if;
 
-         Msgc (1 .. Msg'Length) := Msg;
+         --  Copy message to Msgc, converting any ? in the message into
+         --  < instead, so that we have an error in GNATprove mode.
+
          Msgl := Msg'Length;
 
+         for J in 1 .. Msgl loop
+            if Msg (J) = '?' and then (J = 1 or else Msg (J) /= ''') then
+               Msgc (J) := '<';
+            else
+               Msgc (J) := Msg (J);
+            end if;
+         end loop;
+
          --  Message is a warning, even in Ada 95 case
 
-         if Msg (Msg'Last) = '?' then
+         if Msg (Msg'Last) = '?' or else Msg (Msg'Last) = '<' then
             Wmsg := True;
 
          --  In Ada 83, all messages are warnings. In the private part and
@@ -3297,16 +3314,16 @@ package body Sem_Util is
            or else (Ada_Version = Ada_83 and then Comes_From_Source (N))
          then
             Msgl := Msgl + 1;
-            Msgc (Msgl) := '?';
+            Msgc (Msgl) := '<';
             Msgl := Msgl + 1;
-            Msgc (Msgl) := '?';
+            Msgc (Msgl) := '<';
             Wmsg := True;
 
          elsif In_Instance_Not_Visible then
             Msgl := Msgl + 1;
-            Msgc (Msgl) := '?';
+            Msgc (Msgl) := '<';
             Msgl := Msgl + 1;
-            Msgc (Msgl) := '?';
+            Msgc (Msgl) := '<';
             Wmsg := True;
 
          --  Otherwise we have a real error message (Ada 95 static case)
@@ -3397,6 +3414,8 @@ package body Sem_Util is
          end loop;
 
          if Msgs then
+            Error_Msg_Warn := not GNATprove_Mode;
+
             if Present (Ent) then
                Error_Msg_NEL (Msgc (1 .. Msgl), N, Ent, Eloc);
             else
@@ -3424,25 +3443,27 @@ package body Sem_Util is
                        and then not Comes_From_Source (Conc_Typ)
                      then
                         Error_Msg_NEL
-                          ("\??& will be raised at run time",
-                           N, Standard_Constraint_Error, Eloc);
+                          ("\& [<<", N, Standard_Constraint_Error, Eloc);
 
                      else
-                        Error_Msg_NEL
-                          ("\??& will be raised for objects of this type",
-                           N, Standard_Constraint_Error, Eloc);
+                        if GNATprove_Mode then
+                           Error_Msg_NEL
+                             ("\& would have been raised for objects of this "
+                              & "type", N, Standard_Constraint_Error, Eloc);
+                        else
+                           Error_Msg_NEL
+                             ("\& will be raised for objects of this type??",
+                              N, Standard_Constraint_Error, Eloc);
+                        end if;
                      end if;
                   end;
 
                else
-                  Error_Msg_NEL
-                    ("\??& will be raised at run time",
-                     N, Standard_Constraint_Error, Eloc);
+                  Error_Msg_NEL ("\& [<<", N, Standard_Constraint_Error, Eloc);
                end if;
 
             else
-               Error_Msg
-                 ("\static expression fails Constraint_Check", Eloc);
+               Error_Msg ("\static expression fails Constraint_Check", Eloc);
                Set_Error_Posted (N);
             end if;
          end if;