diff mbox series

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

Message ID 20191010152946.GA87459@adacore.com
State New
Headers show
Series [Ada] Use declared type for deciding on SPARK pointer rules | expand

Commit Message

Pierre-Marie de Rodat Oct. 10, 2019, 3:29 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.

This rule has been already reflected in a recent commit for the Depends
contract; this commit is for the Global contract.

There is no impact on compilation hence no test.

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

2019-10-10  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* sem_prag.adb (Analyze_Global_In_Decl_Part): Simplify previous
	test, just like in a recent commit we simplified a similar test
	for Depends contract.
diff mbox series

Patch

--- gcc/ada/sem_prag.adb
+++ gcc/ada/sem_prag.adb
@@ -2429,8 +2429,7 @@  package body Sem_Prag is
                --  Constant related checks
 
                elsif Ekind (Item_Id) = E_Constant
-                 and then
-                   not Is_Access_Type (Underlying_Type (Etype (Item_Id)))
+                 and then not Is_Access_Type (Etype (Item_Id))
                then
 
                   --  Unless it is of an access type, a constant is a read-only