]> git.ipfire.org Git - thirdparty/gcc.git/commitdiff
[Ada] Fix assertion in GNATprove_Mode
authorBob Duff <duff@adacore.com>
Mon, 21 Jun 2021 11:08:03 +0000 (07:08 -0400)
committerPierre-Marie de Rodat <derodat@adacore.com>
Mon, 20 Sep 2021 12:31:30 +0000 (12:31 +0000)
gcc/ada/

* gnat1drv.adb (Gnat1drv): Avoid calling List_Rep_Info in
Generate_SCIL and GNATprove_Mode.
* repinfo.adb (List_Common_Type_Info): Fix comment.

gcc/ada/gnat1drv.adb
gcc/ada/repinfo.adb

index 6f65d7480f2df06a098776b9d0ae059cde31e42c..95c1537c4847808e3cdbffdfd4734d5fa8b32bfe 100644 (file)
@@ -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
index 148de536f96cc0f2011dfef8c588ce5558e0372b..11e35e778388a85f39610e200b2b693ea3feca6a 100644 (file)
@@ -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