exp_ch9.adb (Expand_Entry_Barrier): Code cleanup.

2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch9.adb (Expand_Entry_Barrier): Code
	cleanup. Do not perform the optimization which removes the
	declarations of the discriminant and component renamings when
	validity checks on operands and attributes are in effect.

2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_spark.adb, exp_util.adb, sem_ch7.adb, g-dyntab.adb, g-dyntab.ads,
	freeze.adb, a-cfinve.ads, a-cofuma.adb, a-cofuma.ads, a-cfhama.adb,
	a-cfhama.ads, a-cofove.ads: Minor reformatting.

2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* g-debpoo.adb (Dump_Gnatmem): Protect against a possible null
	pointer dereference.
	* g-spipat.adb (Dump): Code clean up. Protect against a possible
	null pointer dereference.

From-SVN: r247326
This commit is contained in:
Hristian Kirtchev 2017-04-27 12:18:31 +00:00 committed by Arnaud Charlet
parent a3ef4e650e
commit 3b2249aa1b
16 changed files with 370 additions and 303 deletions

View file

@ -1,3 +1,23 @@
2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch9.adb (Expand_Entry_Barrier): Code
cleanup. Do not perform the optimization which removes the
declarations of the discriminant and component renamings when
validity checks on operands and attributes are in effect.
2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* exp_spark.adb, exp_util.adb, sem_ch7.adb, g-dyntab.adb, g-dyntab.ads,
freeze.adb, a-cfinve.ads, a-cofuma.adb, a-cofuma.ads, a-cfhama.adb,
a-cfhama.ads, a-cofove.ads: Minor reformatting.
2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* g-debpoo.adb (Dump_Gnatmem): Protect against a possible null
pointer dereference.
* g-spipat.adb (Dump): Code clean up. Protect against a possible
null pointer dereference.
2017-04-27 Bob Duff <duff@adacore.com> 2017-04-27 Bob Duff <duff@adacore.com>
* g-dyntab.ads, g-dyntab.adb: Default for Table_Low_Bound. * g-dyntab.ads, g-dyntab.adb: Default for Table_Low_Bound.

View file

@ -38,7 +38,6 @@ with System; use type System.Address;
package body Ada.Containers.Formal_Hashed_Maps with package body Ada.Containers.Formal_Hashed_Maps with
SPARK_Mode => Off SPARK_Mode => Off
is is
----------------------- -----------------------
-- Local Subprograms -- -- Local Subprograms --
----------------------- -----------------------
@ -112,8 +111,10 @@ is
begin begin
Node := Left.First.Node; Node := Left.First.Node;
while Node /= 0 loop while Node /= 0 loop
ENode := Find (Container => Right, ENode :=
Key => Left.Nodes (Node).Key).Node; Find
(Container => Right,
Key => Left.Nodes (Node).Key).Node;
if ENode = 0 or else if ENode = 0 or else
Right.Nodes (ENode).Element /= Left.Nodes (Node).Element Right.Nodes (ENode).Element /= Left.Nodes (Node).Element
@ -202,11 +203,11 @@ is
Capacity : Count_Type := 0) return Map Capacity : Count_Type := 0) return Map
is is
C : constant Count_Type := C : constant Count_Type :=
Count_Type'Max (Capacity, Source.Capacity); Count_Type'Max (Capacity, Source.Capacity);
Cu : Cursor;
H : Hash_Type; H : Hash_Type;
N : Count_Type; N : Count_Type;
Target : Map (C, Source.Modulus); Target : Map (C, Source.Modulus);
Cu : Cursor;
begin begin
if 0 < Capacity and then Capacity < Source.Capacity then if 0 < Capacity and then Capacity < Source.Capacity then
@ -300,8 +301,8 @@ is
raise Constraint_Error with "Position cursor equals No_Element"; raise Constraint_Error with "Position cursor equals No_Element";
end if; end if;
pragma Assert (Vet (Container, Position), pragma Assert
"bad cursor in function Element"); (Vet (Container, Position), "bad cursor in function Element");
return Container.Nodes (Position.Node).Element; return Container.Nodes (Position.Node).Element;
end Element; end Element;
@ -429,9 +430,12 @@ is
-- for their postconditions. -- for their postconditions.
while Position /= 0 loop while Position /= 0 loop
R := M.Add (Container => R, R :=
New_Key => Container.Nodes (Position).Key, M.Add
New_Item => Container.Nodes (Position).Element); (Container => R,
New_Key => Container.Nodes (Position).Key,
New_Item => Container.Nodes (Position).Element);
Position := HT_Ops.Next (Container, Position); Position := HT_Ops.Next (Container, Position);
end loop; end loop;
@ -478,7 +482,6 @@ is
---------------------- ----------------------
procedure Generic_Allocate (HT : in out Map; Node : out Count_Type) is procedure Generic_Allocate (HT : in out Map; Node : out Count_Type) is
procedure Allocate is procedure Allocate is
new HT_Ops.Generic_Allocate (Set_Element); new HT_Ops.Generic_Allocate (Set_Element);
@ -600,8 +603,7 @@ is
Insert (Container, Key, New_Item, Position, Inserted); Insert (Container, Key, New_Item, Position, Inserted);
if not Inserted then if not Inserted then
raise Constraint_Error with raise Constraint_Error with "attempt to insert key already in map";
"attempt to insert key already in map";
end if; end if;
end Insert; end Insert;
@ -647,8 +649,9 @@ is
(Target : in out Map; (Target : in out Map;
Source : in out Map) Source : in out Map)
is is
NN : HT_Types.Nodes_Type renames Source.Nodes; NN : HT_Types.Nodes_Type renames Source.Nodes;
X, Y : Count_Type; X : Count_Type;
Y : Count_Type;
begin begin
if Target'Address = Source'Address then if Target'Address = Source'Address then
@ -695,8 +698,7 @@ is
end if; end if;
if not Has_Element (Container, Position) then if not Has_Element (Container, Position) then
raise Constraint_Error raise Constraint_Error with "Position has no element";
with "Position has no element";
end if; end if;
pragma Assert (Vet (Container, Position), "bad cursor in function Next"); pragma Assert (Vet (Container, Position), "bad cursor in function Next");
@ -731,8 +733,7 @@ is
begin begin
if Node = 0 then if Node = 0 then
raise Constraint_Error with raise Constraint_Error with "attempt to replace key not in map";
"attempt to replace key not in map";
end if; end if;
declare declare
@ -758,8 +759,8 @@ is
"Position cursor of Replace_Element has no element"; "Position cursor of Replace_Element has no element";
end if; end if;
pragma Assert (Vet (Container, Position), pragma Assert
"bad cursor in Replace_Element"); (Vet (Container, Position), "bad cursor in Replace_Element");
Container.Nodes (Position.Node).Element := New_Item; Container.Nodes (Position.Node).Element := New_Item;
end Replace_Element; end Replace_Element;
@ -821,8 +822,9 @@ is
return False; return False;
end if; end if;
X := Container.Buckets X :=
(Key_Ops.Index (Container, Container.Nodes (Position.Node).Key)); Container.Buckets
(Key_Ops.Index (Container, Container.Nodes (Position.Node).Key));
for J in 1 .. Container.Length loop for J in 1 .. Container.Length loop
if X = Position.Node then if X = Position.Node then

