[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
Showing
Please
register
or
sign in
to comment