diff mbox series

[Ada] Check elaboration requirement for SPARK in the static model

Message ID 20171009203702.GA1231@adacore.com
State New
Headers show
Series [Ada] Check elaboration requirement for SPARK in the static model | expand

Commit Message

Pierre-Marie de Rodat Oct. 9, 2017, 8:37 p.m. UTC 
This patch ensures that the Elaborate[_All] requirement imposed on the context
of a unit in SPARK code is verified only when the static model is in effect.

------------
-- Source --
------------

--  server.ads

package Server with SPARK_Mode is
   function Read return Integer;
end Server;

--  server.adb

package body Server with SPARK_Mode is
   function Read return Integer is
   begin
      return 0;
   end Read;
end Server;

--  client.ads

package Client with SPARK_Mode is
   function Prf return Boolean;
end Client;

--  client.adb

with Server;

package body Client with SPARK_Mode is
   function Prf return Boolean is
   begin
      return Server.Read = 0;
   end Prf;
end Client;

-----------------
-- Compilation --
-----------------

$ gcc -c client.adb
$ gcc -c client.adb -gnatE

Tested on x86_64-pc-linux-gnu, committed on trunk

2017-10-09  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_elab.adb (Static_Elaboration_Checks): Elaboration requirements
	are verified only in the static model.
diff mbox series

Patch

Index: sem_elab.adb
===================================================================
--- sem_elab.adb	(revision 253564)
+++ sem_elab.adb	(working copy)
@@ -5516,12 +5516,18 @@ 
 
       Req_Met := False;
 
+      --  Elaboration requirements are verified only when the static model is
+      --  in effect because this diagnostic is graph-dependent.
+
+      if not Static_Elaboration_Checks then
+         return;
+
       --  If the target is within the main unit, either at the source level or
       --  through an instantiation, then there is no real requirement to meet
       --  because the main unit cannot force its own elaboration by means of an
       --  Elaborate[_All] pragma. Treat this case as valid coverage.
 
-      if In_Extended_Main_Code_Unit (Target_Id) then
+      elsif In_Extended_Main_Code_Unit (Target_Id) then
          Req_Met := True;
 
       --  Otherwise the target resides in an external unit