aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/sem_res.adb
diff options
context:
space:
mode:
authorArnaud Charlet <charlet@gcc.gnu.org>2014-10-10 15:57:55 +0200
committerArnaud Charlet <charlet@gcc.gnu.org>2014-10-10 15:57:55 +0200
commit79904ebc48b0103c5a11dcfb76ee7c37399a213a (patch)
tree7195986a7034a9f4a49452941e16b32f41232bcf /gcc/ada/sem_res.adb
parent06a04ce75ab48a0a1b539b2140cd22a746f4c030 (diff)
downloadgcc-79904ebc48b0103c5a11dcfb76ee7c37399a213a.zip
gcc-79904ebc48b0103c5a11dcfb76ee7c37399a213a.tar.gz
gcc-79904ebc48b0103c5a11dcfb76ee7c37399a213a.tar.bz2
[multiple changes]
2014-10-10 Gary Dismukes <dismukes@adacore.com> * a-coinho-shared.adb: Minor typo fix. * prj-env.ads: Minor reformatting. 2014-10-10 Hristian Kirtchev <kirtchev@adacore.com> * sem_res.adb (Resolve_String_Literal): Do not generate a string literal subtype for the default expression of a formal parameter in GNATprove mode. 2014-10-10 Yannick Moy <moy@adacore.com> * errout.adb (SPARK_Msg_N): Issue error unless SPARK_Mode is Off. 2014-10-10 Ed Schonberg <schonberg@adacore.com> * exp_ch5.adb (Expand_Formal_Container_Element_Loop): Analyze declaration for loop parameter before rest of loop, and set entity kind to prevent assignments to it in the user code. * sem_ch3.adb (Analyze_Object_Contract): No contracts apply to the loop parameter in an element iteration over o formal container. 2014-10-10 Robert Dewar <dewar@adacore.com> * gnat_ugn.texi: Document use of user-level routines to handle e.g. col major arrays. 2014-10-10 Doug Rupp <rupp@adacore.com> * s-osinte-android.adb: Fix misspelling. * gsocket.h: Tweak the Android quirks. 2014-10-10 Robert Dewar <dewar@adacore.com> * errout.ads (SPARK_Msg_N): Fix spec to match change in body. From-SVN: r216083
Diffstat (limited to 'gcc/ada/sem_res.adb')
-rw-r--r--gcc/ada/sem_res.adb11
1 files changed, 11 insertions, 0 deletions
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index b35ffbd..eacb977 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -9947,6 +9947,17 @@ package body Sem_Res is
then
Subtype_Id := Typ;
+ -- Do not generate a string literal subtype for the default expression
+ -- of a formal parameter in GNATprove mode. This is because the string
+ -- subtype is associated with the freezing actions of the subprogram,
+ -- however freezing is disabled in GNATprove mode and as a result the
+ -- subtype is unavailable.
+
+ elsif GNATprove_Mode
+ and then Nkind (Parent (N)) = N_Parameter_Specification
+ then
+ Subtype_Id := Typ;
+
-- Otherwise we must create a string literal subtype. Note that the
-- whole idea of string literal subtypes is simply to avoid the need
-- for building a full fledged array subtype for each literal.