2011-08-01 Yannick Moy <moy@adacore.com>

[pf3gnuchains/gcc-fork.git] / gcc / ada / sem_ch5.adb

diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index e572aa2..1673e53 100644 (file)
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -808,7 +808,9 @@ package body Sem_Ch5 is
    begin
       --  Block statement is not allowed in SPARK or ALFA
 
-      if Formal_Verification_Mode then
+      if Formal_Verification_Mode
+        and then Comes_From_Source (N)
+      then
          Error_Msg_F ("|~~block statement is not allowed", N);
       end if;