| commit | 95c1628619e7f9d80aab6b2f662ef4c603eb6d77 | |
| author | pmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4> | |
| Tue, 9 Oct 2018 15:04:58 +0000 (9 15:04 +0000) | ||
| committer | pmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4> | |
| Tue, 9 Oct 2018 15:04:58 +0000 (9 15:04 +0000) | ||
| tree | e8b3ed61cd25937d2f439f3e254621e48d2d3756 | treesnapshot (tar.gz zip) |
| parent | 2157fb63fc455d5d93231df2635e98d993412b00 | commitdiff |
[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.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@264961 138bc75d-0d04-0410-961f-82ee72b054a4
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.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@264961 138bc75d-0d04-0410-961f-82ee72b054a4
| gcc/ada/ChangeLog | diffblobblamehistory | |
| gcc/ada/checks.adb | diffblobblamehistory |