[gcc r12-3694] [Ada] Fix assertion in GNATprove_Mode

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:b8d31ebcfa99599fb2c213e319aee4c6cf6e4f72

commit r12-3694-gb8d31ebcfa99599fb2c213e319aee4c6cf6e4f72
Author: Bob Duff <duff@adacore.com>
Date:   Mon Jun 21 07:08:03 2021 -0400

    [Ada] Fix assertion in GNATprove_Mode
    
    gcc/ada/
    
            * gnat1drv.adb (Gnat1drv): Avoid calling List_Rep_Info in
            Generate_SCIL and GNATprove_Mode.
            * repinfo.adb (List_Common_Type_Info): Fix comment.

Diff:
---
 gcc/ada/gnat1drv.adb | 9 ++++++++-
 gcc/ada/repinfo.adb  | 3 ++-
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 6f65d7480f2..95c1537c484 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -1616,7 +1616,14 @@ begin
 
       Errout.Finalize (Last_Call => True);
       Errout.Output_Messages;
-      Repinfo.List_Rep_Info (Ttypes.Bytes_Big_Endian);
+
+      --  Back annotation of representation info is not done in CodePeer and
+      --  SPARK modes.
+
+      if not (Generate_SCIL or GNATprove_Mode) then
+         Repinfo.List_Rep_Info (Ttypes.Bytes_Big_Endian);
+      end if;
+
       Inline.List_Inlining_Info;
 
       --  Only write the library if the backend did not generate any error
diff --git a/gcc/ada/repinfo.adb b/gcc/ada/repinfo.adb
index 148de536f96..11e35e77838 100644
--- a/gcc/ada/repinfo.adb
+++ b/gcc/ada/repinfo.adb
@@ -422,7 +422,8 @@ package body Repinfo is
             Write_Line (";");
          end if;
 
-      --  Alignment is not always set for task and protected types
+      --  Alignment is not always set for task, protected, and class-wide
+      --  types.
 
       else
          pragma Assert