projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c0ceffb) | patch
[Ada] Set range checks for for 'Update on arrays in GNATprove expansion
authorPiotr Trojanek <trojanek@adacore.com>
Sat, 9 May 2020 20:30:56 +0000 (22:30 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Tue, 7 Jul 2020 09:26:53 +0000 (05:26 -0400)
commitdb290a9e3745e79710d836c955588845baa2bb6b
tree2ff0720f9776c6d0b4a5179add9b387fc9f82cc0tree
parentc0ceffbebdd2946068c1b10c898e6da689ac6507commit | diff
[Ada] Set range checks for for 'Update on arrays in GNATprove expansion

gcc/ada/

* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Add scalar
range checks for 'Update on arrays just like for 'Update on
records.
* sem_attr.adb (Analyze_Array_Component_Update): Do not set
range checks for single-dimensional arrays.
(Resolve_Attribute): Do not set range checks for both single-
and multi- dimensional arrays.
gcc/ada/exp_spark.adb diff | blob | history
gcc/ada/sem_attr.adb diff | blob | history