diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2020-05-09 22:30:56 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-07-07 05:26:53 -0400 |
| commit | db290a9e3745e79710d836c955588845baa2bb6b (patch) | |
| tree | 2ff0720f9776c6d0b4a5179add9b387fc9f82cc0 /gcc/ada/contracts.adb | |
| parent | c0ceffbebdd2946068c1b10c898e6da689ac6507 (diff) | |
| download | gcc-db290a9e3745e79710d836c955588845baa2bb6b.zip gcc-db290a9e3745e79710d836c955588845baa2bb6b.tar.gz gcc-db290a9e3745e79710d836c955588845baa2bb6b.tar.bz2 | |
[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.
Diffstat (limited to 'gcc/ada/contracts.adb')
0 files changed, 0 insertions, 0 deletions