View file

@ -177,18 +177,16 @@ is
-- It contains all the keys contained in Model -- It contains all the keys contained in Model
and and (for all Key of Model (Container) =>
(for all Key of Model (Container) => (for some L of Keys'Result => Equivalent_Keys (L, Key)))
(for some L of Keys'Result => Equivalent_Keys (L, Key)))
-- It has no duplicate -- It has no duplicate
and and (for all I in 1 .. Length (Container) =>
(for all I in 1 .. Length (Container) => (for all J in 1 .. Length (Container) =>
(for all J in 1 .. Length (Container) => (if Equivalent_Keys
(if Equivalent_Keys (K.Get (Keys'Result, I), K.Get (Keys'Result, J))
(K.Get (Keys'Result, I), K.Get (Keys'Result, J)) then I = J)));
then I = J)));
pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys); pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys);
function Positions (Container : Map) return P.Map with function Positions (Container : Map) return P.Map with
@ -242,6 +240,7 @@ is
K : Key_Type) return Element_Type renames M.Get; K : Key_Type) return Element_Type renames M.Get;
-- To improve readability of contracts, we rename the function used to -- To improve readability of contracts, we rename the function used to
-- access an element in the model to Element. -- access an element in the model to Element.
end Formal_Model; end Formal_Model;
use Formal_Model; use Formal_Model;
@ -278,9 +277,8 @@ is
-- Actual keys are preserved -- Actual keys are preserved
and and (for all Key of Keys (Source) =>
(for all Key of Keys (Source) => Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key);
Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key);
function Copy function Copy
(Source : Map; (Source : Map;
@ -296,8 +294,8 @@ is
Copy'Result.Capacity = Source.Capacity Copy'Result.Capacity = Source.Capacity
else else
Copy'Result.Capacity = Capacity); Copy'Result.Capacity = Capacity);
-- Copy returns a container stricty equal to Source. It must have -- Copy returns a container stricty equal to Source. It must have the same
-- the same cursors associated with each element. Therefore: -- cursors associated with each element. Therefore:
-- - capacity=0 means use Source.Capacity as capacity of target -- - capacity=0 means use Source.Capacity as capacity of target
-- - the modulus cannot be changed. -- - the modulus cannot be changed.
@ -356,9 +354,8 @@ is
-- Actual keys are preserved -- Actual keys are preserved
and and (for all Key of Keys (Source)'Old =>
(for all Key of Keys (Source)'Old => Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key);
Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key);
procedure Insert procedure Insert
(Container : in out Map; (Container : in out Map;
@ -477,9 +474,9 @@ is
-- The key equivalent to Key in Container is replaced by Key -- The key equivalent to Key in Container is replaced by Key
and K.Get (Keys (Container), and K.Get
P.Get (Positions (Container), Find (Container, Key))) = (Keys (Container),
Key P.Get (Positions (Container), Find (Container, Key))) = Key
and K.Equal_Except and K.Equal_Except
(Keys (Container)'Old, (Keys (Container)'Old,
Keys (Container), Keys (Container),
@ -533,12 +530,13 @@ is
-- The key equivalent to Key in Container is replaced by Key -- The key equivalent to Key in Container is replaced by Key
and K.Get (Keys (Container), and K.Get
P.Get (Positions (Container), Find (Container, Key))) = Key (Keys (Container),
P.Get (Positions (Container), Find (Container, Key))) = Key
and K.Equal_Except and K.Equal_Except
(Keys (Container)'Old, (Keys (Container)'Old,
Keys (Container), Keys (Container),
P.Get (Positions (Container), Find (Container, Key))) P.Get (Positions (Container), Find (Container, Key)))
-- New_Item is now associated with the Key in Container -- New_Item is now associated with the Key in Container

View file

@ -58,19 +58,22 @@ is
pragma Annotate (CodePeer, Skip_Analysis); pragma Annotate (CodePeer, Skip_Analysis);
subtype Extended_Index is Index_Type'Base subtype Extended_Index is Index_Type'Base
range Index_Type'First - 1 .. range Index_Type'First - 1 ..
Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1; Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
No_Index : constant Extended_Index := Extended_Index'First; No_Index : constant Extended_Index := Extended_Index'First;
Last_Count : constant Count_Type := Last_Count : constant Count_Type :=
(if Index_Type'Last < Index_Type'First then 0 (if Index_Type'Last < Index_Type'First then
0
elsif Index_Type'Last < -1 elsif Index_Type'Last < -1
or else Index_Type'Pos (Index_Type'First) > or else Index_Type'Pos (Index_Type'First) >
Index_Type'Pos (Index_Type'Last) - Count_Type'Last Index_Type'Pos (Index_Type'Last) - Count_Type'Last
then Index_Type'Pos (Index_Type'Last) - then
Index_Type'Pos (Index_Type'First) + 1 Index_Type'Pos (Index_Type'Last) -
else Count_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 -- Maximal capacity of any vector. It is the minimum of the size of the
-- index range and the last possible Count_Type. -- index range and the last possible Count_Type.

View file

@ -52,19 +52,22 @@ is
pragma Annotate (CodePeer, Skip_Analysis); pragma Annotate (CodePeer, Skip_Analysis);
subtype Extended_Index is Index_Type'Base subtype Extended_Index is Index_Type'Base
range Index_Type'First - 1 .. range Index_Type'First - 1 ..
Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1; Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
No_Index : constant Extended_Index := Extended_Index'First; No_Index : constant Extended_Index := Extended_Index'First;
Last_Count : constant Count_Type := Last_Count : constant Count_Type :=
(if Index_Type'Last < Index_Type'First then 0 (if Index_Type'Last < Index_Type'First then
0
elsif Index_Type'Last < -1 elsif Index_Type'Last < -1
or else Index_Type'Pos (Index_Type'First) > or else Index_Type'Pos (Index_Type'First) >
Index_Type'Pos (Index_Type'Last) - Count_Type'Last Index_Type'Pos (Index_Type'Last) - Count_Type'Last
then Index_Type'Pos (Index_Type'Last) - then
Index_Type'Pos (Index_Type'First) + 1 Index_Type'Pos (Index_Type'Last) -
else Count_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 -- Maximal capacity of any vector. It is the minimum of the size of the
-- index range and the last possible Count_Type. -- index range and the last possible Count_Type.

