[Ada] Suppress call to Initial_Condition when the annotation is ignored

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

2018-12-11  Hristian Kirtchev  <kirtchev@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.

From-SVN: r266977

0 files changed, 0 insertions, 0 deletions