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 <squi...@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.
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 253559)
+++ sem_ch3.adb (working copy)
@@ -2233,9 +2233,11 @@
-- Utility to resolve the expressions of aspects at the end of a list of
-- declarations.
- function Uses_Unseen_Lib_Unit_Priv (Pkg : Entity_Id) return Boolean;
- -- Check if an inner package has entities within it that rely on library
- -- level private types where the full view has not been seen.
+ function Uses_Unseen_Priv (Pkg : Entity_Id) return Boolean;
+ -- Check if a nested package has entities within it that rely on library
+ -- level private types where the full view has not been seen for the
+ -- purposes of checking if it is acceptable to freeze an expression
+ -- function at the point of declaration.
-----------------
-- Adjust_Decl --
@@ -2540,11 +2542,11 @@
end loop;
end Resolve_Aspects;
- -------------------------------
- -- Uses_Unseen_Lib_Unit_Priv --
- -------------------------------
+ ----------------------
+ -- Uses_Unseen_Priv --
+ ----------------------
- function Uses_Unseen_Lib_Unit_Priv (Pkg : Entity_Id) return Boolean is
+ function Uses_Unseen_Priv (Pkg : Entity_Id) return Boolean is
Curr : Entity_Id;
begin
@@ -2572,7 +2574,7 @@
end if;
return False;
- end Uses_Unseen_Lib_Unit_Priv;
+ end Uses_Unseen_Priv;
-- Local variables
@@ -2753,8 +2755,9 @@
elsif not Analyzed (Next_Decl) and then Is_Body (Next_Decl)
and then ((Nkind (Next_Decl) /= N_Subprogram_Body
- or else not Was_Expression_Function (Next_Decl))
- or else not Uses_Unseen_Lib_Unit_Priv (Current_Scope))
+ or else not Was_Expression_Function (Next_Decl))
+ or else (not Is_Ignored_Ghost_Entity (Current_Scope)
+ and then not Uses_Unseen_Priv (Current_Scope)))
then
-- When a controlled type is frozen, the expander generates stream
-- and controlled-type support routines. If the freeze is caused
