From 4a28b181a6164561a56bf02dfa1fd568e3d0ec5b Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 20 Jan 2014 17:01:22 +0100 Subject: [multiple changes] 2014-01-20 Robert Dewar * checks.adb: Make warnings on exceptions into errors in GNATprove mode. * errout.adb: Implement [ and ] insertion characters. * errout.ads: Document new [ and ] insertion characters. * sem_ch12.adb, restrict.adb, frontend.adb, exp_ch7.adb: Minor addition of ??? comment. * lib-xref.adb, exp_util.adb, gnat1drv.adb: Minor reformatting * exp_ch4.adb, sem_ch3.adb, sem_ch4.adb, sem_ch6.adb, sem_elab.adb, sem_eval.adb, sem_res.adb, sem_util.adb, sem_attr.adb, sem_aggr.adb: Make warnings on exceptions into errors in GNATprove mode. * sem_dim.adb: Minor reformatting throughout Quote [ and ] in error messages. 2014-01-20 Ed Schonberg * sem_ch13.adb: Code clean up. From-SVN: r206841 --- gcc/ada/restrict.adb | 2 ++ 1 file changed, 2 insertions(+) (limited to 'gcc/ada/restrict.adb') diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb index ff2d7eb..e244526 100644 --- a/gcc/ada/restrict.adb +++ b/gcc/ada/restrict.adb @@ -538,6 +538,8 @@ package body Restrict is -- set in gnat1drv.adb so that we have consistency between each -- compilation. + -- Just checking, SPARK does not allow restrictions to be set ??? + if CodePeer_Mode or GNATprove_Mode then return; end if; -- cgit v1.1