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 <schonb...@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.
Index: sem_res.adb =================================================================== --- sem_res.adb (revision 206844) +++ sem_res.adb (working copy) @@ -10301,6 +10301,14 @@ Op_Node : Node_Id; begin + -- Do not perform this transformation within a pre/postcondition, + -- because the expression will be re-analyzed, and the transformation + -- might affect the visibility of the operator, e.g. in an instance. + + if In_Assertion_Expr > 0 then + return; + end if; + -- Rewrite the operator node using the real operator, not its renaming. -- Exclude user-defined intrinsic operations of the same name, which are -- treated separately and rewritten as calls.