When compiling or analyzing with GNATprove a piece of SPARK code with a
circular definition involving an incomplete declaration and an access to
it, the compilation/analysis may raise Program_Error in some cases. Now
fixed.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* sem_ch3.adb (Access_Type_Declaration): Set Etype before
checking for volatility compatibility.
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -1411,6 +1411,8 @@ package body Sem_Ch3 is
Set_Is_Tagged_Type (T, False);
end if;
+ Set_Etype (T, T);
+
-- For SPARK, check that the designated type is compatible with
-- respect to volatility with the access type.
@@ -1431,8 +1433,6 @@ package body Sem_Ch3 is
Srcpos_Bearer => T);
end if;
- Set_Etype (T, T);
-
-- If the type has appeared already in a with_type clause, it is frozen
-- and the pointer size is already set. Else, initialize.