This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.

Index Nav:	[Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav:	[Date Prev] [Date Next]	[Thread Prev] [Thread Next]
Other format:	[Raw text]

[Ada] Make sure that range check flag is set on real-integer conversions

From: Arnaud Charlet <charlet at adacore dot com>
To: gcc-patches at gcc dot gnu dot org
Cc: Robert Dewar <dewar at adacore dot com>
Date: Mon, 4 Aug 2014 04:08:09 -0400
Subject: [Ada] Make sure that range check flag is set on real-integer conversions
Authentication-results: sourceware.org; auth=none

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: difs
Description: Text document

Index Nav:	[Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav:	[Date Prev] [Date Next]	[Thread Prev] [Thread Next]