This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

[Ada] Internal error on expression function in ghost package


This patch corrects an issue whereby an expression function within a ghost
package would cause orphaned freeze nodes.

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

--  p.ads

package P
  with SPARK_Mode
is
   type Rec is record
      I : Integer;
   end record;
   package Inner with Ghost is
      function F (I : Integer) return Integer is (I);
      function Zero (B : Rec) return Integer;
   end Inner;
   procedure Proc (B : Rec);
end P;

--  p.adb

package body P
  with SPARK_Mode
is
   package body Inner is
      function Zero (B : Rec) return Integer is
      begin
         return 0;
      end;
   end Inner;
   procedure Proc (B : Rec) is
   begin
       if B.I = 0 then
          raise Program_Error;
       end if;
   end;
end P;

--  buffers.ads

with Ada.Containers.Functional_Vectors;
package Buffers
  with SPARK_Mode
is
   subtype Resource is Natural range 0 .. 1000;
   subtype Num is Natural range 0 .. 6;
   subtype Index is Num range 1 .. 6;
   type Data is array (Index) of Resource;
   type Buffer is record
      D : Data;
      K : Index;
   end record;
   package Models with Ghost is
      package Seqs is new Ada.Containers.Functional_Vectors (Index, Resource);
      use Seqs;
      function Rotate_Right (S : Sequence) return Sequence is
        (Add (Remove (S, First), Get (S, First)));
      function Model (B : Buffer) return Sequence;
   end Models;
   use Models;
   use Models.Seqs;
   procedure Bump (B : in out Buffer) with
     Post => Model(B) = Model(B);
end Buffers;

--  buffers.adb

with Ada.Containers.Functional_Vectors;
package body Buffers
  with SPARK_Mode
is
   package body Models is
      function Model (B : Buffer) return Sequence is
         S : Sequence;
      begin
         for J in B.K .. Index'Last loop
            S := Add (S, B.D(J));
         end loop;
         for J in Index'First .. B.K-1 loop
            S := Add (S, B.D(J));
         end loop;
         return S;
      end Model;
   end Models;
   procedure Bump (B : in out Buffer) is
   begin
      if B.K = Index'Last then
         B.K := Index'First;
      else
         B.K := B.K + 1;
      end if;
   end Bump;
end Buffers;

----------------------------
-- Compilation and output --
----------------------------

& gcc -c buffers.adb
& gcc -c p.adb

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

2017-10-09  Justin Squirek  <squirek@adacore.com>

	* sem_ch3.adb (Analyze_Declarations): Add check for ghost packages
	before analyzing a given scope due to an expression function.
	(Uses_Unseen_Lib_Unit_Priv): Rename to Uses_Unseen_Priv.

Attachment: difs
Description: Text document


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]