This patch suppresses the generation of the Initial_Condition procedure
tasked with verifying the run-time semantics of the pragma when the
pragma is ignored by means of -gnata, pragma Assertion_Policy, etc.

------------
-- Source --
------------

--  all_asserts_off.adc

pragma Assertion_Policy (Ignore);

--  all_asserts_on.adc

pragma Assertion_Policy (Check);

--  ic_off.adc

pragma Assertion_Policy (Initial_Condition => Ignore);

--  ic_on.adc

pragma Assertion_Policy (Initial_Condition => Check);

--  init_cond.ads

package Init_Cond
  with SPARK_Mode,
       Initial_Condition => Flag = False
is
   Flag : Boolean := True;

   procedure Set_Flag;
end Init_Cond;

--  init_cond.adb

package body Init_Cond
  with SPARK_Mode
is
   procedure Set_Flag is
   begin
      Flag := True;
   end Set_Flag;
end Init_Cond;

----------------------------
-- Compilation and output --
----------------------------

& gcc  -c -S -gnatDG init_cond.adb -gnatec=all_asserts_on.adc
& grep -c "Initial_Condition;" init_cond.adb.dg
& grep -c "_elabb" init_cond.s
& gcc  -c -S -gnatDG init_cond.adb -gnatec=ic_on.adc
& grep -c "Initial_Condition;" init_cond.adb.dg
& grep -c "_elabb" init_cond.s
& gcc  -c -S -gnatDG init_cond.adb -gnatec=all_asserts_off.adc
& grep -c "Initial_Condition;" init_cond.adb.dg
& grep -c "_elabb" init_cond.s
& gcc  -c -S -gnatDG init_cond.adb -gnatec=ic_off.adc
& grep -c "Initial_Condition;" init_cond.adb.dg
& grep -c "_elabb" init_cond.s
2
4
2
4
0
0
0
0

Tested on x86_64-pc-linux-gnu, committed on trunk

2018-12-11  Hristian Kirtchev  <kirtc...@adacore.com>

gcc/ada/

        * exp_prag.adb (Expand_Pragma_Initial_Condition): Do not
        generate an Initial_Condition procedure and a call to it when
        the associated pragma is ignored.
        * sem_ch10.adb (Analyze_Compilation_Unit): Minor cleanup.
--- gcc/ada/exp_prag.adb
+++ gcc/ada/exp_prag.adb
@@ -1636,10 +1636,16 @@ package body Exp_Prag is
       Expr := Get_Pragma_Arg (First (Pragma_Argument_Associations (IC_Prag)));
       Loc  := Sloc (IC_Prag);
 
+      --  Nothing to do when the pragma is ignored because its semantics are
+      --  suppressed.
+
+      if Is_Ignored (IC_Prag) then
+         return;
+
       --  Nothing to do when the pragma or its argument are illegal because
       --  there is no valid expression to check.
 
-      if Error_Posted (IC_Prag) or else Error_Posted (Expr) then
+      elsif Error_Posted (IC_Prag) or else Error_Posted (Expr) then
          return;
       end if;
 

--- gcc/ada/sem_ch10.adb
+++ gcc/ada/sem_ch10.adb
@@ -1203,8 +1203,6 @@ package body Sem_Ch10 is
             --  binder generated code of all the units involved in a partition
             --  when control-flow preservation is requested.
 
-            --  Case of units which do not require an elaboration entity
-
             if not Opt.Suppress_Control_Flow_Optimizations
               and then
               ( --  Pure units do not need checks
@@ -1232,16 +1230,16 @@ package body Sem_Ch10 is
                 or else Acts_As_Spec (N)
               )
             then
-               --  This is a case where we only need the entity for
-               --  checking to prevent multiple elaboration checks.
+               --  This is a case where we only need the entity for checking to
+               --  prevent multiple elaboration checks.
 
                Set_Elaboration_Entity_Required (Spec_Id, False);
 
-            --  Case of elaboration entity is required for access before
-            --  elaboration checking (so certainly we must build it).
+            --  Otherwise the unit requires an elaboration entity because it
+            --  carries a body.
 
             else
-               Set_Elaboration_Entity_Required (Spec_Id, True);
+               Set_Elaboration_Entity_Required (Spec_Id);
             end if;
 
             Build_Elaboration_Entity (N, Spec_Id);

Reply via email to