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] |
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] |