[Ada] Refine expansion in Alfa mode

Index: exp_ch9.adb
===================================================================
--- exp_ch9.adb	(revision 178306)
+++ exp_ch9.adb	(working copy)
@@ -4906,14 +4906,10 @@ 
       Ldecl2 : Node_Id;
 
    begin
-      --  In formal verification mode, do not expand tasking constructs
+      if Expander_Active
+        and then not ALFA_Mode
+      then
 
-      if ALFA_Mode then
-         return;
-      end if;
-
-      if Expander_Active then
-
          --  If we have no handled statement sequence, we may need to build
          --  a dummy sequence consisting of a null statement. This can be
          --  skipped if the trivial accept optimization is permitted.
@@ -11599,7 +11595,9 @@ 
          Error_Msg_CRT ("protected body", N);
          return;
 
-      elsif Expander_Active then
+      elsif Expander_Active
+        and then not ALFA_Mode
+      then
 
          --  Associate discriminals with the first subprogram or entry body to
          --  be expanded.
Index: sem_ch9.adb
===================================================================
--- sem_ch9.adb	(revision 178304)
+++ sem_ch9.adb	(working copy)
@@ -1280,6 +1280,7 @@ 
 
          if Serious_Errors_Detected = 0
            and then Expander_Active
+           and then not ALFA_Mode
          then
             Expand_N_Protected_Type_Declaration (N);
             Process_Full_View (N, T, Def_Id);
@@ -2083,6 +2084,7 @@ 
 
          if Serious_Errors_Detected = 0
            and then Expander_Active
+           and then not ALFA_Mode
          then
             Expand_N_Task_Type_Declaration (N);
             Process_Full_View (N, T, Def_Id);
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 178303)
+++ sem_res.adb	(working copy)
@@ -3443,6 +3443,7 @@ 
               and then Is_Limited_Record (Etype (F))
               and then not Is_Constrained (Etype (F))
               and then Expander_Active
+              and then not ALFA_Mode
               and then (Is_Controlled (Etype (F)) or else Has_Task (Etype (F)))
             then
                Establish_Transient_Scope (A, False);
@@ -3458,6 +3459,7 @@ 
             elsif Nkind (A) = N_Op_Concat
               and then Nkind (N) = N_Procedure_Call_Statement
               and then Expander_Active
+              and then not ALFA_Mode
               and then
                 not (Is_Intrinsic_Subprogram (Nam)
                       and then Chars (Nam) = Name_Asm)
@@ -3521,6 +3523,7 @@ 
 
                      if (Is_Controlled (DDT) or else Has_Task (DDT))
                        and then Expander_Active
+                       and then not ALFA_Mode
                      then
                         Establish_Transient_Scope (A, False);
                      end if;
@@ -5492,6 +5495,7 @@ 
          null;
 
       elsif Expander_Active
+        and then not ALFA_Mode
         and then Is_Type (Etype (Nam))
         and then Requires_Transient_Scope (Etype (Nam))
         and then
@@ -6613,6 +6617,7 @@ 
       --  case we must trigger the transient scope mechanism.
 
       elsif Expander_Active
+        and then not ALFA_Mode
         and then Requires_Transient_Scope (Etype (Nam))
       then
          Establish_Transient_Scope (N, Sec_Stack => True);
Index: exp_disp.adb
===================================================================
--- exp_disp.adb	(revision 178293)
+++ exp_disp.adb	(working copy)
@@ -702,6 +702,7 @@ 
       --  of this restriction.
 
       if not Expander_Active
+        or else ALFA_Mode
         or else Restriction_Active (No_Dispatching_Calls)
       then
          return;