View file

@ -95,8 +95,8 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
if not Equivalent_Keys (K, New_Key) if not Equivalent_Keys (K, New_Key)
and then and then
(Find (Right.Keys, K) = 0 (Find (Right.Keys, K) = 0
or else Get (Right.Elements, Find (Right.Keys, K)) /= or else Get (Right.Elements, Find (Right.Keys, K)) /=
Get (Left.Elements, I)) Get (Left.Elements, I))
then then
return False; return False;
end if; end if;
@ -120,8 +120,8 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
and then not Equivalent_Keys (K, Y) and then not Equivalent_Keys (K, Y)
and then and then
(Find (Right.Keys, K) = 0 (Find (Right.Keys, K) = 0
or else Get (Right.Elements, Find (Right.Keys, K)) /= or else Get (Right.Elements, Find (Right.Keys, K)) /=
Get (Left.Elements, I)) Get (Left.Elements, I))
then then
return False; return False;
end if; end if;

View file

@ -88,7 +88,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
Post => Post =>
Has_Key (Container, Left) = Has_Key (Container, Right) Has_Key (Container, Left) = Has_Key (Container, Right)
and (if Has_Key (Container, Left) then and (if Has_Key (Container, Left) then
Get (Container, Left) = Get (Container, Right)); Get (Container, Left) = Get (Container, Right));
------------------------ ------------------------
-- Property Functions -- -- Property Functions --
@ -101,7 +101,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
Post => Post =>
"<="'Result = "<="'Result =
(for all Key of Left => (for all Key of Left =>
Has_Key (Right, Key) and then Get (Right, Key) = Get (Left, Key)); Has_Key (Right, Key) and then Get (Right, Key) = Get (Left, Key));
function "=" (Left : Map; Right : Map) return Boolean with function "=" (Left : Map; Right : Map) return Boolean with
-- Extensional equality over maps -- Extensional equality over maps
@ -110,9 +110,9 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
Post => Post =>
"="'Result = "="'Result =
((for all Key of Left => ((for all Key of Left =>
Has_Key (Right, Key) Has_Key (Right, Key)
and then Get (Right, Key) = Get (Left, Key)) and then Get (Right, Key) = Get (Left, Key))
and (for all Key of Right => Has_Key (Left, Key))); and (for all Key of Right => Has_Key (Left, Key)));
pragma Warnings (Off, "unused variable ""Key"""); pragma Warnings (Off, "unused variable ""Key""");
function Is_Empty (Container : Map) return Boolean with function Is_Empty (Container : Map) return Boolean with

View file

