projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0ffbef9) | patch
[Ada] Preserve Do_Range_Check flags in SPARK mode
authorEd Schonberg <schonberg@adacore.com>
Tue, 9 Oct 2018 15:04:58 +0000 (15:04 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Tue, 9 Oct 2018 15:04:58 +0000 (15:04 +0000)
commit94a98e801a6889e791aee63fcdbb6ee173d0259e
treee8b3ed61cd25937d2f439f3e254621e48d2d3756tree
parent0ffbef9f3553b6f9841f01ac5ff61850af63b219commit | diff
[Ada] Preserve Do_Range_Check flags in SPARK mode

2018-10-09  Ed Schonberg  <schonberg@adacore.com>

gcc/ada/

* checks.adb (Apply_Type_Conversion_Checks): Use GNATprove_Mode
rather than SPARK_mode in order to preserve the Do_Range_Check
flag for verification purposes.

From-SVN: r264961
gcc/ada/ChangeLog diff | blob | history
gcc/ada/checks.adb diff | blob | history