This adds an additional warning message for Suppress (Elaboration_Check)
in SPARK mode:
The following is compiled with -gnatj55
1. pragma SPARK_Mode (On);
2. package SupEcheck is
3. pragma Suppress (Elaboration_Check);
|
>>> warning: Suppress of Elaboration_Check
ignored in SPARK, elaboration checking
rules are statically enforced (SPARK RM
7.7)
4. X : Integer;
5. end;
Tested on x86_64-pc-linux-gnu, committed on trunk
2015-01-06 Robert Dewar <[email protected]>
* sem_prag.adb (Process_Suppress_Unsuppress): Add extra warning
for ignoring pragma Suppress (Elaboration_Check) in SPARK mode.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 219222)
+++ sem_prag.adb (working copy)
@@ -9050,7 +9050,9 @@
if C = Elaboration_Check and then SPARK_Mode = On then
Error_Pragma_Arg
- ("Suppress of Elaboration_Check ignored in SPARK??", Arg1);
+ ("Suppress of Elaboration_Check ignored in SPARK??",
+ "\elaboration checking rules are statically enforced "
+ & "(SPARK RM 7.7)", Arg1);
end if;
-- One-argument case