@ -63,6 +63,7 @@ with Stand; use Stand;
with Targparm; use Targparm; with Targparm; use Targparm;
with Tbuild; use Tbuild; with Tbuild; use Tbuild;
with Uintp; use Uintp; with Uintp; use Uintp;
with Validsw; use Validsw;
package body Exp_Ch9 is package body Exp_Ch9 is
@ -5927,13 +5928,12 @@ package body Exp_Ch9 is
-------------------------- --------------------------
procedure Expand_Entry_Barrier (N : Node_Id; Ent : Entity_Id) is procedure Expand_Entry_Barrier (N : Node_Id; Ent : Entity_Id) is
Cond : constant Node_Id := Cond : constant Node_Id := Condition (Entry_Body_Formal_Part (N));
Condition (Entry_Body_Formal_Part (N));
Prot : constant Entity_Id := Scope (Ent); Prot : constant Entity_Id := Scope (Ent);
Spec_Decl : constant Node_Id := Parent (Prot); Spec_Decl : constant Node_Id := Parent (Prot);
Func : Entity_Id := Empty;
B_F : Node_Id; Func_Id : Entity_Id := Empty;
Body_Decl : Node_Id; -- The entity of the barrier function
function Is_Global_Entity (N : Node_Id) return Traverse_Result; function Is_Global_Entity (N : Node_Id) return Traverse_Result;
-- Check whether entity in Barrier is external to protected type. -- Check whether entity in Barrier is external to protected type.
@ -5966,7 +5966,7 @@ package body Exp_Ch9 is
-- during expansion, it is ok. If expansion is not performed, -- during expansion, it is ok. If expansion is not performed,
-- then Func is Empty so this test cannot succeed. -- then Func is Empty so this test cannot succeed.
if Scope (E) = Func then if Scope (E) = Func_Id then
null; null;
-- A protected call from a barrier to another object is ok -- A protected call from a barrier to another object is ok
@ -6112,6 +6112,12 @@ package body Exp_Ch9 is
function Check_Pure_Barriers is new Traverse_Func (Is_Pure_Barrier); function Check_Pure_Barriers is new Traverse_Func (Is_Pure_Barrier);
-- Local variables
Cond_Id : Entity_Id;
Entry_Body : Node_Id;
Func_Body : Node_Id;
-- Start of processing for Expand_Entry_Barrier -- Start of processing for Expand_Entry_Barrier
begin begin
@ -6130,20 +6136,20 @@ package body Exp_Ch9 is
-- version of it because it is never called. -- version of it because it is never called.
if Expander_Active then if Expander_Active then
B_F := Build_Barrier_Function (N, Ent, Prot); Func_Body := Build_Barrier_Function (N, Ent, Prot);
Func := Barrier_Function (Ent); Func_Id := Barrier_Function (Ent);
Set_Corresponding_Spec (B_F, Func); Set_Corresponding_Spec (Func_Body, Func_Id);
Body_Decl := Parent (Corresponding_Body (Spec_Decl)); Entry_Body := Parent (Corresponding_Body (Spec_Decl));
if Nkind (Parent (Body_Decl)) = N_Subunit then if Nkind (Parent (Entry_Body)) = N_Subunit then
Body_Decl := Corresponding_Stub (Parent (Body_Decl)); Entry_Body := Corresponding_Stub (Parent (Entry_Body));
end if; end if;
Insert_Before_And_Analyze (Body_Decl, B_F); Insert_Before_And_Analyze (Entry_Body, Func_Body);
Set_Discriminals (Spec_Decl); Set_Discriminals (Spec_Decl);
Set_Scope (Func, Scope (Prot)); Set_Scope (Func_Id, Scope (Prot));
else else
Analyze_And_Resolve (Cond, Any_Boolean); Analyze_And_Resolve (Cond, Any_Boolean);
@ -6167,20 +6173,25 @@ package body Exp_Ch9 is
-- scope. -- scope.
if Is_Entity_Name (Cond) then if Is_Entity_Name (Cond) then
Cond_Id := Entity (Cond);
-- A small optimization of useless renamings. If the scope of the -- Perform a small optimization of simple barrier functions. If the
-- entity of the condition is not the barrier function, then the -- scope of the condition's entity is not the barrier function, then
-- condition does not reference any of the generated renamings -- the condition does not depend on any of the generated renamings.
-- within the function. -- If this is the case, eliminate the renamings as they are useless.
-- This optimization is not performed when the condition was folded
-- and validity checks are in effect because the original condition
-- may have produced at least one check that depends on the generated
-- renamings.
if Expander_Active and then Scope (Entity (Cond)) /= Func then if Expander_Active
Set_Declarations (B_F, Empty_List); and then Scope (Cond_Id) /= Func_Id
and then not Validity_Check_Operands
then
Set_Declarations (Func_Body, Empty_List);
end if; end if;
if Entity (Cond) = Standard_False if Cond_Id = Standard_False or else Cond_Id = Standard_True then
or else
Entity (Cond) = Standard_True
then
return; return;
elsif Is_Simple_Barrier_Name (Cond) then elsif Is_Simple_Barrier_Name (Cond) then

View file

@ -251,9 +251,7 @@ package body Exp_SPARK is
-- specialized to the descendant type, hence build a separate DIC -- specialized to the descendant type, hence build a separate DIC
-- procedure for it as done during regular expansion for compilation. -- procedure for it as done during regular expansion for compilation.
if Has_DIC (E) if Has_DIC (E) and then Is_Tagged_Type (E) then
and then Is_Tagged_Type (E)
then
Build_DIC_Procedure_Body (E, For_Freeze => True); Build_DIC_Procedure_Body (E, For_Freeze => True);
end if; end if;
end Expand_SPARK_Freeze_Type; end Expand_SPARK_Freeze_Type;

View file

@ -1132,17 +1132,16 @@ package body Exp_Util is
if not Is_Abstract_Subprogram (Subp) if not Is_Abstract_Subprogram (Subp)
and then Is_Abstract_Subprogram (Entity (N)) and then Is_Abstract_Subprogram (Entity (N))
then then
Error_Msg_Sloc := Sloc (Current_Scope); Error_Msg_Sloc := Sloc (Current_Scope);
-- Error_Msg_Node_1 := Entity (N);
Error_Msg_Node_2 := Subp; Error_Msg_Node_2 := Subp;
if Comes_From_Source (Subp) then if Comes_From_Source (Subp) then
Error_Msg_NE Error_Msg_NE
("cannot call abstract subprogram& in inherited " ("cannot call abstract subprogram & in inherited "
& "condition for&#", Subp, Entity (N)); & "condition for&#", Subp, Entity (N));
else else
Error_Msg_NE Error_Msg_NE
("cannot call abstract subprogram& in inherited " ("cannot call abstract subprogram & in inherited "
& "condition for inherited&#", Subp, Entity (N)); & "condition for inherited&#", Subp, Entity (N));
end if; end if;
-- In SPARK mode, reject an inherited condition for an -- In SPARK mode, reject an inherited condition for an

View file

