[Ada] Use declared type for deciding on SPARK pointer rules
diff mbox series

Message ID 20190919132819.GA41841@adacore.com
State New
Headers show
Series
  • [Ada] Use declared type for deciding on SPARK pointer rules
Related show

Commit Message

Pierre-Marie de Rodat Sept. 19, 2019, 1:28 p.m. UTC
A constant of pointer type is considered as mutable in SPARK, according
to SPARK RM 3.10, but this should be based on the declared type of the
constant instead of its underlying type.

There is no impact on compilation hence no test.

Tested on x86_64-pc-linux-gnu, committed on trunk

2019-09-19  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_prag.adb (Analyze_Depends_In_Decl_Part): Simplify previous
	test.

Patch
diff mbox series

--- gcc/ada/sem_prag.adb
+++ gcc/ada/sem_prag.adb
@@ -1272,13 +1272,7 @@  package body Sem_Prag is
             if Ekind_In (Item_Id, E_Constant,
                                   E_Generic_In_Parameter,
                                   E_In_Parameter)
-
-              --  If Item_Id is of a private type whose completion has not been
-              --  analyzed yet, its Underlying_Type is empty and we handle it
-              --  as a constant.
-
-              and then Present (Underlying_Type (Etype (Item_Id)))
-              and then Is_Access_Type (Underlying_Type (Etype (Item_Id)))
+              and then Is_Access_Type (Etype (Item_Id))
             then
                Adjusted_Kind := E_Variable;
             end if;