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);