Several static evaluation routines use Determine_Range to establish the bounds
of a non-static expression. If overflow cheks are enabled, the range of the
result of unary and binary operations may raise an exception, and cannot be
assumed to evaluate correctly without a run-time check. This patch prevents
unwarranted optimizations on boolean expressions appearing in preconditions
and other contexts.
The following must execute quietly;
gcc -c -gnato -gnatDG -gnatc add.ads
grep true gnat.ads.dg
---
package Add is
function AddTwo (X, Y : Integer) return Integer;
Pragma Precondition (X + Y <= Integer'Last);
Pragma Postcondition (AddTwo'Result = X + Y);
end Add;
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-08-03 Ed Schonberg <schonb...@adacore.com>
* checks.adb (Determine_Range): If a computed bound of an operation is
outside the range of the base type of the expression, and overflow
checks are enabled, the result is unknown and cannot be used for any
subsequent constant folding.
* sem_eval.adb (Compile_Time_Compare): if the bounds of one operand are
unknown, so is the result of the comparison.
Index: checks.adb
===================================================================
--- checks.adb (revision 177274)
+++ checks.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
@@ -3457,6 +3457,18 @@
-- the computed expression is in the range Lor .. Hir. We can use this
-- to restrict the possible range of results.
+ -- If one of the computed bounds is outside the range of the base type,
+ -- the expression may raise an exception and we better indicate that
+ -- the evaluation has failed, at least if checks are enabled.
+
+ if Enable_Overflow_Checks
+ and then not Is_Entity_Name (N)
+ and then (Lor < Lo or else Hir > Hi)
+ then
+ OK := False;
+ return;
+ end if;
+
if OK1 then
-- If the refined value of the low bound is greater than the type
Index: sem_eval.adb
===================================================================
--- sem_eval.adb (revision 177274)
+++ sem_eval.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
@@ -964,6 +964,12 @@
return Unknown;
end if;
end if;
+ else
+
+ -- If the range of either operand cannot be determined,
+ -- nothing further can be inferred.
+
+ return Unknown;
end if;
end;
