[Ada] Do not apply float conversion checks if expansion not enabled

Submitted by Arnaud Charlet on April 24, 2013, 2:33 p.m.

Details

Message ID 20130424143335.GA21275@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet April 24, 2013, 2:33 p.m.
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  <moy@adacore.com>

	* checks.adb (Apply_Float_Conversion_Check): Do not apply checks if
	full expansion is not enabled.

Patch hide | download patch | download mbox

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