[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

18 files changed, 282 insertions, 123 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index aa77d3d..09f3423 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,34 @@
 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.
+
+2011-08-04  Yannick Moy  <moy@adacore.com>
+
 	* sem_ch3.adb (Array_Type_Declaration): move test for type in ALFA
 	after index creation; mark unconstrained base array type generated as
 	being in/not in ALFA as well
diff --git a/gcc/ada/adaint.c b/gcc/ada/adaint.c
index 3d4c50a..b0fd8c5 100644
--- a/gcc/ada/adaint.c
+++ b/gcc/ada/adaint.c
@@ -1183,7 +1183,7 @@ __gnat_tmp_name (char *tmp_filename)
        directory specified by P_tmpdir in stdio.h if c:\temp does not
        exist. The filename will be created with the prefix "gnat-".  */
 
-    pname = (char *) tempnam ("c:\\temp", "gnat-");
+    pname = (char *) _tempnam ("c:\\temp", "gnat-");
 
     /* if pname is NULL, the file was not created properly, the disk is full
        or there is no more free temporary files */
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index e1b63f0..be00816 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -522,7 +522,7 @@ package body Einfo is
    --    Body_Is_In_ALFA                 Flag251
    --    Is_Processed_Transient          Flag252
    --    Is_Postcondition_Proc           Flag253
-   --    (unused)                        Flag254
+   --    Formal_Proof_On                 Flag254
 
    -----------------------
    -- Local subprograms --
@@ -1126,6 +1126,12 @@ package body Einfo is
       return Node6 (Id);
    end First_Rep_Item;
 
+   function Formal_Proof_On (Id : E) return B is
+   begin
+      pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
+      return Flag254 (Id);
+   end Formal_Proof_On;
+
    function Freeze_Node (Id : E) return N is
    begin
       return Node7 (Id);
@@ -3606,6 +3612,12 @@ package body Einfo is
       Set_Uint10 (Id, UI_From_Int (F'Pos (V)));
    end Set_Float_Rep;
 
+   procedure Set_Formal_Proof_On (Id : E; V : B := True) is
+   begin
+      pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
+      Set_Flag254 (Id, V);
+   end Set_Formal_Proof_On;
+
    procedure Set_Freeze_Node (Id : E; V : N) is
    begin
       Set_Node7 (Id, V);
@@ -7430,6 +7442,7 @@ package body Einfo is
       W ("Entry_Accepted",                  Flag152 (Id));
       W ("Can_Use_Internal_Rep",            Flag229 (Id));
       W ("Finalize_Storage_Only",           Flag158 (Id));
+      W ("Formal_Proof_On",                 Flag254 (Id));
       W ("From_With_Type",                  Flag159 (Id));
       W ("Has_Aliased_Components",          Flag135 (Id));
       W ("Has_Alignment_Clause",            Flag46  (Id));
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 9a96e8c..10f7c78 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -1272,6 +1272,10 @@ package Einfo is
 --       Float_Rep_Kind. Together with the Digits_Value uniquely defines
 --       the floating-point representation to be used.
 
+--    Formal_Proof_On (Flag254)
+--       Present in subprogram entities. Set for subprograms whose body
+--       contains an Annotate pragma which forces formal proof on this body.
+
 --    Freeze_Node (Node7)
 --       Present in all entities. If there is an associated freeze node for
 --       the entity, this field references this freeze node. If no freeze
@@ -6068,6 +6072,7 @@ package Einfo is
    function First_Private_Entity                (Id : E) return E;
    function First_Rep_Item                      (Id : E) return N;
    function Float_Rep                           (Id : E) return F;
+   function Formal_Proof_On                     (Id : E) return B;
    function Freeze_Node                         (Id : E) return N;
    function From_With_Type                      (Id : E) return B;
    function Full_View                           (Id : E) return E;
@@ -6657,6 +6662,7 @@ package Einfo is
    procedure Set_First_Private_Entity            (Id : E; V : E);
    procedure Set_First_Rep_Item                  (Id : E; V : N);
    procedure Set_Float_Rep                       (Id : E; V : F);
+   procedure Set_Formal_Proof_On                 (Id : E; V : B := True);
    procedure Set_Freeze_Node                     (Id : E; V : N);
    procedure Set_From_With_Type                  (Id : E; V : B := True);
    procedure Set_Full_View                       (Id : E; V : E);
@@ -7354,6 +7360,7 @@ package Einfo is
    pragma Inline (First_Optional_Parameter);
    pragma Inline (First_Private_Entity);
    pragma Inline (First_Rep_Item);
+   pragma Inline (Formal_Proof_On);
    pragma Inline (Freeze_Node);
    pragma Inline (From_With_Type);
    pragma Inline (Full_View);
@@ -7798,6 +7805,7 @@ package Einfo is
    pragma Inline (Set_First_Optional_Parameter);
    pragma Inline (Set_First_Private_Entity);
    pragma Inline (Set_First_Rep_Item);
+   pragma Inline (Set_Formal_Proof_On);
    pragma Inline (Set_Freeze_Node);
    pragma Inline (Set_From_With_Type);
    pragma Inline (Set_Full_View);
diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb
index 0e40946..a5038a9 100644
--- a/gcc/ada/exp_ch3.adb
+++ b/gcc/ada/exp_ch3.adb
@@ -5576,6 +5576,12 @@ package body Exp_Ch3 is
       if Restriction_Active (No_Finalization) then
          return;
 
+      --  Do not create TSS routine Finalize_Address when dispatching calls are
+      --  disabled since the core of the routine is a dispatching call.
+
+      elsif Restriction_Active (No_Dispatching_Calls) then
+         return;
+
       --  Do not create TSS routine Finalize_Address for concurrent class-wide
       --  types. Ignore C, C++, CIL and Java types since it is assumed that the
       --  non-Ada side will handle their destruction.
@@ -5588,17 +5594,17 @@ package body Exp_Ch3 is
       then
          return;
 
-      --  Do not create TSS routine Finalize_Address when dispatching calls are
-      --  disabled since the core of the routine is a dispatching call.
-
-      elsif Restriction_Active (No_Dispatching_Calls) then
-         return;
-
       --  Do not create TSS routine Finalize_Address for .NET/JVM because these
       --  targets do not support address arithmetic and unchecked conversions.
 
       elsif VM_Target /= No_VM then
          return;
+
+      --  Do not create TSS routine Finalize_Address when compiling in CodePeer
+      --  mode since the routine contains an Unchecked_Conversion.
+
+      elsif CodePeer_Mode then
+         return;
       end if;
 
       --  Generate the body of Finalize_Address. This routine is accessible
diff --git a/gcc/ada/gcc-interface/Make-lang.in b/gcc/ada/gcc-interface/Make-lang.in
index c418482..1f119ee 100644
--- a/gcc/ada/gcc-interface/Make-lang.in
+++ b/gcc/ada/gcc-interface/Make-lang.in
@@ -1297,16 +1297,20 @@ ada/a-ioexce.o : ada/ada.ads ada/a-except.ads ada/a-ioexce.ads \
 ada/ada.o : ada/ada.ads ada/system.ads 
 
 ada/alfa.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \
-   ada/a-uncdea.ads ada/alfa.ads ada/alfa.adb ada/alloc.ads ada/atree.ads \
-   ada/einfo.ads ada/snames.ads ada/interfac.ads ada/namet.ads \
-   ada/s-conca2.ads ada/sinfo.ads ada/table.ads ada/uintp.ads \
-   ada/urealp.ads ada/gnat.ads ada/g-table.ads \
-   ada/g-table.adb ada/hostparm.ads ada/output.ads ada/output.adb \
-   ada/put_alfa.ads ada/put_alfa.adb ada/system.ads ada/s-exctab.ads \
-   ada/s-memory.ads ada/s-os_lib.ads ada/s-parame.ads ada/s-soflin.ads \
-   ada/s-stache.ads ada/s-stalib.ads ada/s-stoele.ads ada/s-stoele.adb \
-   ada/s-string.ads ada/s-traent.ads ada/s-unstyp.ads ada/types.ads \
-   ada/unchconv.ads ada/unchdeal.ads 
+   ada/a-uncdea.ads ada/alfa.ads ada/alfa.adb ada/alloc.ads \
+   ada/aspects.ads ada/atree.ads ada/atree.adb ada/casing.ads \
+   ada/debug.ads ada/einfo.ads ada/gnat.ads ada/g-htable.ads \
+   ada/g-table.ads ada/g-table.adb ada/hostparm.ads ada/interfac.ads \
+   ada/namet.ads ada/namet.adb ada/nlists.ads ada/nlists.adb ada/opt.ads \
+   ada/output.ads ada/output.adb ada/put_alfa.ads ada/put_alfa.adb \
+   ada/sinfo.ads ada/sinfo.adb ada/sinput.ads ada/snames.ads \
+   ada/system.ads ada/s-exctab.ads ada/s-htable.ads ada/s-imenne.ads \
+   ada/s-memory.ads ada/s-os_lib.ads ada/s-parame.ads ada/s-secsta.ads \
+   ada/s-soflin.ads ada/s-stache.ads ada/s-stalib.ads ada/s-stoele.ads \
+   ada/s-stoele.adb ada/s-string.ads ada/s-traent.ads ada/s-unstyp.ads \
+   ada/s-wchcon.ads ada/table.ads ada/table.adb ada/tree_io.ads \
+   ada/types.ads ada/uintp.ads ada/uintp.adb ada/unchconv.ads \
+   ada/unchdeal.ads ada/urealp.ads ada/widechar.ads 
 
 ada/ali-util.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \
    ada/a-uncdea.ads ada/ali.ads ada/ali.adb ada/ali-util.ads \
@@ -2094,16 +2098,15 @@ ada/exp_ch7.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \
    ada/sem_ch8.ads ada/sem_ch9.ads ada/sem_dist.ads ada/sem_eval.ads \
    ada/sem_prag.ads ada/sem_res.ads ada/sem_type.ads ada/sem_util.ads \
    ada/sinfo.ads ada/sinfo.adb ada/sinput.ads ada/snames.ads ada/stand.ads \
-   ada/stringt.ads ada/stringt.adb ada/stylesw.ads ada/system.ads \
-   ada/s-exctab.ads ada/s-htable.ads ada/s-imenne.ads ada/s-memory.ads \
-   ada/s-os_lib.ads ada/s-parame.ads ada/s-rident.ads ada/s-secsta.ads \
-   ada/s-soflin.ads ada/s-stache.ads ada/s-stalib.ads ada/s-stoele.ads \
-   ada/s-stoele.adb ada/s-string.ads ada/s-traent.ads ada/s-unstyp.ads \
-   ada/s-wchcon.ads ada/table.ads ada/table.adb ada/targparm.ads \
-   ada/tbuild.ads ada/tbuild.adb ada/tree_io.ads ada/ttypes.ads \
-   ada/types.ads ada/uintp.ads ada/uintp.adb ada/uname.ads \
-   ada/unchconv.ads ada/unchdeal.ads ada/urealp.ads ada/validsw.ads \
-   ada/widechar.ads 
+   ada/stringt.ads ada/stylesw.ads ada/system.ads ada/s-exctab.ads \
+   ada/s-htable.ads ada/s-imenne.ads ada/s-memory.ads ada/s-os_lib.ads \
+   ada/s-parame.ads ada/s-rident.ads ada/s-secsta.ads ada/s-soflin.ads \
+   ada/s-stache.ads ada/s-stalib.ads ada/s-stoele.ads ada/s-stoele.adb \
+   ada/s-string.ads ada/s-traent.ads ada/s-unstyp.ads ada/s-wchcon.ads \
+   ada/table.ads ada/table.adb ada/targparm.ads ada/tbuild.ads \
+   ada/tbuild.adb ada/tree_io.ads ada/ttypes.ads ada/types.ads \
+   ada/uintp.ads ada/uintp.adb ada/uname.ads ada/unchconv.ads \
+   ada/unchdeal.ads ada/urealp.ads ada/validsw.ads ada/widechar.ads 
 
 ada/exp_ch8.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \
    ada/a-uncdea.ads ada/alloc.ads ada/aspects.ads ada/atree.ads \
@@ -2745,13 +2748,17 @@ ada/g-u3spch.o : ada/gnat.ads ada/g-spchge.ads ada/g-spchge.adb \
    ada/g-u3spch.ads ada/g-u3spch.adb ada/system.ads ada/s-wchcnv.ads \
    ada/s-wchcon.ads 
 
-ada/get_alfa.o : ada/ada.ads ada/a-ioexce.ads ada/a-unccon.ads \
-   ada/a-uncdea.ads ada/alfa.ads ada/alfa.adb ada/get_alfa.ads \
-   ada/get_alfa.adb ada/gnat.ads ada/g-table.ads ada/g-table.adb \
-   ada/hostparm.ads ada/output.ads ada/put_alfa.ads ada/system.ads \
-   ada/s-exctab.ads ada/s-memory.ads ada/s-os_lib.ads ada/s-stalib.ads \
-   ada/s-string.ads ada/s-unstyp.ads ada/types.ads ada/unchconv.ads \
-   ada/unchdeal.ads 
+ada/get_alfa.o : ada/ada.ads ada/a-except.ads ada/a-ioexce.ads \
+   ada/a-unccon.ads ada/a-uncdea.ads ada/alfa.ads ada/alfa.adb \
+   ada/alloc.ads ada/atree.ads ada/debug.ads ada/einfo.ads \
+   ada/get_alfa.ads ada/get_alfa.adb ada/gnat.ads ada/g-table.ads \
+   ada/g-table.adb ada/hostparm.ads ada/namet.ads ada/opt.ads \
+   ada/output.ads ada/put_alfa.ads ada/sinfo.ads ada/snames.ads \
+   ada/system.ads ada/s-exctab.ads ada/s-memory.ads ada/s-os_lib.ads \
+   ada/s-parame.ads ada/s-stalib.ads ada/s-string.ads ada/s-traent.ads \
+   ada/s-unstyp.ads ada/s-wchcon.ads ada/table.ads ada/table.adb \
+   ada/tree_io.ads ada/types.ads ada/uintp.ads ada/unchconv.ads \
+   ada/unchdeal.ads ada/urealp.ads 
 
 ada/get_scos.o : ada/ada.ads ada/a-ioexce.ads ada/a-unccon.ads \
    ada/get_scos.ads ada/get_scos.adb ada/gnat.ads ada/g-table.ads \
@@ -3303,12 +3310,16 @@ ada/prepcomp.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \
    ada/uintp.adb ada/uname.ads ada/unchconv.ads ada/unchdeal.ads \
    ada/urealp.ads ada/widechar.ads 
 
-ada/put_alfa.o : ada/ada.ads ada/a-unccon.ads ada/a-uncdea.ads \
-   ada/alfa.ads ada/alfa.adb ada/gnat.ads ada/g-table.ads ada/g-table.adb \
-   ada/hostparm.ads ada/output.ads ada/put_alfa.ads ada/put_alfa.adb \
-   ada/system.ads ada/s-exctab.ads ada/s-memory.ads ada/s-os_lib.ads \
-   ada/s-stalib.ads ada/s-string.ads ada/s-unstyp.ads ada/types.ads \
-   ada/unchconv.ads ada/unchdeal.ads 
+ada/put_alfa.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \
+   ada/a-uncdea.ads ada/alfa.ads ada/alfa.adb ada/alloc.ads ada/atree.ads \
+   ada/debug.ads ada/einfo.ads ada/gnat.ads ada/g-table.ads \
+   ada/g-table.adb ada/hostparm.ads ada/namet.ads ada/opt.ads \
+   ada/output.ads ada/put_alfa.ads ada/put_alfa.adb ada/sinfo.ads \
+   ada/snames.ads ada/system.ads ada/s-exctab.ads ada/s-memory.ads \
+   ada/s-os_lib.ads ada/s-parame.ads ada/s-stalib.ads ada/s-string.ads \
+   ada/s-traent.ads ada/s-unstyp.ads ada/s-wchcon.ads ada/table.ads \
+   ada/table.adb ada/tree_io.ads ada/types.ads ada/uintp.ads \
+   ada/unchconv.ads ada/unchdeal.ads ada/urealp.ads 
 
 ada/put_scos.o : ada/ada.ads ada/a-unccon.ads ada/gnat.ads ada/g-table.ads \
    ada/g-table.adb ada/put_scos.ads ada/put_scos.adb ada/scos.ads \
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);
 
diff --git a/gcc/ada/sem_ch2.adb b/gcc/ada/sem_ch2.adb
index f2c915b..d6db4d9 100644
--- a/gcc/ada/sem_ch2.adb
+++ b/gcc/ada/sem_ch2.adb
@@ -81,7 +81,7 @@ package body Sem_Ch2 is
            and then Is_Object (Entity (N))
            and then not Is_In_ALFA (Entity (N))
          then
-            Mark_Non_ALFA_Subprogram;
+            Mark_Non_ALFA_Subprogram ("object is not in 'A'L'F'A", N);
          end if;
       end if;
    end Analyze_Identifier;
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 081b7fa..401436d 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -3052,10 +3052,12 @@ package body Sem_Ch3 is
       --  The object is in ALFA if-and-only-if its type is in ALFA and it is
       --  not aliased.
 
-      if Is_In_ALFA (T) and then not Aliased_Present (N) then
-         Set_Is_In_ALFA (Id);
+      if not Is_In_ALFA (T) then
+         Mark_Non_ALFA_Subprogram ("object type is not in 'A'L'F'A", N);
+      elsif Aliased_Present (N) then
+         Mark_Non_ALFA_Subprogram ("ALIASED is not in 'A'L'F'A", N);
       else
-         Mark_Non_ALFA_Subprogram;
+         Set_Is_In_ALFA (Id);
       end if;
 
       --  These checks should be performed before the initialization expression
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index e04773a..44cda40 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -350,7 +350,7 @@ package body Sem_Ch4 is
 
    procedure Analyze_Aggregate (N : Node_Id) is
    begin
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("aggregate is not in 'A'L'F'A", N);
 
       if No (Etype (N)) then
          Set_Etype (N, Any_Composite);
@@ -371,7 +371,7 @@ package body Sem_Ch4 is
       C        : Node_Id;
 
    begin
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("allocator is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("allocator is not allowed", N);
 
       --  Deal with allocator restrictions
@@ -988,10 +988,10 @@ package body Sem_Ch4 is
          --  If this is an indirect call, or the subprogram called is not in
          --  ALFA, then the call is not in ALFA.
 
-         if not Is_Subprogram (Nam_Ent)
-           or else not Is_In_ALFA (Nam_Ent)
-         then
-            Mark_Non_ALFA_Subprogram;
+         if not Is_Subprogram (Nam_Ent) then
+            Mark_Non_ALFA_Subprogram ("indirect call is not in 'A'L'F'A", N);
+         elsif not Is_In_ALFA (Nam_Ent) then
+            Mark_Non_ALFA_Subprogram ("call to subprogram not in 'A'L'F'A", N);
          end if;
 
          Analyze_One_Call (N, Nam_Ent, True, Success);
@@ -1370,7 +1370,7 @@ package body Sem_Ch4 is
       L  : Node_Id;
 
    begin
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("concatenation is not in 'A'L'F'A", N);
 
       Candidate_Type := Empty;
 
@@ -1540,7 +1540,8 @@ package body Sem_Ch4 is
       --  resolution.
 
       if Present (Else_Expr) and then not In_Pre_Post_Expression then
-         Mark_Non_ALFA_Subprogram;
+         Mark_Non_ALFA_Subprogram
+           ("this form of conditional expression is not in 'A'L'F'A", N);
       end if;
 
       if Comes_From_Source (N) then
@@ -1739,7 +1740,7 @@ package body Sem_Ch4 is
    --  Start of processing for Analyze_Explicit_Dereference
 
    begin
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("explicit dereference is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("explicit dereference is not allowed", N);
 
       Analyze (P);
@@ -2622,7 +2623,7 @@ package body Sem_Ch4 is
 
    procedure Analyze_Null (N : Node_Id) is
    begin
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("null is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("null is not allowed", N);
 
       Set_Etype (N, Any_Access);
@@ -3254,7 +3255,7 @@ package body Sem_Ch4 is
       T    : Entity_Id;
 
    begin
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("qualified expression is not in 'A'L'F'A", N);
 
       Analyze_Expression (Expr);
 
@@ -3314,7 +3315,7 @@ package body Sem_Ch4 is
       Iterator : Node_Id;
 
    begin
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("quantified expression is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("quantified expression is not allowed", N);
 
       Set_Etype  (Ent,  Standard_Void_Type);
@@ -3480,7 +3481,7 @@ package body Sem_Ch4 is
       Acc_Type : Entity_Id;
 
    begin
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("reference is not in 'A'L'F'A", N);
 
       Analyze (P);
 
@@ -4346,7 +4347,7 @@ package body Sem_Ch4 is
    --  Start of processing for Analyze_Slice
 
    begin
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("slice is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("slice is not allowed", N);
 
       Analyze (P);
@@ -4416,7 +4417,8 @@ package body Sem_Ch4 is
       --  type conversions are not allowed.
 
       if not (Is_Scalar_Type (Etype (Expr)) and then Is_Scalar_Type (T)) then
-         Mark_Non_ALFA_Subprogram;
+         Mark_Non_ALFA_Subprogram
+           ("only type conversion between scalar types is in 'A'L'F'A", N);
       end if;
 
       --  Only remaining step is validity checks on the argument. These
@@ -4528,7 +4530,8 @@ package body Sem_Ch4 is
 
    procedure Analyze_Unchecked_Type_Conversion (N : Node_Id) is
    begin
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram
+        ("unchecked type conversion is not in 'A'L'F'A", N);
       Find_Type (Subtype_Mark (N));
       Analyze_Expression (Expression (N));
       Set_Etype (N, Entity (Subtype_Mark (N)));
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 239f9fe..b9c03c0 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -1113,7 +1113,8 @@ package body Sem_Ch5 is
       if Others_Present
         and then List_Length (Alternatives (N)) = 1
       then
-         Mark_Non_ALFA_Subprogram;
+         Mark_Non_ALFA_Subprogram
+           ("OTHERS as unique case alternative is not in 'A'L'F'A", N);
          Check_SPARK_Restriction
            ("OTHERS as unique case alternative is not allowed", N);
       end if;
@@ -1195,7 +1196,9 @@ package body Sem_Ch5 is
 
          else
             if Has_Loop_In_Inner_Open_Scopes (U_Name) then
-               Mark_Non_ALFA_Subprogram;
+               Mark_Non_ALFA_Subprogram
+                 ("exit label must name the closest enclosing loop"
+                   & " in 'A'L'F'A", N);
                Check_SPARK_Restriction
                  ("exit label must name the closest enclosing loop", N);
             end if;
@@ -1242,23 +1245,29 @@ package body Sem_Ch5 is
 
       if Present (Cond) then
          if Nkind (Parent (N)) /= N_Loop_Statement then
-            Mark_Non_ALFA_Subprogram;
+            Mark_Non_ALFA_Subprogram
+              ("exit with when clause must be directly in loop"
+                & " in 'A'L'F'A", N);
             Check_SPARK_Restriction
               ("exit with when clause must be directly in loop", N);
          end if;
 
       else
          if Nkind (Parent (N)) /= N_If_Statement then
-            Mark_Non_ALFA_Subprogram;
             if Nkind (Parent (N)) = N_Elsif_Part then
+               Mark_Non_ALFA_Subprogram
+                 ("exit must be in IF without ELSIF in 'A'L'F'A", N);
                Check_SPARK_Restriction
                  ("exit must be in IF without ELSIF", N);
             else
+               Mark_Non_ALFA_Subprogram
+                 ("exit must be directly in IF in 'A'L'F'A", N);
                Check_SPARK_Restriction ("exit must be directly in IF", N);
             end if;
 
          elsif Nkind (Parent (Parent (N))) /= N_Loop_Statement then
-            Mark_Non_ALFA_Subprogram;
+            Mark_Non_ALFA_Subprogram
+              ("exit must be in IF directly in loop in 'A'L'F'A", N);
             Check_SPARK_Restriction
               ("exit must be in IF directly in loop", N);
 
@@ -1266,14 +1275,16 @@ package body Sem_Ch5 is
             --  leads to an error mentioning the ELSE.
 
          elsif Present (Else_Statements (Parent (N))) then
-            Mark_Non_ALFA_Subprogram;
+            Mark_Non_ALFA_Subprogram
+              ("exit must be in IF without ELSE in 'A'L'F'A", N);
             Check_SPARK_Restriction ("exit must be in IF without ELSE", N);
 
             --  An exit in an ELSIF does not reach here, as it would have been
             --  detected in the case (Nkind (Parent (N)) /= N_If_Statement).
 
          elsif Present (Elsif_Parts (Parent (N))) then
-            Mark_Non_ALFA_Subprogram;
+            Mark_Non_ALFA_Subprogram
+              ("exit must be in IF without ELSIF in 'A'L'F'A", N);
             Check_SPARK_Restriction ("exit must be in IF without ELSIF", N);
          end if;
       end if;
@@ -1302,7 +1313,7 @@ package body Sem_Ch5 is
       Label_Ent   : Entity_Id;
 
    begin
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("goto statement is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("goto statement is not allowed", N);
 
       --  Actual semantic checks
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 854810f..4eaaaa6 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -649,13 +649,14 @@ package body Sem_Ch6 is
              (Nkind (Parent (Parent (N))) /= N_Subprogram_Body
                or else Present (Next (N)))
          then
-            Mark_Non_ALFA_Subprogram;
+            Mark_Non_ALFA_Subprogram
+              ("RETURN should be the last statement in 'A'L'F'A", N);
             Check_SPARK_Restriction
               ("RETURN should be the last statement in function", N);
          end if;
 
       else
-         Mark_Non_ALFA_Subprogram;
+         Mark_Non_ALFA_Subprogram ("extended RETURN is not in 'A'L'F'A", N);
          Check_SPARK_Restriction ("extended RETURN is not allowed", N);
 
          --  Analyze parts specific to extended_return_statement:
@@ -8886,7 +8887,7 @@ package body Sem_Ch6 is
          if Is_In_ALFA (Formal_Type) then
             Set_Is_In_ALFA (Formal);
          else
-            Mark_Non_ALFA_Subprogram;
+            Mark_Non_ALFA_Subprogram ("formal is not in 'A'L'F'A", Formal);
          end if;
 
          Default := Expression (Param_Spec);
diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb
index f535f7e..204ecad 100644
--- a/gcc/ada/sem_ch9.adb
+++ b/gcc/ada/sem_ch9.adb
@@ -101,7 +101,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("abort statement is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("abort statement is not allowed", N);
 
       T_Name := First (Names (N));
@@ -140,7 +140,7 @@ package body Sem_Ch9 is
    procedure Analyze_Accept_Alternative (N : Node_Id) is
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("accept is not in 'A'L'F'A", N);
 
       if Present (Pragmas_Before (N)) then
          Analyze_List (Pragmas_Before (N));
@@ -174,7 +174,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("accept statement is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("accept statement is not allowed", N);
 
       --  Entry name is initialized to Any_Id. It should get reset to the
@@ -406,7 +406,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("select statement is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (Max_Asynchronous_Select_Nesting, N);
       Check_Restriction (No_Select_Statements, N);
@@ -453,7 +453,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("select statement is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (No_Select_Statements, N);
 
@@ -500,7 +500,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("delay is not in 'A'L'F'A", N);
       Check_Restriction (No_Delay, N);
 
       if Present (Pragmas_Before (N)) then
@@ -552,7 +552,7 @@ package body Sem_Ch9 is
       E : constant Node_Id := Expression (N);
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("delay statement is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("delay statement is not allowed", N);
       Check_Restriction (No_Relative_Delay, N);
       Check_Restriction (No_Delay, N);
@@ -571,7 +571,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("delay statement is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("delay statement is not allowed", N);
       Check_Restriction (No_Delay, N);
       Check_Potentially_Blocking_Operation (N);
@@ -600,7 +600,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("entry is not in 'A'L'F'A", N);
 
       --  Entry_Name is initialized to Any_Id. It should get reset to the
       --  matching entry entity. An error is signalled if it is not reset
@@ -833,7 +833,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("entry is not in 'A'L'F'A", N);
 
       if Present (Index) then
          Analyze (Index);
@@ -861,7 +861,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("entry call is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("entry call is not allowed", N);
 
       if Present (Pragmas_Before (N)) then
@@ -897,7 +897,7 @@ package body Sem_Ch9 is
    begin
       Generate_Definition (Def_Id);
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("entry is not in 'A'L'F'A", N);
 
       --  Case of no discrete subtype definition
 
@@ -967,7 +967,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("entry is not in 'A'L'F'A", N);
       Analyze (Def);
 
       --  There is no elaboration of the entry index specification. Therefore,
@@ -1009,7 +1009,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("protected body is not in 'A'L'F'A", N);
       Set_Ekind (Body_Id, E_Protected_Body);
       Spec_Id := Find_Concurrent_Spec (Body_Id);
 
@@ -1128,7 +1128,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("protected definition is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("protected definition is not allowed", N);
       Analyze_Declarations (Visible_Declarations (N));
 
@@ -1182,7 +1182,7 @@ package body Sem_Ch9 is
       end if;
 
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("protected type is not in 'A'L'F'A", N);
       Check_Restriction (No_Protected_Types, N);
 
       T := Find_Type_Name (N);
@@ -1324,7 +1324,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("requeue statement is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("requeue statement is not allowed", N);
       Check_Restriction (No_Requeue_Statements, N);
       Check_Unreachable_Code (N);
@@ -1599,7 +1599,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("select statement is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (No_Select_Statements, N);
 
@@ -1720,7 +1720,7 @@ package body Sem_Ch9 is
    begin
       Generate_Definition (Id);
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("protected object is not in 'A'L'F'A", N);
 
       --  The node is rewritten as a protected type declaration, in exact
       --  analogy with what is done with single tasks.
@@ -1782,7 +1782,7 @@ package body Sem_Ch9 is
    begin
       Generate_Definition (Id);
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("task is not in 'A'L'F'A", N);
 
       --  The node is rewritten as a task type declaration, followed by an
       --  object declaration of that anonymous task type.
@@ -1860,7 +1860,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("task body is not in 'A'L'F'A", N);
       Set_Ekind (Body_Id, E_Task_Body);
       Set_Scope (Body_Id, Current_Scope);
       Spec_Id := Find_Concurrent_Spec (Body_Id);
@@ -1981,7 +1981,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("task definition is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("task definition is not allowed", N);
 
       if Present (Visible_Declarations (N)) then
@@ -2016,7 +2016,7 @@ package body Sem_Ch9 is
    begin
       Check_Restriction (No_Tasking, N);
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("task type is not in 'A'L'F'A", N);
       T := Find_Type_Name (N);
       Generate_Definition (T);
 
@@ -2122,7 +2122,7 @@ package body Sem_Ch9 is
    procedure Analyze_Terminate_Alternative (N : Node_Id) is
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("terminate is not in 'A'L'F'A", N);
 
       if Present (Pragmas_Before (N)) then
          Analyze_List (Pragmas_Before (N));
@@ -2144,7 +2144,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("select statement is not in 'A'L'F'A", N);
       Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (No_Select_Statements, N);
 
@@ -2181,7 +2181,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Mark_Non_ALFA_Subprogram;
+      Mark_Non_ALFA_Subprogram ("triggering statement is not in 'A'L'F'A", N);
 
       if Present (Pragmas_Before (N)) then
          Analyze_List (Pragmas_Before (N));
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 4ce7ec5..e992315 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -6103,6 +6103,53 @@ package body Sem_Prag is
                Exp : Node_Id;
 
             begin
+               if Chars (Get_Pragma_Arg (Arg1)) = Name_Formal_Proof then
+                  if No (Arg2) then
+                     Error_Pragma_Arg
+                       ("missing second argument for pragma%", Arg1);
+                  end if;
+
+                  Check_Arg_Is_Identifier (Arg2);
+                  Check_Arg_Count (2);
+
+                  if Chars (Get_Pragma_Arg (Arg2)) /= Name_On
+                    and then Chars (Get_Pragma_Arg (Arg2)) /= Name_Off
+                  then
+                     Error_Pragma_Arg
+                       ("wrong second argument for pragma%", Arg2);
+                  end if;
+
+                  if Chars (Get_Pragma_Arg (Arg2)) = Name_On then
+                     declare
+                        Cur_Subp : constant Entity_Id := Current_Subprogram;
+
+                     begin
+                        if Present (Cur_Subp)
+                          and then (Is_Subprogram (Cur_Subp)
+                                     or else Is_Generic_Subprogram (Cur_Subp))
+                        then
+                           --  Notify user if some ALFA violation occurred
+                           --  before this point in Cur_Subp. These violations
+                           --  are not precisly located, but this is better
+                           --  than ignoring them.
+
+                           if not Is_In_ALFA (Cur_Subp)
+                             or else not Body_Is_In_ALFA (Cur_Subp)
+                           then
+                              Error_Pragma
+                                ("pragma% is placed after violation"
+                                 & " of 'A'L'F'A");
+                           end if;
+
+                           Set_Formal_Proof_On (Cur_Subp);
+
+                        else
+                           Error_Pragma ("wrong placement for pragma%");
+                        end if;
+                     end;
+                  end if;
+               end if;
+
                --  Second unanalyzed parameter is optional
 
                if No (Arg2) then
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 3286e3a..241abd6 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -5796,12 +5796,14 @@ package body Sem_Res is
       --  types or array types except String.
 
       if Is_Boolean_Type (T) then
-         Mark_Non_ALFA_Subprogram;
+         Mark_Non_ALFA_Subprogram
+           ("ordering operator on boolean type is not in 'A'L'F'A", N);
          Check_SPARK_Restriction
            ("comparison is not defined on Boolean type", N);
 
       elsif Is_Array_Type (T) then
-         Mark_Non_ALFA_Subprogram;
+         Mark_Non_ALFA_Subprogram
+           ("ordering operator on array type is not in 'A'L'F'A", N);
 
          if Base_Type (T) /= Standard_String then
             Check_SPARK_Restriction
@@ -5861,7 +5863,8 @@ package body Sem_Res is
       end if;
 
       if Root_Type (Typ) /= Standard_Boolean then
-         Mark_Non_ALFA_Subprogram;
+         Mark_Non_ALFA_Subprogram
+           ("non-boolean conditional expression is not in 'A'L'F'A", N);
       end if;
 
       Set_Etype (N, Typ);
@@ -6664,7 +6667,8 @@ package body Sem_Res is
          --  operands have equal static bounds.
 
          if Is_Array_Type (T) then
-            Mark_Non_ALFA_Subprogram;
+            Mark_Non_ALFA_Subprogram
+              ("equality operator on array is not in 'A'L'F'A", N);
 
             --  Protect call to Matching_Static_Array_Bounds to avoid costly
             --  operation if not needed.
@@ -7214,7 +7218,8 @@ package body Sem_Res is
       if Is_Array_Type (B_Typ)
         and then Nkind (N) in N_Binary_Op
       then
-         Mark_Non_ALFA_Subprogram;
+         Mark_Non_ALFA_Subprogram
+           ("binary operator on array is not in 'A'L'F'A", N);
 
          declare
             Left_Typ  : constant Node_Id := Etype (Left_Opnd (N));
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index e62d013..2a90f67 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -141,9 +141,13 @@ package body Sem_Util is
    --  T is a derived tagged type. Check whether the type extension is null.
    --  If the parent type is fully initialized, T can be treated as such.
 
-   procedure Mark_Non_ALFA_Subprogram_Unconditional;
+   procedure Mark_Non_ALFA_Subprogram_Unconditional
+     (Msg : String;
+      N   : Node_Id);
    --  Perform the action for Mark_Non_ALFA_Subprogram_Body, which allows the
-   --  latter to be small and inlined.
+   --  latter to be small and inlined. 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.
 
    ------------------------------
    --  Abstract_Interface_List --
@@ -2323,13 +2327,13 @@ package body Sem_Util is
    -- Mark_Non_ALFA_Subprogram --
    ------------------------------
 
-   procedure Mark_Non_ALFA_Subprogram is
+   procedure Mark_Non_ALFA_Subprogram (Msg : String; N : Node_Id) is
    begin
       --  Isolate marking of the current subprogram body so that the body of
       --  Mark_Non_ALFA_Subprogram is small and inlined.
 
       if ALFA_Mode then
-         Mark_Non_ALFA_Subprogram_Unconditional;
+         Mark_Non_ALFA_Subprogram_Unconditional (Msg, N);
       end if;
    end Mark_Non_ALFA_Subprogram;
 
@@ -2337,7 +2341,10 @@ package body Sem_Util is
    -- Mark_Non_ALFA_Subprogram_Unconditional --
    --------------------------------------------
 
-   procedure Mark_Non_ALFA_Subprogram_Unconditional is
+   procedure Mark_Non_ALFA_Subprogram_Unconditional
+     (Msg : String;
+      N   : Node_Id)
+   is
       Cur_Subp : constant Entity_Id := Current_Subprogram;
 
    begin
@@ -2345,12 +2352,22 @@ package body Sem_Util is
         and then (Is_Subprogram (Cur_Subp)
                    or else Is_Generic_Subprogram (Cur_Subp))
       then
+         --  If the subprogram has been annotated with Formal_Proof being On,
+         --  then an error must be issued to notify the user that this
+         --  subprogram unexpectedly falls outside the ALFA subset.
+
+         if Formal_Proof_On (Cur_Subp) then
+            Error_Msg_F (Msg, N);
+         end if;
+
          --  If the non-ALFA construct is in a precondition or postcondition,
-         --  then mark the subprogram as not in ALFA. Otherwise, mark the
-         --  subprogram body as not in ALFA.
+         --  then mark the subprogram as not in ALFA, because neither the
+         --  subprogram nor its callers can be proved formally.
 
-         --  This comment just says what is done, but not why ??? and it
-         --  just repeats what is in the spec ???
+         --  If the non-ALFA construct is in a regular piece of code inside the
+         --  body of the subprogram, then mark the subprogram body as not in
+         --  ALFA, because the subprogram cannot be proved formally, but its
+         --  callers could.
 
          if In_Pre_Post_Expression then
             Set_Is_In_ALFA (Cur_Subp, False);
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
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index 818cc8b..c3c7bea 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -629,6 +629,7 @@ package Snames is
    Name_External_Name                  : constant Name_Id := N + $;
    Name_First_Optional_Parameter       : constant Name_Id := N + $;
    Name_Form                           : constant Name_Id := N + $;
+   Name_Formal_Proof                   : constant Name_Id := N + $;
    Name_G_Float                        : constant Name_Id := N + $;
    Name_Gcc                            : constant Name_Id := N + $;
    Name_Gnat                           : constant Name_Id := N + $;