diff mbox

[Ada] Removal of elaboration-related flags for SPARK

Message ID 20170427105530.GA6314@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet April 27, 2017, 10:55 a.m. UTC 
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  <kirtchev@adacore.com>

	* 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.
diff mbox

Patch

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