This patch suppresses the generation of elaboration counters and access-before-
elaboration checks for GNATprove compilations.
------------
-- Source --
------------
-- dic.ads
package Dic with Elaborate_Body Is
G : Integer;
type T is private with Default_Initial_Condition => Foo (T);
function Foo (Par : T) return Boolean;
private
type T is new Integer with Default_Value => 0;
end Dic;
-- dic.adb
package body Dic is
B : T;
function Foo (Par : T) return Boolean is (Integer (Par) = G);
begin
G := 0;
end Dic;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c -gnatd.F -gnatdI -gnatDG dic.adb > dic.adb.dg
$ grep -c "E" dic.adb.dg
0
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-04-27 Hristian Kirtchev <[email protected]>
* sem_elab.adb (Check_Internal_Call_Continue): Do not generate
an elaboration counter nor a check when in GNATprove mode.
* sem_util.adb (Build_Elaboration_Entity): Do not create an
elaboration counter when in GNATprove mode.
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 247313)
+++ sem_util.adb (working copy)
@@ -1584,8 +1584,14 @@
elsif ASIS_Mode then
return;
- -- See if we need elaboration entity.
+ -- Do not generate an elaboration entity in GNATprove move because the
+ -- elaboration counter is a form of expansion.
+ elsif GNATprove_Mode then
+ return;
+
+ -- See if we need elaboration entity
+
-- We always need an elaboration entity when preserving control flow, as
-- we want to remain explicit about the unit's elaboration order.
Index: sem_elab.adb
===================================================================
--- sem_elab.adb (revision 247301)
+++ sem_elab.adb (working copy)
@@ -2573,9 +2573,15 @@
-- Call is not at outer level
else
+ -- Do not generate elaboration checks in GNATprove mode because the
+ -- elaboration counter and the check are both forms of expansion.
+
+ if GNATprove_Mode then
+ null;
+
-- Deal with dynamic elaboration check
- if not Elaboration_Checks_Suppressed (E) then
+ elsif not Elaboration_Checks_Suppressed (E) then
Set_Elaboration_Entity_Required (E);
-- Case of no elaboration entity allocated yet
