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 co
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 Y
