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] Missing predicate functions for private types.


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: difs
Description: Text document


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