@ -1406,10 +1406,6 @@ package body Freeze is
Par_Prim : Entity_Id; Par_Prim : Entity_Id;
Prim : Entity_Id; Prim : Entity_Id;
---------------------------------------
-- Build_Inherited_Condition_Pragmas --
---------------------------------------
procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id); procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id);
-- Build corresponding pragmas for an operation whose ancestor has -- Build corresponding pragmas for an operation whose ancestor has
-- class-wide pre/postconditions. If the operation is inherited, the -- class-wide pre/postconditions. If the operation is inherited, the
@ -1418,6 +1414,10 @@ package body Freeze is
-- to verify their legality, in case they contain calls to other -- to verify their legality, in case they contain calls to other
-- primitives that may haven been overridden. -- primitives that may haven been overridden.
---------------------------------------
-- Build_Inherited_Condition_Pragmas --
---------------------------------------
procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id) is procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id) is
A_Post : Node_Id; A_Post : Node_Id;
A_Pre : Node_Id; A_Pre : Node_Id;
@ -1462,6 +1462,8 @@ package body Freeze is
end if; end if;
end Build_Inherited_Condition_Pragmas; end Build_Inherited_Condition_Pragmas;
-- Start of processing for Check_Inherited_Conditions
begin begin
Op_Node := First_Elmt (Prim_Ops); Op_Node := First_Elmt (Prim_Ops);
while Present (Op_Node) loop while Present (Op_Node) loop
@ -1480,13 +1482,14 @@ package body Freeze is
Next_Elmt (Op_Node); Next_Elmt (Op_Node);
end loop; end loop;
-- Now perform validity checks on the inherited conditions of -- Perform validity checks on the inherited conditions of overriding
-- overriding operations, for conformance with LSP, and apply -- operations, for conformance with LSP, and apply SPARK-specific
-- SPARK-specific restrictions on inherited conditions. -- restrictions on inherited conditions.
Op_Node := First_Elmt (Prim_Ops); Op_Node := First_Elmt (Prim_Ops);
while Present (Op_Node) loop while Present (Op_Node) loop
Prim := Node (Op_Node); Prim := Node (Op_Node);
if Present (Overridden_Operation (Prim)) if Present (Overridden_Operation (Prim))
and then Comes_From_Source (Prim) and then Comes_From_Source (Prim)
then then
@ -1505,11 +1508,10 @@ package body Freeze is
if SPARK_Mode = On then if SPARK_Mode = On then
Collect_Inherited_Class_Wide_Conditions (Prim); Collect_Inherited_Class_Wide_Conditions (Prim);
-- Otherwise build the corresponding pragmas to check for legality
-- of the inherited condition.
else else
-- Build the corresponding pragmas to check for legality
-- of the inherited condition.
Build_Inherited_Condition_Pragmas (Prim); Build_Inherited_Condition_Pragmas (Prim);
end if; end if;
end if; end if;
@ -1541,10 +1543,10 @@ package body Freeze is
Build_Inherited_Condition_Pragmas (Prim); Build_Inherited_Condition_Pragmas (Prim);
end if; end if;
if Needs_Wrapper and then not Is_Abstract_Subprogram (Par_Prim) if Needs_Wrapper
and then not Is_Abstract_Subprogram (Par_Prim)
and then Expander_Active and then Expander_Active
then then
-- We need to build a new primitive that overrides the inherited -- We need to build a new primitive that overrides the inherited
-- one, and whose inherited expression has been updated above. -- one, and whose inherited expression has been updated above.
-- These expressions are the arguments of pragmas that are part -- These expressions are the arguments of pragmas that are part

View file

@ -6,7 +6,7 @@
-- -- -- --
-- B o d y -- -- B o d y --
-- -- -- --
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. -- -- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
-- -- -- --
-- GNAT is free software; you can redistribute it and/or modify it under -- -- 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- -- -- terms of the GNU General Public License as published by the Free Soft- --
@ -401,7 +401,7 @@ package body GNAT.Debug_Pools is
--------------- ---------------
function Header_Of (Address : System.Address) function Header_Of (Address : System.Address)
return Allocation_Header_Access return Allocation_Header_Access
is is
function Convert is new Ada.Unchecked_Conversion function Convert is new Ada.Unchecked_Conversion
(System.Address, Allocation_Header_Access); (System.Address, Allocation_Header_Access);
@ -2293,8 +2293,12 @@ package body GNAT.Debug_Pools is
begin begin
File := fopen (File_Name & ASCII.NUL, "wb" & ASCII.NUL); File := fopen (File_Name & ASCII.NUL, "wb" & ASCII.NUL);
fwrite ("GMEM DUMP" & ASCII.LF, 10, 1, File); fwrite ("GMEM DUMP" & ASCII.LF, 10, 1, File);
fwrite (Dummy_Time'Address, Duration'Max_Size_In_Storage_Elements, 1,
File); fwrite
(Ptr => Dummy_Time'Address,
Size => Duration'Max_Size_In_Storage_Elements,
Nmemb => 1,
Stream => File);
-- List of not deallocated blocks (see Print_Info) -- List of not deallocated blocks (see Print_Info)
@ -2303,9 +2307,9 @@ package body GNAT.Debug_Pools is
Header := Header_Of (Current); Header := Header_Of (Current);
Actual_Size := size_t (Header.Block_Size); Actual_Size := size_t (Header.Block_Size);
Tracebk := Header.Alloc_Traceback.Traceback;
if Header.Alloc_Traceback /= null then if Header.Alloc_Traceback /= null then
Tracebk := Header.Alloc_Traceback.Traceback;
Num_Calls := Tracebk'Length; Num_Calls := Tracebk'Length;
-- (Code taken from memtrack.adb in GNAT's sources) -- (Code taken from memtrack.adb in GNAT's sources)
@ -2316,12 +2320,24 @@ package body GNAT.Debug_Pools is
fputc (Character'Pos ('A'), File); fputc (Character'Pos ('A'), File);
fwrite (Current'Address, Address_Size, 1, File); fwrite (Current'Address, Address_Size, 1, File);
fwrite (Actual_Size'Address, size_t'Max_Size_In_Storage_Elements,
1, File); fwrite
fwrite (Dummy_Time'Address, Duration'Max_Size_In_Storage_Elements, (Ptr => Actual_Size'Address,
1, File); Size => size_t'Max_Size_In_Storage_Elements,
fwrite (Num_Calls'Address, Integer'Max_Size_In_Storage_Elements, 1, Nmemb => 1,
File); Stream => File);
fwrite
(Ptr => Dummy_Time'Address,
Size => Duration'Max_Size_In_Storage_Elements,
Nmemb => 1,
Stream => File);
fwrite
(Ptr => Num_Calls'Address,
Size => Integer'Max_Size_In_Storage_Elements,
Nmemb => 1,
Stream => File);
for J in Tracebk'First .. Tracebk'First + Num_Calls - 1 loop for J in Tracebk'First .. Tracebk'First + Num_Calls - 1 loop
declare declare
@ -2330,7 +2346,6 @@ package body GNAT.Debug_Pools is
fwrite (Ptr'Address, Address_Size, 1, File); fwrite (Ptr'Address, Address_Size, 1, File);
end; end;
end loop; end loop;
end if; end if;
Current := Header.Next; Current := Header.Next;

View file

