[Ada] Internal error on expression function in ghost package

Message ID 20171009200054.GA44565@adacore.com
State New
Headers show
Series
  • [Ada] Internal error on expression function in ghost package
Related show

Commit Message

Pierre-Marie de Rodat Oct. 9, 2017, 8 p.m.
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.

Patch

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