[multiple changes]

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

	* 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  <kirtchev@adacore.com>

	* exp_ch3.adb (Expand_Freeze_Class_Wide_Type): Do not generate
	Finalize_Address when CodePeer is enabled.

2011-08-04  Pascal Obry  <obry@adacore.com>

	* 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

1 files changed, 15 insertions, 10 deletions

diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index d50dc5f..e8773a4 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -277,17 +277,22 @@ package Sem_Util is
    --  Current_Scope is returned. The returned value is Empty if this is called
    --  from a library package which is not within any subprogram.
 
-   procedure Mark_Non_ALFA_Subprogram;
+   procedure Mark_Non_ALFA_Subprogram (Msg : String; N : Node_Id);
    --  If Current_Subprogram is not Empty, mark either its specification or its
-   --  body as not being in ALFA. This procedure may be called during the
-   --  analysis of a precondition or postcondition, as indicated by the flag
-   --  In_Pre_Post_Expression, or during the analysis of a subprogram's body.
-   --  In the first case, the specification of Current_Subprogram must be
-   --  marked as not being in ALFA, as the contract is considered to be part of
-   --  the specification, so that calls to this subprogram are not in ALFA. In
-   --  the second case, mark the body as not being in ALFA, which does not
-   --  prevent the subprogram's specification, and calls to the subprogram,
-   --  from being in ALFA.
+   --  body as not being in ALFA.
+
+   --  This procedure may be called during the analysis of a precondition or
+   --  postcondition, as indicated by the flag In_Pre_Post_Expression, or
+   --  during the analysis of a subprogram's body. In the first case, the
+   --  specification of Current_Subprogram must be marked as not being in ALFA,
+   --  as the contract is considered to be part of the specification, so that
+   --  calls to this subprogram are not in ALFA. In the second case, mark the
+   --  body as not being in ALFA, which does not prevent the subprogram's
+   --  specification, and calls to the subprogram, from being in ALFA.
+
+   --  If the subprogram being marked as not in ALFA is annotated with
+   --  Formal_Proof being On, then an error is issued with message Msg on node
+   --  N.
 
    function Defining_Entity (N : Node_Id) return Entity_Id;
    --  Given a declaration N, returns the associated defining entity. If the