From 9534ab171e71fa56c4b384c5984d0d457f2eb55d Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 4 Aug 2011 10:18:13 +0200 Subject: [multiple changes] 2011-08-04 Yannick Moy * einfo.adb, einfo.ads (Formal_Proof_On): new flag set on subprogram entities whose body contains an Annotate pragma which forces formal proof on this body. * sem_ch11.adb, sem_ch2.adb, sem_ch3.adb, sem_ch4.adb, sem_ch5.adb, sem_ch6.adb, sem_ch9.adb, sem_res.adb: Adapt call to Mark_Non_ALFA_Subprogram to pass in a message and node. * sem_prag.adb (Analyze_Pragma): add treatment of pragma Annotate (Forma_Proof, On) which sets the flag Formal_Proof_On in the surrounding subprogram. * sem_util.adb, sem_util.ads (Mark_Non_ALFA_Subprogram, Mark_Non_ALFA_Subprogram_Unconditional): if the subprogram being marked as not in ALFA is annotated with Formal_Proof being On, then an error is issued based on the additional parameters for message and node. * snames.ads-tmpl (Name_Formal_Proof): new name for annotation. * gcc-interface/Make-lang.in: Update dependencies. 2011-08-04 Hristian Kirtchev * exp_ch3.adb (Expand_Freeze_Class_Wide_Type): Do not generate Finalize_Address when CodePeer is enabled. 2011-08-04 Pascal Obry * adaint.c (__gnat_tmp_name): Use _tempnam() instead of tempnam() as the latter returns a pointer to a static buffer which is deallocated at the end of the routine. From-SVN: r177328 --- gcc/ada/sem_ch11.adb | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'gcc/ada/sem_ch11.adb') diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb index 68f3d17..4ae09e1 100644 --- a/gcc/ada/sem_ch11.adb +++ b/gcc/ada/sem_ch11.adb @@ -434,7 +434,7 @@ package body Sem_Ch11 is P : Node_Id; begin - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("raise statement is not in 'A'L'F'A", N); Check_SPARK_Restriction ("raise statement is not allowed", N); Check_Unreachable_Code (N); -- cgit v1.1