@ -284,18 +284,24 @@ package body GNAT.Dynamic_Tables is
-- Last, but if Release_Threshold /= 0, then we need to take that into -- Last, but if Release_Threshold /= 0, then we need to take that into
-- account. -- account.
------------------------
-- New_Last_Allocated --
------------------------
function New_Last_Allocated return Table_Last_Type is function New_Last_Allocated return Table_Last_Type is
subtype Table_Length_Type is Table_Index_Type'Base subtype Table_Length_Type is Table_Index_Type'Base
range 0 .. Table_Index_Type'Base'Last; range 0 .. Table_Index_Type'Base'Last;
Length : constant Table_Length_Type := T.P.Last - First + 1; Length : constant Table_Length_Type := T.P.Last - First + 1;
Comp_Size_In_Bytes : constant Table_Length_Type := Comp_Size_In_Bytes : constant Table_Length_Type :=
Table_Type'Component_Size / System.Storage_Unit; Table_Type'Component_Size / System.Storage_Unit;
Length_Threshold : constant Table_Length_Type := Length_Threshold : constant Table_Length_Type :=
Table_Length_Type (Release_Threshold) / Comp_Size_In_Bytes; Table_Length_Type (Release_Threshold) / Comp_Size_In_Bytes;
begin begin
if Release_Threshold = 0 if Release_Threshold = 0 or else Length < Length_Threshold then
or else Length < Length_Threshold
then
return T.P.Last; return T.P.Last;
else else
declare declare
@ -306,6 +312,8 @@ package body GNAT.Dynamic_Tables is
end if; end if;
end New_Last_Allocated; end New_Last_Allocated;
-- Local variables
New_Last_Alloc : constant Table_Last_Type := New_Last_Allocated; New_Last_Alloc : constant Table_Last_Type := New_Last_Allocated;
-- Start of processing for Release -- Start of processing for Release
@ -324,15 +332,15 @@ package body GNAT.Dynamic_Tables is
function To_Old_Alloc_Ptr is function To_Old_Alloc_Ptr is
new Ada.Unchecked_Conversion (Table_Ptr, Old_Alloc_Ptr); new Ada.Unchecked_Conversion (Table_Ptr, Old_Alloc_Ptr);
subtype Alloc_Type is subtype Alloc_Type is Table_Type (First .. New_Last_Alloc);
Table_Type (First .. New_Last_Alloc);
type Alloc_Ptr is access all Alloc_Type; type Alloc_Ptr is access all Alloc_Type;
function To_Table_Ptr is function To_Table_Ptr is
new Ada.Unchecked_Conversion (Alloc_Ptr, Table_Ptr); new Ada.Unchecked_Conversion (Alloc_Ptr, Table_Ptr);
Old_Table : Old_Alloc_Ptr := To_Old_Alloc_Ptr (T.Table); Old_Table : Old_Alloc_Ptr := To_Old_Alloc_Ptr (T.Table);
New_Table : constant Alloc_Ptr := new Alloc_Type; New_Table : constant Alloc_Ptr := new Alloc_Type;
begin begin
New_Table (Alloc_Type'Range) := Old_Table (Alloc_Type'Range); New_Table (Alloc_Type'Range) := Old_Table (Alloc_Type'Range);
T.P.Last_Allocated := New_Last_Alloc; T.P.Last_Allocated := New_Last_Alloc;
@ -353,6 +361,7 @@ package body GNAT.Dynamic_Tables is
is is
pragma Assert (not T.Locked); pragma Assert (not T.Locked);
Item_Copy : constant Table_Component_Type := Item; Item_Copy : constant Table_Component_Type := Item;
begin begin
-- If Set_Last is going to reallocate the table, we make a copy of Item, -- If Set_Last is going to reallocate the table, we make a copy of Item,
-- in case the call was "Set_Item (T, X, T.Table (Y));", and Item is -- in case the call was "Set_Item (T, X, T.Table (Y));", and Item is

View file

@ -69,12 +69,12 @@ package GNAT.Dynamic_Tables is
-- Table_Component_Type must not be a type with controlled parts. -- Table_Component_Type must not be a type with controlled parts.
-- The Table_Initial value controls the allocation of the table when -- The Table_Initial value controls the allocation of the table when it is
-- it is first allocated. -- first allocated.
-- The Table_Increment value controls the amount of increase, if the -- The Table_Increment value controls the amount of increase, if the table
-- table has to be increased in size. The value given is a percentage -- has to be increased in size. The value given is a percentage value (e.g.
-- value (e.g. 100 = increase table size by 100%, i.e. double it). -- 100 = increase table size by 100%, i.e. double it).
-- The Last and Set_Last subprograms provide control over the current -- The Last and Set_Last subprograms provide control over the current
-- logical allocation. They are quite efficient, so they can be used -- logical allocation. They are quite efficient, so they can be used
@ -85,18 +85,18 @@ package GNAT.Dynamic_Tables is
-- restrict the use of table for discriminated types. If it is necessary -- restrict the use of table for discriminated types. If it is necessary
-- to take the access of a table element, use Unrestricted_Access. -- to take the access of a table element, use Unrestricted_Access.
-- WARNING: On HPPA, the virtual addressing approach used in this unit -- WARNING: On HPPA, the virtual addressing approach used in this unit is
-- is incompatible with the indexing instructions on the HPPA. So when -- incompatible with the indexing instructions on the HPPA. So when using
-- using this unit, compile your application with -mdisable-indexing. -- this unit, compile your application with -mdisable-indexing.
-- WARNING: If the table is reallocated, then the address of all its -- WARNING: If the table is reallocated, then the address of all its
-- components will change. So do not capture the address of an element -- components will change. So do not capture the address of an element
-- and then use the address later after the table may be reallocated. -- and then use the address later after the table may be reallocated. One
-- One tricky case of this is passing an element of the table to a -- tricky case of this is passing an element of the table to a subprogram
-- subprogram by reference where the table gets reallocated during -- by reference where the table gets reallocated during the execution of
-- the execution of the subprogram. The best rule to follow is never -- the subprogram. The best rule to follow is never to pass a table element
-- to pass a table element as a parameter except for the case of IN -- as a parameter except for the case of IN mode parameters with scalar
-- mode parameters with scalar values. -- values.
pragma Assert (Table_Low_Bound /= Table_Index_Type'Base'First); pragma Assert (Table_Low_Bound /= Table_Index_Type'Base'First);
@ -107,12 +107,12 @@ package GNAT.Dynamic_Tables is
-- Table_Component_Type must not be a type with controlled parts. -- Table_Component_Type must not be a type with controlled parts.
-- The Table_Initial value controls the allocation of the table when -- The Table_Initial value controls the allocation of the table when it is
-- it is first allocated. -- first allocated.
-- The Table_Increment value controls the amount of increase, if the -- The Table_Increment value controls the amount of increase, if the table
-- table has to be increased in size. The value given is a percentage -- has to be increased in size. The value given is a percentage value (e.g.
-- value (e.g. 100 = increase table size by 100%, i.e. double it). -- 100 = increase table size by 100%, i.e. double it).
-- The Last and Set_Last subprograms provide control over the current -- The Last and Set_Last subprograms provide control over the current
-- logical allocation. They are quite efficient, so they can be used -- logical allocation. They are quite efficient, so they can be used
@ -201,9 +201,9 @@ package GNAT.Dynamic_Tables is
procedure Release (T : in out Instance); procedure Release (T : in out Instance);
-- Storage is allocated in chunks according to the values given in the -- Storage is allocated in chunks according to the values given in the
-- Table_Initial and Table_Increment parameters. If Release_Threshold is 0 -- Table_Initial and Table_Increment parameters. If Release_Threshold is
-- or the length of the table does not exceed this threshold then a call to -- 0 or the length of the table does not exceed this threshold then a call
-- Release releases all storage that is allocated, but is not logically -- to Release releases all storage that is allocated, but is not logically
-- part of the current array value; otherwise the call to Release leaves -- part of the current array value; otherwise the call to Release leaves
-- the current array value plus 0.1% of the current table length free -- the current array value plus 0.1% of the current table length free
-- elements located at the end of the table. This parameter facilitates -- elements located at the end of the table. This parameter facilitates
@ -267,14 +267,14 @@ package GNAT.Dynamic_Tables is
generic generic
with function Lt (Comp1, Comp2 : Table_Component_Type) return Boolean; with function Lt (Comp1, Comp2 : Table_Component_Type) return Boolean;
procedure Sort_Table (Table : in out Instance); procedure Sort_Table (Table : in out Instance);
-- This procedure sorts the components of the table into ascending -- This procedure sorts the components of the table into ascending order
-- order making calls to Lt to do required comparisons, and using -- making calls to Lt to do required comparisons, and using assignments
-- assignments to move components around. The Lt function returns True -- to move components around. The Lt function returns True if Comp1 is
-- if Comp1 is less than Comp2 (in the sense of the desired sort), and -- less than Comp2 (in the sense of the desired sort), and False if Comp1
-- False if Comp1 is greater than Comp2. For equal objects it does not -- is greater than Comp2. For equal objects it does not matter if True or
-- matter if True or False is returned (it is slightly more efficient -- False is returned (it is slightly more efficient to return False). The
-- to return False). The sort is not stable (the order of equal items -- sort is not stable (the order of equal items in the table is not
-- in the table is not preserved). -- preserved).
private private

