public inbox for gcc-patches@gcc.gnu.org
 help / color / mirror / Atom feed
* [Ada] Make sure that range check flag is set on real-integer conversions
@ 2014-08-04  8:08 Arnaud Charlet
  0 siblings, 0 replies; only message in thread
From: Arnaud Charlet @ 2014-08-04  8:08 UTC (permalink / raw)
  To: gcc-patches; +Cc: Robert Dewar

[-- Attachment #1: Type: text/plain, Size: 586 bytes --]

This change makes sure that the Do_Range_Check flag is set in -gnatc or
GNATprove mode for type conversions from real to integer. This makes sure
that SPARK2014 programs properly verify that such conversions cannot raise
an exception due to an out of range value. The following test compiled
with -gnatdt generates a tree that has one instance of Do_Range_Check
being set.

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

2014-08-04  Robert Dewar  <dewar@adacore.com>

	* sem_res.adb (Resolve_Type_Conversion): Set Do_Range_Check on
	conversion from a real type to an integer type.


[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 1399 bytes --]

Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 213537)
+++ sem_res.adb	(working copy)
@@ -10322,11 +10322,11 @@
          --  odd subtype coming from the bounds).
 
          if (Is_Entity_Name (Orig_N)
-               and then
-                 (Etype (Entity (Orig_N)) = Orig_T
-                   or else
-                     (Ekind (Entity (Orig_N)) = E_Loop_Parameter
-                       and then Covers (Orig_T, Etype (Entity (Orig_N))))))
+              and then
+                (Etype (Entity (Orig_N)) = Orig_T
+                  or else
+                    (Ekind (Entity (Orig_N)) = E_Loop_Parameter
+                      and then Covers (Orig_T, Etype (Entity (Orig_N))))))
 
            --  If not an entity, then type of expression must match
 
@@ -10504,6 +10504,17 @@
             Apply_Predicate_Check (N, Target_Typ);
          end if;
       end if;
+
+      --  If at this stage we have a real to integer conversion, make sure
+      --  that the Do_Range_Check flag is set, because such conversions in
+      --  general need a range check.
+
+      if Nkind (N) = N_Type_Conversion
+        and then Is_Integer_Type (Target_Typ)
+        and then Is_Real_Type (Operand_Typ)
+      then
+         Set_Do_Range_Check (Operand);
+      end if;
    end Resolve_Type_Conversion;
 
    ----------------------

^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2014-08-04  8:08 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2014-08-04  8:08 [Ada] Make sure that range check flag is set on real-integer conversions Arnaud Charlet

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).