diff mbox

[Ada] Fix some missing cases of floating-point validity checks

Message ID 20140124143553.GA30810@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Jan. 24, 2014, 2:35 p.m. UTC
When a program is compiled with -gnatVaf, all floating-point results
of operators must be checked, since they might yield infinite or NaN
results. Some cases of required checks, notably the result of object
declarations with initialization expressions were not being checked.

The following program, compiled with -gnatVaf

     1. with Ada.Text_IO; use Ada.Text_IO;
     2.
     3. procedure Float_Div_Inf is
     4.    function Id (X : Float) return Float is (X);
     5.
     6.    A : Float := Id (1.0);
     7.    B : Float := Id (0.0);
     8.    C : Float := A / B;
     9. begin
    10.    Put_Line (C'Img);
    11.    C := B / B;
    12.    Put_Line (C'Img);
    13. end Float_Div_Inf;

must yield the output:

raised CONSTRAINT_ERROR : float_div_inf.adb:8 invalid data

Previously the check on line 8 was missing, line 10 printed out
+Inf, and then there was a validity check failure on line 11.

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

2014-01-24  Robert Dewar  <dewar@adacore.com>

	* checks.adb (Expr_Known_Valid): Result of fpt operator never
	considered valid.
diff mbox

Patch

Index: checks.adb
===================================================================
--- checks.adb	(revision 207026)
+++ checks.adb	(working copy)
@@ -5308,23 +5308,27 @@ 
       elsif Nkind_In (Expr, N_Type_Conversion, N_Qualified_Expression) then
          return Expr_Known_Valid (Expression (Expr));
 
-      --  The result of any operator is always considered valid, since we
-      --  assume the necessary checks are done by the operator. For operators
-      --  on floating-point operations, we must also check when the operation
-      --  is the right-hand side of an assignment, or is an actual in a call.
+      --  Case of expression is a non-floating-point operator. In this case we
+      --  can assume the result is valid the generated code for the operator
+      --  will include whatever checks are needed (e.g. range checks) to ensure
+      --  validity. This assumption does not hold for the floating-point case,
+      --  since floating-point operators can generate Infinite or NaN results
+      --  which are considered invalid.
 
-      elsif Nkind (Expr) in N_Op then
-         if Is_Floating_Point_Type (Typ)
-            and then Validity_Check_Floating_Point
-            and then (Nkind_In (Parent (Expr), N_Assignment_Statement,
-                                               N_Function_Call,
-                                               N_Parameter_Association))
-         then
-            return False;
-         else
-            return True;
-         end if;
+      --  Historical note: in older versions, the exemption of floating-point
+      --  types from this assumption was done only in cases where the parent
+      --  was an assignment, function call or parameter association. Presumably
+      --  the idea was that in other contexts, the result would be checked
+      --  elsewhere, but this list of cases was missing tests (at least the
+      --  N_Object_Declaration case, as shown by a reported missing validity
+      --  check), and it is not clear why function calls but not procedure
+      --  calls were tested for. It really seems more accurate and much
+      --  safer to recognize that expressions which are the result of a
+      --  floating-point operator can never be assumed to be valid.
 
+      elsif Nkind (Expr) in N_Op and then not Is_Floating_Point_Type (Typ) then
+         return True;
+
       --  The result of a membership test is always valid, since it is true or
       --  false, there are no other possibilities.