We do not need checks if we are not generating code, and in SPARK mode, we
specifically don't want the frontend to expand these checks, which are dealt
with directly in the formal verification backend. This is similar to what is
already done for other checks.
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-04-24 Yannick Moy <m...@adacore.com>
* checks.adb (Apply_Float_Conversion_Check): Do not apply checks if
full expansion is not enabled.
Index: checks.adb
===================================================================
--- checks.adb (revision 198226)
+++ checks.adb (working copy)
@@ -1907,6 +1907,15 @@
Reason : RT_Exception_Code;
begin
+ -- We do not need checks if we are not generating code (i.e. the full
+ -- expander is not active). In SPARK mode, we specifically don't want
+ -- the frontend to expand these checks, which are dealt with directly
+ -- in the formal verification backend.
+
+ if not Full_Expander_Active then
+ return;
+ end if;
+
if not Compile_Time_Known_Value (LB)
or not Compile_Time_Known_Value (HB)
then
