From d3ef4bd61fdcc491c39249dd256c3733f45219b9 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 13 Mar 2015 14:28:15 +0100 Subject: [multiple changes] 2015-03-13 Claire Dross * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Do not inline subprograms with unconstrained record parameters containing Itype declarations. * sinfo.ads Document GNATprove assumption that type should match in the AST. * sem_ch6.adb (Analyze_Subprogram_Body_Contract): Do not check for Refined_Depends and Refined_Globals contracts as they are optional. 2015-03-13 Ed Schonberg * sem_ch12.adb (Instantiate_Type): For a floating-point type, capture dimension info if any, because the generated subtype declaration does not come from source and will not process dimensions. * sem_dim,adb (Analyze_Dimension_Extension_Or_Record_Aggregate): Do not analyze expressions with an initialization procedure because aggregates will have been checked at the point of record declaration. 2015-03-13 Robert Dewar * aspects.ads, aspects.adb: Add entries for aspect Unimplemented. * einfo.ads, einfo.adb (Is_Unimplemented): New flag. * sem_ch13.adb: Add dummy entry for aspect Unimplemented. * snames.ads-tmpl: Add entry for Name_Unimplemented. From-SVN: r221420 --- gcc/ada/sinfo.ads | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'gcc/ada/sinfo.ads') diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 3dc9311..5f057f2 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -617,6 +617,17 @@ package Sinfo is -- checks on empty ranges, which typically appear in deactivated -- code in a particular configuration). + -- 6. Subtypes should match in the AST, even after a generic is + -- instantiated. In particular, GNATprove relies on the fact that, + -- on a selected component, the type of the selected component is + -- the type of the corresponding component in the prefix of the + -- selected component. + -- + -- Note that, in some cases, we know that this rule is broken by the + -- frontend. In particular, if the selected component is a packed + -- array depending on a discriminant of a unconstrained formal object + -- parameter of a generic. + ----------------------- -- Check Flag Fields -- ----------------------- -- cgit v1.1