[Ada] Fix of some permission rules of pointers in SPARK
authorMaroua Maalej <maalej@adacore.com>
Wed, 23 May 2018 10:22:41 +0000 (10:22 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Wed, 23 May 2018 10:22:41 +0000 (10:22 +0000)
commit6734617cedcadfddfc33378ce824b4620381d91c
tree1e991009a1ab7bcdb12be98cd9d244fce47187b6
parenta0fa549732f1a6ab26c7b904472a8f7d241dae39
[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.

From-SVN: r260583
gcc/ada/ChangeLog
gcc/ada/sem_spark.adb