public inbox for gcc-patches@gcc.gnu.org
 help / color / mirror / Atom feed
From: Arnaud Charlet <charlet@adacore.com>
To: gcc-patches@gcc.gnu.org
Cc: Ed Schonberg <schonberg@adacore.com>
Subject: [Ada] Missing predicate functions for private types.
Date: Tue, 25 Apr 2017 13:05:00 -0000	[thread overview]
Message-ID: <20170425125857.GA37277@adacore.com> (raw)

[-- Attachment #1: Type: text/plain, Size: 1846 bytes --]

This patch fixes an omission in the generation of predicate functions for
private types whose full view derives from a subtype with predicates.

Executing the following:

   gnatmake -gnata -q predicate_check
   predicate_check

must yield;

   OK derived subtype
   OK original subtype

---
with Text_IO; use Text_IO;
with Ada.Assertions; use Ada.Assertions;
procedure Predicate_Check with SPARK_Mode is
   type R is --  new Integer;
    record
      F : Integer := 42;
    end record;

   package Nested is
      subtype S is R with Predicate => S.F = 42;
      --  subtype S is R with Predicate => S = 42;
      procedure P (X : in out S) is null;

      type T is private;
      procedure P (X : in out T);
   private
      type T is new S;
   end Nested;
   package body Nested is
      procedure P (X : in out T) is
      begin
         X.F := X.F * 7;
      end;
   end Nested;

   X : Nested.T;
   Y : Nested.S;
begin
   Y.F := Y.F * 3;
   begin
      Nested.P (X);
      Put_Line ("should not be here");
   exception
      when Assertion_Error => Put_Line ("OK derived subtype");
   end;

   begin
      Nested.P (Y);
      Put_Line ("should not be here");
   exception
      when Assertion_Error => Put_Line ("OK original subtype");
   end;
end Predicate_Check;

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

2017-04-25  Ed Schonberg  <schonberg@adacore.com>

	* sem_aux.adb (Nearest_Ancestor): Use original node of type
	declaration to locate nearest ancestor, because derived
	type declarations for record types are rewritten as record
	declarations.
	* sem_ch13.adb (Add_Call): Use an unchecked conversion to handle
	properly derivations that are completions of private types.
	(Add_Predicates): If type is private, examine rep. items of full
	view, which may include inherited predicates.
	(Build_Predicate_Functions): Ditto.


[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 3886 bytes --]

Index: sem_aux.adb
===================================================================
--- sem_aux.adb	(revision 247177)
+++ sem_aux.adb	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -1295,7 +1295,10 @@
    ----------------------
 
    function Nearest_Ancestor (Typ : Entity_Id) return Entity_Id is
-      D : constant Node_Id := Declaration_Node (Typ);
+      D : constant Node_Id := Original_Node (Declaration_Node (Typ));
+      --  We use the original node of the declaration, because derived
+      --  types from record subtypes are rewritten as record declarations,
+      --  and it is the original declaration that carries the ancestor.
 
    begin
       --  If we have a subtype declaration, get the ancestor subtype
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 247218)
+++ sem_ch13.adb	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -8309,11 +8309,15 @@
          if Present (T) and then Present (Predicate_Function (T)) then
             Set_Has_Predicates (Typ);
 
-            --  Build the call to the predicate function of T
+            --  Build the call to the predicate function of T. The type may be
+            --  derived, so use an unchecked conversion for the actual.
 
             Exp :=
               Make_Predicate_Call
-                (T, Convert_To (T, Make_Identifier (Loc, Object_Name)));
+                (Typ  => T,
+                 Expr =>
+                   Unchecked_Convert_To (T,
+                     Make_Identifier (Loc, Object_Name)));
 
             --  "and"-in the call to evolving expression
 
@@ -8456,6 +8460,14 @@
 
       begin
          Ritem := First_Rep_Item (Typ);
+
+         --  If the type is private, check whether full view has inherited
+         --  predicates.
+
+         if Is_Private_Type (Typ) and then No (Ritem) then
+            Ritem := First_Rep_Item (Full_View (Typ));
+         end if;
+
          while Present (Ritem) loop
             if Nkind (Ritem) = N_Pragma
               and then Pragma_Name (Ritem) = Name_Predicate
@@ -8562,8 +8574,16 @@
       --  ones for the current type, as required by AI12-0071-1.
 
       declare
-         Atyp : constant Entity_Id := Nearest_Ancestor (Typ);
+         Atyp : Entity_Id;
       begin
+         Atyp := Nearest_Ancestor (Typ);
+
+         --  The type may be private but the full view may inherit predicates
+
+         if No (Atyp) and then Is_Private_Type (Typ) then
+            Atyp := Nearest_Ancestor (Full_View (Typ));
+         end if;
+
          if Present (Atyp) then
             Add_Call (Atyp);
          end if;

                 reply	other threads:[~2017-04-25 12:58 UTC|newest]

Thread overview: [no followups] expand[flat|nested]  mbox.gz  Atom feed

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20170425125857.GA37277@adacore.com \
    --to=charlet@adacore.com \
    --cc=gcc-patches@gcc.gnu.org \
    --cc=schonberg@adacore.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).