View file

@ -6,7 +6,7 @@
-- -- -- --
-- B o d y -- -- B o d y --
-- -- -- --
-- Copyright (C) 1998-2016, AdaCore -- -- Copyright (C) 1998-2017, AdaCore --
-- -- -- --
-- GNAT is free software; you can redistribute it and/or modify it under -- -- 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- -- -- terms of the GNU General Public License as published by the Free Soft- --
@ -2086,28 +2086,15 @@ package body GNAT.Spitbol.Patterns is
---------- ----------
procedure Dump (P : Pattern) is procedure Dump (P : Pattern) is
procedure Write_Node_Id (E : PE_Ptr; Cols : Natural);
subtype Count is Ada.Text_IO.Count; -- Writes out a string identifying the given pattern element. Cols is
Scol : Count; -- the column indentation level.
-- Used to keep track of column in dump output
Refs : Ref_Array (1 .. P.P.Index);
-- We build a reference array whose N'th element points to the
-- pattern element whose Index value is N.
Cols : Natural := 2;
-- Number of columns used for pattern numbers, minimum is 2
E : PE_Ptr;
procedure Write_Node_Id (E : PE_Ptr);
-- Writes out a string identifying the given pattern element
------------------- -------------------
-- Write_Node_Id -- -- Write_Node_Id --
------------------- -------------------
procedure Write_Node_Id (E : PE_Ptr) is procedure Write_Node_Id (E : PE_Ptr; Cols : Natural) is
begin begin
if E = EOP then if E = EOP then
Put ("EOP"); Put ("EOP");
@ -2134,16 +2121,29 @@ package body GNAT.Spitbol.Patterns is
end if; end if;
end Write_Node_Id; end Write_Node_Id;
-- Local variables
Cols : Natural := 2;
-- Number of columns used for pattern numbers, minimum is 2
E : PE_Ptr;
subtype Count is Ada.Text_IO.Count;
Scol : Count;
-- Used to keep track of column in dump output
-- Start of processing for Dump -- Start of processing for Dump
begin begin
New_Line; New_Line;
Put ("Pattern Dump Output (pattern at " & Put
Image (P'Address) & ("Pattern Dump Output (pattern at "
", S = " & Natural'Image (P.Stk) & ')'); & Image (P'Address)
& ", S = "
& Natural'Image (P.Stk) & ')');
New_Line;
Scol := Col; Scol := Col;
New_Line;
while Col < Scol loop while Col < Scol loop
Put ('-'); Put ('-');
@ -2165,144 +2165,151 @@ package body GNAT.Spitbol.Patterns is
return; return;
end if; end if;
Build_Ref_Array (P.P, Refs); declare
Refs : Ref_Array (1 .. P.P.Index);
-- We build a reference array whose N'th element points to the
-- pattern element whose Index value is N.
-- Set number of columns required for node numbers begin
Build_Ref_Array (P.P, Refs);
while 10 ** Cols - 1 < Integer (P.P.Index) loop -- Set number of columns required for node numbers
Cols := Cols + 1;
end loop;
-- Now dump the nodes in reverse sequence. We output them in reverse while 10 ** Cols - 1 < Integer (P.P.Index) loop
-- sequence since this corresponds to the natural order used to Cols := Cols + 1;
-- construct the patterns. end loop;
for J in reverse Refs'Range loop -- Now dump the nodes in reverse sequence. We output them in reverse
E := Refs (J); -- sequence since this corresponds to the natural order used to
Write_Node_Id (E); -- construct the patterns.
Set_Col (Count (Cols) + 4);
Put (Image (E));
Put (" ");
Put (Pattern_Code'Image (E.Pcode));
Put (" ");
Set_Col (21 + Count (Cols) + Address_Image_Length);
Write_Node_Id (E.Pthen);
Set_Col (24 + 2 * Count (Cols) + Address_Image_Length);
case E.Pcode is for J in reverse Refs'Range loop
when PC_Alt E := Refs (J);
| PC_Arb_X Write_Node_Id (E, Cols);
| PC_Arbno_S Set_Col (Count (Cols) + 4);
| PC_Arbno_X Put (Image (E));
=> Put (" ");
Write_Node_Id (E.Alt); Put (Pattern_Code'Image (E.Pcode));
Put (" ");
Set_Col (21 + Count (Cols) + Address_Image_Length);
Write_Node_Id (E.Pthen, Cols);
Set_Col (24 + 2 * Count (Cols) + Address_Image_Length);
when PC_Rpat => case E.Pcode is
Put (Str_PP (E.PP)); when PC_Alt
| PC_Arb_X
| PC_Arbno_S
| PC_Arbno_X
=>
Write_Node_Id (E.Alt, Cols);
when PC_Pred_Func => when PC_Rpat =>
Put (Str_BF (E.BF)); Put (Str_PP (E.PP));
when PC_Assign_Imm when PC_Pred_Func =>
| PC_Assign_OnM Put (Str_BF (E.BF));
| PC_Any_VP
| PC_Break_VP
| PC_BreakX_VP
| PC_NotAny_VP
| PC_NSpan_VP
| PC_Span_VP
| PC_String_VP
=>
Put (Str_VP (E.VP));
when PC_Write_Imm when PC_Assign_Imm
| PC_Write_OnM | PC_Assign_OnM
=> | PC_Any_VP
Put (Str_FP (E.FP)); | PC_Break_VP
| PC_BreakX_VP
| PC_NotAny_VP
| PC_NSpan_VP
| PC_Span_VP
| PC_String_VP
=>
Put (Str_VP (E.VP));
when PC_String => when PC_Write_Imm
Put (Image (E.Str.all)); | PC_Write_OnM
=>
Put (Str_FP (E.FP));
when PC_String_2 => when PC_String =>
Put (Image (E.Str2)); Put (Image (E.Str.all));
when PC_String_3 => when PC_String_2 =>
Put (Image (E.Str3)); Put (Image (E.Str2));
when PC_String_4 => when PC_String_3 =>
Put (Image (E.Str4)); Put (Image (E.Str3));
when PC_String_5 => when PC_String_4 =>
Put (Image (E.Str5)); Put (Image (E.Str4));
when PC_String_6 => when PC_String_5 =>
Put (Image (E.Str6)); Put (Image (E.Str5));
when PC_Setcur => when PC_String_6 =>
Put (Str_NP (E.Var)); Put (Image (E.Str6));
when PC_Any_CH when PC_Setcur =>
| PC_Break_CH Put (Str_NP (E.Var));
| PC_BreakX_CH
| PC_Char
| PC_NotAny_CH
| PC_NSpan_CH
| PC_Span_CH
=>
Put (''' & E.Char & ''');
when PC_Any_CS when PC_Any_CH
| PC_Break_CS | PC_Break_CH
| PC_BreakX_CS | PC_BreakX_CH
| PC_NotAny_CS | PC_Char
| PC_NSpan_CS | PC_NotAny_CH
| PC_Span_CS | PC_NSpan_CH
=> | PC_Span_CH
Put ('"' & To_Sequence (E.CS) & '"'); =>
Put (''' & E.Char & ''');
when PC_Arbno_Y when PC_Any_CS
| PC_Len_Nat | PC_Break_CS
| PC_Pos_Nat | PC_BreakX_CS
| PC_RPos_Nat | PC_NotAny_CS
| PC_RTab_Nat | PC_NSpan_CS
| PC_Tab_Nat | PC_Span_CS
=> =>
Put (S (E.Nat)); Put ('"' & To_Sequence (E.CS) & '"');
when PC_Pos_NF when PC_Arbno_Y
| PC_Len_NF | PC_Len_Nat
| PC_RPos_NF | PC_Pos_Nat
| PC_RTab_NF | PC_RPos_Nat
| PC_Tab_NF | PC_RTab_Nat
=> | PC_Tab_Nat
Put (Str_NF (E.NF)); =>
Put (S (E.Nat));
when PC_Pos_NP when PC_Pos_NF
| PC_Len_NP | PC_Len_NF
| PC_RPos_NP | PC_RPos_NF
| PC_RTab_NP | PC_RTab_NF
| PC_Tab_NP | PC_Tab_NF
=> =>
Put (Str_NP (E.NP)); Put (Str_NF (E.NF));
when PC_Any_VF when PC_Pos_NP
| PC_Break_VF | PC_Len_NP
| PC_BreakX_VF | PC_RPos_NP
| PC_NotAny_VF | PC_RTab_NP
| PC_NSpan_VF | PC_Tab_NP
| PC_Span_VF =>
| PC_String_VF Put (Str_NP (E.NP));
=>
Put (Str_VF (E.VF));
when others => when PC_Any_VF
null; | PC_Break_VF
end case; | PC_BreakX_VF
| PC_NotAny_VF
| PC_NSpan_VF
| PC_Span_VF
| PC_String_VF
=>
Put (Str_VF (E.VF));
when others =>
null;
end case;
New_Line;
end loop;
New_Line; New_Line;
end loop; end;
New_Line;
end Dump; end Dump;
---------- ----------

View file

@ -983,9 +983,9 @@ package body Sem_Ch7 is
Set_SPARK_Aux_Pragma_Inherited (Id); Set_SPARK_Aux_Pragma_Inherited (Id);
-- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in case -- 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 -- the body of this package is instantiated or inlined later and out of
-- of context. The body uses this attribute to restore the value of -- context. The body uses this attribute to restore the value of the
-- the global flag. -- global flag.
if Ignore_SPARK_Mode_Pragmas_In_Instance then if Ignore_SPARK_Mode_Pragmas_In_Instance then
Set_Ignore_SPARK_Mode_Pragmas (Id); Set_Ignore_SPARK_Mode_Pragmas (Id);