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

login
register
mail settings
Submitter Arnaud Charlet
Date April 24, 2013, 2:33 p.m.
Message ID <20130424143335.GA21275@adacore.com>
Download mbox | patch
Permalink /patch/239215/
State New
Headers show

Comments

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

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