diff options
| author | Bob Duff <duff@adacore.com> | 2021-06-21 07:08:03 -0400 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-09-20 12:31:30 +0000 |
| commit | b8d31ebcfa99599fb2c213e319aee4c6cf6e4f72 (patch) | |
| tree | 7e4f839bbd63dc411661d8e7cb39ff22a2dfde39 | |
| parent | dae0df6cd979c71c7ed1c60b9203f2a41b03e20e (diff) | |
| download | gcc-b8d31ebcfa99599fb2c213e319aee4c6cf6e4f72.zip gcc-b8d31ebcfa99599fb2c213e319aee4c6cf6e4f72.tar.gz gcc-b8d31ebcfa99599fb2c213e319aee4c6cf6e4f72.tar.bz2 | |
[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.
| -rw-r--r-- | gcc/ada/gnat1drv.adb | 9 | ||||
| -rw-r--r-- | 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 6f65d74..95c1537 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 148de53..11e35e7 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 |