+2017-04-27 Ed Schonberg <schonberg@adacore.com>
+
+ * freeze.adb (Build_Inherited_Condition_Pragmas): New procedure,
+ subsidiary of Check_Inherited_Conditions, to build pragmas for an
+ operation whose ancestor has classwide pre/postconditions. This
+ is used both to check the legality of the inheritance in Ada
+ and in SPARK, and to determine whether a wrapper is needed for
+ an inherited operation.
+ * exp_util.adb (Build_Class_Wide_Expression, Replace_Entity):
+ Improve placement of error message for inherited classwide
+ conditions that become illegal on type derivation.
+
+2017-04-27 Yannick Moy <moy@adacore.com>
+
+ * sem_ch12.adb (Analyze_Generic_Package_Declaration): Set
+ SPARK_Mode from context on generic package.
+ * sem_ch7.adb (Analyze_Package_Declaration): Simplify code to remove
+ useless test.
+
+2017-04-27 Claire Dross <dross@adacore.com>
+
+ * a-cofuve.ads (Range_Shifted): Rewrite precondition to avoid
+ overflows in computations.
+ * a-cofove.ads (Capacity_Range): Rewrite last bound to avoid
+ overflows in computations.
+ (Insert): Rewrite precondition to avoid overflows in computations.
+ * a-cfinve.ads (Capacity_Range): Rewrite last bound to avoid
+ overflows in computations.
+ (Insert): Rewrite precondition to avoid overflows in computations.
+
2017-04-27 Steve Baird <baird@adacore.com>
* exp_ch9.adb (Expand_N_Asynchronous_Select): Initialize the Cancel
No_Index : constant Extended_Index := Extended_Index'First;
- subtype Capacity_Range is
- Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
+ Last_Count : constant Count_Type :=
+ (if Index_Type'Last < Index_Type'First then 0
+ elsif Index_Type'Last < -1
+ or else Index_Type'Pos (Index_Type'First) >
+ Index_Type'Pos (Index_Type'Last) - Count_Type'Last
+ then Index_Type'Pos (Index_Type'Last) -
+ Index_Type'Pos (Index_Type'First) + 1
+ else Count_Type'Last);
+ -- Maximal capacity of any vector. It is the minimum of the size of the
+ -- index range and the last possible Count_Type.
+
+ subtype Capacity_Range is Count_Type range 0 .. Last_Count;
type Vector (Capacity : Capacity_Range) is limited private with
Default_Initial_Condition => Is_Empty (Vector);
Pre =>
Length (Container) <= Capacity (Container) - Length (New_Item)
and (Before in Index_Type'First .. Last_Index (Container)
- or Before - 1 = Last_Index (Container)),
+ or (Before /= No_Index
+ and then Before - 1 = Last_Index (Container))),
Post =>
Length (Container) = Length (Container)'Old + Length (New_Item)
Pre =>
Length (Container) <= Capacity (Container) - Count
and (Before in Index_Type'First .. Last_Index (Container)
- or Before - 1 = Last_Index (Container)),
+ or (Before /= No_Index
+ and then Before - 1 = Last_Index (Container))),
Post =>
Length (Container) = Length (Container)'Old + Count
No_Index : constant Extended_Index := Extended_Index'First;
- subtype Capacity_Range is
- Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
+ Last_Count : constant Count_Type :=
+ (if Index_Type'Last < Index_Type'First then 0
+ elsif Index_Type'Last < -1
+ or else Index_Type'Pos (Index_Type'First) >
+ Index_Type'Pos (Index_Type'Last) - Count_Type'Last
+ then Index_Type'Pos (Index_Type'Last) -
+ Index_Type'Pos (Index_Type'First) + 1
+ else Count_Type'Last);
+ -- Maximal capacity of any vector. It is the minimum of the size of the
+ -- index range and the last possible Count_Type.
+
+ subtype Capacity_Range is Count_Type range 0 .. Last_Count;
type Vector (Capacity : Capacity_Range) is limited private with
Default_Initial_Condition => Is_Empty (Vector);
Pre =>
Length (Container) <= Capacity (Container) - Length (New_Item)
and (Before in Index_Type'First .. Last_Index (Container)
- or Before - 1 = Last_Index (Container)),
+ or (Before /= No_Index
+ and then Before - 1 = Last_Index (Container))),
Post =>
Length (Container) = Length (Container)'Old + Length (New_Item)
Pre =>
Length (Container) <= Capacity (Container) - Count
and (Before in Index_Type'First .. Last_Index (Container)
- or Before - 1 = Last_Index (Container)),
+ or (Before /= No_Index
+ and then Before - 1 = Last_Index (Container))),
Post =>
Length (Container) = Length (Container)'Old + Count
Global => null,
Pre =>
Lst <= Last (Left)
- and Offset in
- Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) ..
- (Index_Type'Pos (Index_Type'First) - 1) + Length (Right) -
- Index_Type'Pos (Lst),
+ and then
+ (if Offset < 0 then
+ Index_Type'Pos (Index_Type'Base'First) - Offset <=
+ Index_Type'Pos (Index_Type'First))
+ and then
+ (if Fst <= Lst then
+ Offset in
+ Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) ..
+ (Index_Type'Pos (Index_Type'First) - 1) + Length (Right) -
+ Index_Type'Pos (Lst)),
Post =>
Range_Shifted'Result =
((for all I in Fst .. Lst =>
and then Is_Abstract_Subprogram (Entity (N))
then
Error_Msg_Sloc := Sloc (Current_Scope);
- Error_Msg_NE
- ("cannot call abstract subprogram in inherited condition "
- & "for&#", N, Current_Scope);
+ -- Error_Msg_Node_1 := Entity (N);
+ Error_Msg_Node_2 := Subp;
+ if Comes_From_Source (Subp) then
+ Error_Msg_NE
+ ("cannot call abstract subprogram& in inherited "
+ & "condition for&#", Subp, Entity (N));
+ else
+ Error_Msg_NE
+ ("cannot call abstract subprogram& in inherited "
+ & "condition for inherited&#", Subp, Entity (N));
+ end if;
-- In SPARK mode, reject an inherited condition for an
-- inherited operation if it contains a call to an overriding
procedure Check_Inherited_Conditions (R : Entity_Id) is
Prim_Ops : constant Elist_Id := Primitive_Operations (R);
- A_Post : Node_Id;
- A_Pre : Node_Id;
Decls : List_Id;
Needs_Wrapper : Boolean;
- New_Prag : Node_Id;
Op_Node : Elmt_Id;
Par_Prim : Entity_Id;
Prim : Entity_Id;
+ ---------------------------------------
+ -- Build_Inherited_Condition_Pragmas --
+ ---------------------------------------
+
+ procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id);
+ -- Build corresponding pragmas for an operation whose ancestor has
+ -- class-wide pre/postconditions. If the operation is inherited, the
+ -- pragmas force the creation of a wrapper for the inherited operation.
+ -- If the ancestor is being overridden, the pragmas are constructed only
+ -- to verify their legality, in case they contain calls to other
+ -- primitives that may haven been overridden.
+
+ procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id) is
+ A_Post : Node_Id;
+ A_Pre : Node_Id;
+ New_Prag : Node_Id;
+
+ begin
+ A_Pre := Get_Pragma (Par_Prim, Pragma_Precondition);
+ if Present (A_Pre) and then Class_Present (A_Pre) then
+ New_Prag := New_Copy_Tree (A_Pre);
+ Build_Class_Wide_Expression
+ (Prag => New_Prag,
+ Subp => Prim,
+ Par_Subp => Par_Prim,
+ Adjust_Sloc => False,
+ Needs_Wrapper => Needs_Wrapper);
+
+ if Needs_Wrapper
+ and then not Comes_From_Source (Subp)
+ and then Expander_Active
+ then
+ Append (New_Prag, Decls);
+ end if;
+ end if;
+
+ A_Post := Get_Pragma (Par_Prim, Pragma_Postcondition);
+
+ if Present (A_Post) and then Class_Present (A_Post) then
+ New_Prag := New_Copy_Tree (A_Post);
+ Build_Class_Wide_Expression
+ (Prag => New_Prag,
+ Subp => Prim,
+ Par_Subp => Par_Prim,
+ Adjust_Sloc => False,
+ Needs_Wrapper => Needs_Wrapper);
+
+ if Needs_Wrapper
+ and then not Comes_From_Source (Subp)
+ and then Expander_Active
+ then
+ Append (New_Prag, Decls);
+ end if;
+ end if;
+ end Build_Inherited_Condition_Pragmas;
+
begin
Op_Node := First_Elmt (Prim_Ops);
while Present (Op_Node) loop
- Prim := Node (Op_Node);
- Needs_Wrapper := False;
+ Prim := Node (Op_Node);
-- Map the overridden primitive to the overriding one. This takes
-- care of all overridings and is done only once.
if Present (Overridden_Operation (Prim))
and then Comes_From_Source (Prim)
then
- Update_Primitives_Mapping (Overridden_Operation (Prim), Prim);
+ Par_Prim := Overridden_Operation (Prim);
+ Update_Primitives_Mapping (Par_Prim, Prim);
+ end if;
+
+ Next_Elmt (Op_Node);
+ end loop;
+
+ -- Now perform validity checks on the inherited conditions of
+ -- overriding operations, for conformance with LSP, and apply
+ -- SPARK-specific restrictions on inherited conditions.
+
+ Op_Node := First_Elmt (Prim_Ops);
+ while Present (Op_Node) loop
+ Prim := Node (Op_Node);
+ if Present (Overridden_Operation (Prim))
+ and then Comes_From_Source (Prim)
+ then
+ Par_Prim := Overridden_Operation (Prim);
+
+ -- Analyze the contract items of the overridden operation, before
+ -- they are rewritten as pragmas.
+
+ Analyze_Entry_Or_Subprogram_Contract (Par_Prim);
-- In SPARK mode this is where we can collect the inherited
-- conditions, because we do not create the Check pragmas that
-- overriding operations.
if SPARK_Mode = On then
+ Collect_Inherited_Class_Wide_Conditions (Prim);
- -- Analyze the contract items of the parent operation, before
- -- they are rewritten when inherited.
-
- Analyze_Entry_Or_Subprogram_Contract
- (Overridden_Operation (Prim));
+ else
- -- Now verify the legality of inherited contracts for LSP
- -- conformance.
+ -- Build the corresponding pragmas to check for legality
+ -- of the inherited condition.
- Collect_Inherited_Class_Wide_Conditions (Prim);
+ Build_Inherited_Condition_Pragmas (Prim);
end if;
end if;
Next_Elmt (Op_Node);
end loop;
- -- In all cases, we examine inherited operations to check whether they
- -- require a wrapper to handle inherited conditions that call other
- -- primitives, so that LSP can be verified/enforced.
+ -- Now examine the inherited operations to check whether they require
+ -- a wrapper to handle inherited conditions that call other primitives,
+ -- so that LSP can be verified/enforced.
Op_Node := First_Elmt (Prim_Ops);
+ Needs_Wrapper := False;
+
while Present (Op_Node) loop
Decls := Empty_List;
Prim := Node (Op_Node);
if not Comes_From_Source (Prim) and then Present (Alias (Prim)) then
Par_Prim := Alias (Prim);
- -- Analyze the contract items of the parent operation, before
- -- they are rewritten when inherited.
+ -- Analyze the contract items of the parent operation, and
+ -- determine whether a wrapper is needed. This is determined
+ -- when the condition is rewritten in sem_prag, using the
+ -- mapping between overridden and overriding operations built
+ -- in the loop above.
Analyze_Entry_Or_Subprogram_Contract (Par_Prim);
-
- A_Pre := Get_Pragma (Par_Prim, Pragma_Precondition);
-
- if Present (A_Pre) and then Class_Present (A_Pre) then
- New_Prag := New_Copy_Tree (A_Pre);
- Build_Class_Wide_Expression
- (Prag => New_Prag,
- Subp => Prim,
- Par_Subp => Par_Prim,
- Adjust_Sloc => False,
- Needs_Wrapper => Needs_Wrapper);
-
- if Needs_Wrapper then
- Append (New_Prag, Decls);
- end if;
- end if;
-
- A_Post := Get_Pragma (Par_Prim, Pragma_Postcondition);
-
- if Present (A_Post) and then Class_Present (A_Post) then
- New_Prag := New_Copy_Tree (A_Post);
- Build_Class_Wide_Expression
- (Prag => New_Prag,
- Subp => Prim,
- Par_Subp => Par_Prim,
- Adjust_Sloc => False,
- Needs_Wrapper => Needs_Wrapper);
-
- if Needs_Wrapper then
- Append (New_Prag, Decls);
- end if;
- end if;
+ Build_Inherited_Condition_Pragmas (Prim);
end if;
- if Needs_Wrapper and then not Is_Abstract_Subprogram (Par_Prim) then
+ if Needs_Wrapper and then not Is_Abstract_Subprogram (Par_Prim)
+ and then Expander_Active
+ then
-- We need to build a new primitive that overrides the inherited
-- one, and whose inherited expression has been updated above.
Set_Ekind (Id, E_Generic_Package);
Set_Etype (Id, Standard_Void_Type);
+ -- Set SPARK_Mode from context
+
+ Set_SPARK_Pragma (Id, SPARK_Mode_Pragma);
+ Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Id);
+ Set_SPARK_Aux_Pragma_Inherited (Id);
+
-- Analyze aspects now, so that generated pragmas appear in the
-- declarations before building and analyzing the generic copy.
Set_Ekind (Id, E_Package);
Set_Etype (Id, Standard_Void_Type);
- -- Set SPARK_Mode from context only for non-generic package
+ -- Set SPARK_Mode from context
- if Ekind (Id) = E_Package then
- Set_SPARK_Pragma (Id, SPARK_Mode_Pragma);
- Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma);
- Set_SPARK_Pragma_Inherited (Id);
- Set_SPARK_Aux_Pragma_Inherited (Id);
+ Set_SPARK_Pragma (Id, SPARK_Mode_Pragma);
+ Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Id);
+ Set_SPARK_Aux_Pragma_Inherited (Id);
- -- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in
- -- case the body of this package is instantiated or inlined later and
- -- out of context. The body uses this attribute to restore the value
- -- of the global flag.
+ -- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in case
+ -- the body of this package is instantiated or inlined later and out
+ -- of context. The body uses this attribute to restore the value of
+ -- the global flag.
- if Ignore_SPARK_Mode_Pragmas_In_Instance then
- Set_Ignore_SPARK_Mode_Pragmas (Id);
- end if;
+ if Ignore_SPARK_Mode_Pragmas_In_Instance then
+ Set_Ignore_SPARK_Mode_Pragmas (Id);
end if;
-- Analyze aspect specifications immediately, since we need to recognize
projects / gcc.git / commitdiff