[Ada] Spurious visibility error for operator in pre-condition

[Arnaud Charlet <charlet at adacore dot com>]

If a user-defined operator renames a predefined one, a use of that operator is
rewritten with the predefined one, because the back-end requires it. This
transformation must not be performed when analyzing the expression in a pre- or
postcondition aspect or pragma, because the expression will be reanalyzed at a
later point, and the rewriting may affect vsibility of the operator, typically
within an instance, where the operator may be a defaulted formal subprogram.

The following must compile quietly
   gcc -c libm.adb
   gcc -c -gnata libm.adb

---
package Libm is
   pragma Pure;

   procedure Req_Body;
end Libm;
---
with Libm.Aux; use Libm.Aux;
package body Libm is

   function Exact (X : Float) return Float is (X);

   package Float_Approximations is new Generic_Float_Approximations (Float);
   use Float_Approximations;

   procedure Req_Body is null;

end Libm;
--
package body Libm.Aux is
   use Ada.Numerics;

   generic
      type T is private;
      with function Multiply_Add (X, Y, Z : T) return T is <>;
   package Generic_Polynomials is

      type Polynomial is array (Positive range <>) of T;

      function Compute_Horner
        (P      : Polynomial;
         X      : T)
         return T with Inline;
   end Generic_Polynomials;

   package body Generic_Polynomials is

      function Compute_Horner
        (P      : Polynomial;
         X      : T)
         return T
      is
         Result : T := P (P'Last);

      begin
         for P_j of reverse P (P'First .. P'Last - 1) loop
            Result := Multiply_Add (Result, X, P_j);
         end loop;

         return Result;
      end Compute_Horner;
   end Generic_Polynomials;

   function Multiply_Add (X, Y, Z : Float) return Float is (X * Y + Z);

   package Float_Polynomials is new Generic_Polynomials (Float);
   use Float_Polynomials;

   package body Generic_Float_Approximations is

      function Multiply_Add (X, Y, Z : T) return T is (X * Y + Z);

      package Float_Polynomials is new Generic_Polynomials (T);
      use Float_Polynomials;

      function Approx_Sin  (X : T) return T is
         --  Hart's constants: #SIN 3040# (p. 199)

         P1 : constant T := Exact (-0.16666_66567);
         P2 : constant T := Exact (0.83320_15015E-2);
         P3 : constant T := Exact (-0.19501_81031E-3);

         Result : T;
         G  : constant T := X * X;
      begin
         Result := Compute_Horner ((P1, P2, P3), G);
         return Multiply_Add (X, Result * G, X);
      end Approx_Sin;

   end Generic_Float_Approximations;

end Libm.Aux;
---
with Ada.Numerics;
package Libm.Aux is
   pragma Pure;

   generic
      type T is private;
      with function "+" (X, Y : T) return T is <>;
      with function "*" (X, Y : T) return T is <>;
      with function "+" (X : T) return T is <>;
      with function "<=" (X, Y : T) return Boolean is <>;
      with function "abs" (X : T) return T is <>;
      with function Exact (X : Float) return T is <>;
   package Generic_Float_Approximations is
      --  The approximations in this package will work well for single
      --  precision floating point types.

      function Approx_Sin  (X : T) return T
        with
             Pre  => (abs X) <= Exact (Ada.Numerics.Pi / 2.0),
             Post => (abs Approx_Sin'Result) <= Exact (1.0);

   end Generic_Float_Approximations;

end Libm.Aux;

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

2014-01-21  Ed Schonberg  <schonberg@adacore.com>

	* sem_res.adb (Rewrite_Renamed_Operator): Do not replace entity
	with the operator it renames if we are within an expression of
	a pre/postcondition, because the expression will be reanalyzed
	at a later point, and the analysis of the renaming may affect
	the visibility of the operator when in an instance.

Attachment: difs
Description: Text document