r260583 - in /trunk/gcc/ada: ChangeLog sem_spar...

[pmderodat at gcc dot gnu dot org]

Author: pmderodat
Date: Wed May 23 10:22:41 2018
New Revision: 260583

URL: https://gcc.gnu.org/viewcvs?rev=260583&root=gcc&view=rev
Log:
[Ada] Fix of some permission rules of pointers in SPARK

This commit fixes bugs in the code that implements the rules for safe pointers
in SPARK. This only affects SPARK tools, not compilation.

  * Global variables should be handled differently compared
    to parameters. The whole tree of an in global variable has the
    permission Read-Only. In contrast, an in parameter has the
    permission Read-Only for the first level and Read-Write permission
    for suffixes.
  * The suffix X of Integer'image(X) was not analyzed correctly.
  * The instruction X'img was not dealt with.
  * Shallow aliased types which are not initialized are now allowed
    and analyzed.

Dealing with function inlining is not handled correctly yet.

2018-05-23  Maroua Maalej  <maalej@adacore.com>

gcc/ada/

	* sem_spark.adb: Fix of some permission rules of pointers in SPARK.

Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/sem_spark.adb