+2015-03-13 Claire Dross <dross@adacore.com>
+
+ * 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 <schonberg@adacore.com>
+
+ * 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 <dewar@adacore.com>
+
+ * 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.
+
2015-03-13 Gary Dismukes <dismukes@adacore.com>
* style.adb (Missing_Overriding): Apply the
-- --
-- B o d y --
-- --
--- Copyright (C) 2010-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 2010-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
Aspect_Thread_Local_Storage => Aspect_Thread_Local_Storage,
Aspect_Type_Invariant => Aspect_Invariant,
Aspect_Unchecked_Union => Aspect_Unchecked_Union,
+ Aspect_Unimplemented => Aspect_Unimplemented,
Aspect_Universal_Aliasing => Aspect_Universal_Aliasing,
Aspect_Universal_Data => Aspect_Universal_Data,
Aspect_Unmodified => Aspect_Unmodified,
-- --
-- S p e c --
-- --
--- Copyright (C) 2010-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 2010-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
Aspect_Synchronization,
Aspect_Test_Case, -- GNAT
Aspect_Type_Invariant,
+ Aspect_Unimplemented, -- GNAT
Aspect_Unsuppress,
Aspect_Value_Size, -- GNAT
Aspect_Variable_Indexing,
Aspect_Synchronization => Name,
Aspect_Test_Case => Expression,
Aspect_Type_Invariant => Expression,
+ Aspect_Unimplemented => Optional_Expression,
Aspect_Unsuppress => Name,
Aspect_Value_Size => Expression,
Aspect_Variable_Indexing => Name,
Aspect_Test_Case => Name_Test_Case,
Aspect_Type_Invariant => Name_Type_Invariant,
Aspect_Unchecked_Union => Name_Unchecked_Union,
+ Aspect_Unimplemented => Name_Unimplemented,
Aspect_Universal_Aliasing => Name_Universal_Aliasing,
Aspect_Universal_Data => Name_Universal_Data,
Aspect_Unmodified => Name_Unmodified,
Aspect_SPARK_Mode => Never_Delay,
Aspect_Synchronization => Never_Delay,
Aspect_Test_Case => Never_Delay,
+ Aspect_Unimplemented => Never_Delay,
Aspect_Warnings => Never_Delay,
Aspect_Alignment => Rep_Aspect,
-- Is_Static_Type Flag281
-- Has_Nested_Subprogram Flag282
-- Uplevel_Reference_Noted Flag283
+ -- Is_Unimplemented Flag284
- -- (unused) Flag284
-- (unused) Flag285
-- (unused) Flag286
-- (unused) Flag287
return Flag246 (Id);
end Is_Underlying_Record_View;
+ function Is_Unimplemented (Id : E) return B is
+ begin
+ return Flag284 (Id);
+ end Is_Unimplemented;
+
function Is_Unsigned_Type (Id : E) return B is
begin
pragma Assert (Is_Type (Id));
Set_Flag246 (Id, V);
end Set_Is_Underlying_Record_View;
+ procedure Set_Is_Unimplemented (Id : E; V : B := True) is
+ begin
+ Set_Flag284 (Id, V);
+ end Set_Is_Unimplemented;
+
procedure Set_Is_Unsigned_Type (Id : E; V : B := True) is
begin
pragma Assert (Is_Discrete_Or_Fixed_Point_Type (Id));
W ("Is_True_Constant", Flag163 (Id));
W ("Is_Unchecked_Union", Flag117 (Id));
W ("Is_Underlying_Record_View", Flag246 (Id));
+ W ("Is_Unimplemented", Flag284 (Id));
W ("Is_Unsigned_Type", Flag144 (Id));
W ("Is_Valued_Procedure", Flag127 (Id));
W ("Is_Visible_Formal", Flag206 (Id));
-- including generic formal parameters.
-- Is_Obsolescent (Flag153)
--- Defined in all entities. Set for any entity for which a valid pragma
--- Obsolescent applies.
+-- Defined in all entities. Set for any entity to which a valid pragma
+-- or aspect Obsolescent applies.
-- Is_Only_Out_Parameter (Flag226)
-- Defined in formal parameter entities. Set if this parameter is the
-- as its corresponding record type, but whose parent is the full view
-- of the parent in the original type extension.
+-- Is_Unimplemented (Flag284)
+-- Defined in all entities. Set for any entity to which a valid pragma
+-- or aspect Unimplemented applies.
+
-- Is_Unsigned_Type (Flag144)
-- Defined in all types, but can be set only for discrete and fixed-point
-- type and subtype entities. This flag is only valid if the entity is
-- Is_Thunk (Flag225)
-- Is_Trivial_Subprogram (Flag235)
-- Is_Unchecked_Union (Flag117)
+ -- Is_Unimplemented (Flag284)
-- Is_Visible_Formal (Flag206)
-- Kill_Elaboration_Checks (Flag32)
-- Kill_Range_Checks (Flag33)
-- SPARK_Pragma (Node32)
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
+ -- Import_Pragma (Node35) (non-generic case only)
-- Body_Needed_For_SAL (Flag40)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Default_Expressions_Processed (Flag108)
-- Subprograms_For_Type (Node29)
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
+ -- Import_Pragma (Node35)
-- Has_Invariants (Flag232)
-- Is_Machine_Code_Subprogram (Flag137)
-- Is_Pure (Flag44)
-- SPARK_Pragma (Node32)
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
+ -- Import_Pragma (Node35) (non-generic case only)
-- Body_Needed_For_SAL (Flag40)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Delay_Cleanups (Flag114)
function Is_True_Constant (Id : E) return B;
function Is_Unchecked_Union (Id : E) return B;
function Is_Underlying_Record_View (Id : E) return B;
+ function Is_Unimplemented (Id : E) return B;
function Is_Unsigned_Type (Id : E) return B;
function Is_Valued_Procedure (Id : E) return B;
function Is_Visible_Formal (Id : E) return B;
procedure Set_Is_True_Constant (Id : E; V : B := True);
procedure Set_Is_Unchecked_Union (Id : E; V : B := True);
procedure Set_Is_Underlying_Record_View (Id : E; V : B := True);
+ procedure Set_Is_Unimplemented (Id : E; V : B := True);
procedure Set_Is_Unsigned_Type (Id : E; V : B := True);
procedure Set_Is_Valued_Procedure (Id : E; V : B := True);
procedure Set_Is_Visible_Formal (Id : E; V : B := True);
pragma Inline (Is_Type);
pragma Inline (Is_Unchecked_Union);
pragma Inline (Is_Underlying_Record_View);
+ pragma Inline (Is_Unimplemented);
pragma Inline (Is_Unsigned_Type);
pragma Inline (Is_Valued_Procedure);
pragma Inline (Is_Visible_Formal);
pragma Inline (Set_Is_True_Constant);
pragma Inline (Set_Is_Unchecked_Union);
pragma Inline (Set_Is_Underlying_Record_View);
+ pragma Inline (Set_Is_Unimplemented);
pragma Inline (Set_Is_Unsigned_Type);
pragma Inline (Set_Is_Valued_Procedure);
pragma Inline (Set_Is_Visible_Formal);
(Spec_Id : Entity_Id;
Body_Id : Entity_Id) return Boolean
is
+ function Has_Parameter_With_Discriminant_Dependent_Fields
+ (Id : Entity_Id) return Boolean;
+ -- Returns true if the subprogram as parameters of an unconstrained
+ -- record types with fields whose types depend on a discriminant.
+
function Has_Some_Contract (Id : Entity_Id) return Boolean;
-- Returns True if subprogram Id has any contract (Pre, Post, Global,
-- Depends, etc.)
-- Returns True if subprogram Id was defined originally as an expression
-- function.
+ ------------------------------------------------------
+ -- Has_Parameter_With_Discriminant_Dependent_Fields --
+ ------------------------------------------------------
+
+ function Has_Parameter_With_Discriminant_Dependent_Fields
+ (Id : Entity_Id) return Boolean
+ is
+ E : Entity_Id := Id;
+ Spec : Node_Id := Parent (E);
+
+ begin
+ -- Get the specification of the subprogram. Go through alias if
+ -- needed.
+
+ if Nkind (Spec) = N_Defining_Program_Unit_Name then
+ Spec := Parent (Spec);
+ end if;
+
+ while Nkind (Spec) not in N_Subprogram_Specification loop
+ pragma Assert (Present (Alias (E)));
+ E := Alias (E);
+ Spec := Parent (E);
+
+ if Nkind (Spec) = N_Defining_Program_Unit_Name then
+ Spec := Parent (Spec);
+ end if;
+ end loop;
+
+ declare
+ Params : constant List_Id := Parameter_Specifications (Spec);
+ Param : Node_Id;
+ Param_Ty : Entity_Id;
+
+ begin
+ if Is_Non_Empty_List (Params) then
+ Param := First (Params);
+ while Present (Param) loop
+ Param_Ty := Etype (Defining_Identifier (Param));
+
+ -- If the parameter is an unconstrained record, check if
+ -- it has components whose types depend on a discriminant.
+
+ if Is_Record_Type (Param_Ty)
+ and then not Is_Constrained (Param_Ty)
+ then
+ declare
+ Comp : Node_Id := First_Component (Param_Ty);
+
+ begin
+ while Present (Comp) loop
+ if Has_Discriminant_Dependent_Constraint (Comp) then
+ return True;
+ end if;
+
+ Comp := Next_Component (Comp);
+ end loop;
+ end;
+ end if;
+
+ Param := Next (Param);
+ end loop;
+ end if;
+ end;
+
+ return False;
+ end Has_Parameter_With_Discriminant_Dependent_Fields;
+
-----------------------
-- Has_Some_Contract --
-----------------------
elsif Instantiation_Location (Sloc (Id)) /= No_Location then
return False;
- -- Don't inline predicate functions (treated specially by GNATprove)
+ -- Do not inline predicate functions (treated specially by GNATprove)
elsif Is_Predicate_Function (Id) then
return False;
+ -- Do not inline subprograms with a parameter of an unconstrained
+ -- record type if it has discrimiant dependent fields. Indeed, with
+ -- such parameters, the frontend cannot always ensure type compliance
+ -- in record component accesses (in particular with records containing
+ -- packed arrays).
+
+ elsif Has_Parameter_With_Discriminant_Dependent_Fields (Id) then
+ return False;
+
-- Otherwise, this is a subprogram declared inside the private part of a
-- package, or inside a package body, or locally in a subprogram, and it
-- does not have any contract. Inline it.
end;
end if;
+ -- 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.
+
+ if Is_Floating_Point_Type (Act_T) then
+ Copy_Dimensions (Act_T, Subt);
+ end if;
+
return Decl_Nodes;
end Instantiate_Type;
-- Processing based on specific aspect
case A_Id is
+ when Aspect_Unimplemented =>
+ null; -- ??? temp for now
-- No_Aspect should be impossible
Aspect_Refined_Post |
Aspect_Refined_State |
Aspect_SPARK_Mode |
- Aspect_Test_Case =>
+ Aspect_Test_Case |
+ Aspect_Unimplemented =>
raise Program_Error;
end case;
if Present (Ref_Global) then
Analyze_Refined_Global_In_Decl_Part (Ref_Global);
-
- -- When the corresponding Global pragma references a state with
- -- visible refinement, the body requires Refined_Global. Such a
- -- refinement is not required when SPARK checks are suppressed.
-
- else
- Prag := Get_Pragma (Spec_Id, Pragma_Global);
-
- if SPARK_Mode /= Off
- and then Present (Prag)
- and then Contains_Refined_State (Prag)
- then
- Error_Msg_NE
- ("body of subprogram& requires global refinement",
- Body_Decl, Spec_Id);
- end if;
end if;
-- Refined_Depends must be analyzed after Refined_Global in order to
if Present (Ref_Depends) then
Analyze_Refined_Depends_In_Decl_Part (Ref_Depends);
-
- -- When the corresponding Depends pragma references a state with
- -- visible refinement, the body requires Refined_Depends. Such a
- -- refinement is not required when SPARK checks are suppressed.
-
- else
- Prag := Get_Pragma (Spec_Id, Pragma_Depends);
-
- if SPARK_Mode /= Off
- and then Present (Prag)
- and then Contains_Refined_State (Prag)
- then
- Error_Msg_NE
- ("body of subprogram& requires dependance refinement",
- Body_Decl, Spec_Id);
- end if;
end if;
end Analyze_Completion_Contract;
-- --
-- B o d y --
-- --
--- Copyright (C) 2011-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 2011-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
with Atree; use Atree;
with Einfo; use Einfo;
with Errout; use Errout;
+with Exp_Util; use Exp_Util;
with Lib; use Lib;
with Namet; use Namet;
with Nlists; use Nlists;
begin
-- Aspect is an Ada 2012 feature. Note that there is no need to check
- -- dimensions for aggregates that don't come from source.
+ -- dimensions for aggregates that don't come from source, or if we are
+ -- within an initialization procedure, whose expressions have been
+ -- checked at the point of record declaration.
- if Ada_Version < Ada_2012 or else not Comes_From_Source (N) then
+ if Ada_Version < Ada_2012
+ or else not Comes_From_Source (N)
+ or else Inside_Init_Proc
+ then
return;
end if;
-- 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 --
-----------------------
Name_Dynamic_Predicate : constant Name_Id := N + $;
Name_Static_Predicate : constant Name_Id := N + $;
Name_Synchronization : constant Name_Id := N + $;
+ Name_Unimplemented : constant Name_Id := N + $;
-- Some special names used by the expander. Note that the lower case u's
-- at the start of these names get translated to extra underscores. These
projects / platform / upstream / linaro-gcc.git / commitdiff