Illegal Global/Depends contracts should be flagged by frontend in code for which SPARK_Mode is not specified, as GNATprove relies on contracts being legal in those cases. The frontend should skip these errors only when SPARK_Mode is Off. Now fixed, as shown on the following example.
Command: -------- $ gcc -c notinspark.ads Output: ------- 1. package Notinspark is 2. 3. function Get return Integer; 4. 5. procedure Set with 6. Global => (In_Out => Get); | >>> global item must denote variable or state 7. 8. end Notinspark; Tested on x86_64-pc-linux-gnu, committed on trunk 2014-10-10 Yannick Moy <m...@adacore.com> * errout.adb (SPARK_Msg_N): Issue error unless SPARK_Mode is Off.
Index: errout.adb =================================================================== --- errout.adb (revision 216063) +++ errout.adb (working copy) @@ -3138,7 +3138,7 @@ procedure SPARK_Msg_N (Msg : String; N : Node_Or_Entity_Id) is begin - if SPARK_Mode = On then + if SPARK_Mode /= Off then Error_Msg_N (Msg, N); end if; end SPARK_Msg_N;