+2017-04-27 Bob Duff <duff@adacore.com>
+
+ * g-dyntab.ads, g-dyntab.adb: Add assertions to subprograms that
+ can reallocate.
+ * atree.adb, elists.adb, fname-uf.adb, ghost.adb, inline.adb,
+ * lib.adb, namet.adb, nlists.adb, sem.adb, sinput.adb, stringt.adb:
+ Reorder code so that above assertions do not fail.
+ * table.ads: Remove obsolete comment on Locked.
+
+2017-04-27 Claire Dross <dross@adacore.com>
+
+ * a-cfdlli.ads: Code cleanup.
+
+2017-04-27 Yannick Moy <moy@adacore.com>
+
+ * exp_spark.adb (Expand_SPARK_Freeze_Type): Build a DIC procedure
+ when needed for proof. (Expand_SPARK): Call the new procedure.
+ * exp_util.ads Fix typo.
+
+2017-04-27 Gary Dismukes <dismukes@adacore.com>
+
+ * a-cofuma.ads, a-cfhama.ads: Minor reformatting, grammar, and typo
+ fixes.
+
2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* sem_elab.adb Add new type Visited_Element
-- Big contains all cursors of Small
- P.Keys_Included (Small, Big)
+ (P.Keys_Included (Small, Big)
-- Cursors located before Cut are not moved, cursors located
-- after are shifted by Count.
and (for all I of Big =>
P.Has_Key (Small, I)
- or P.Get (Big, I) - Count in Cut - Count .. Cut - 1);
+ or P.Get (Big, I) - Count in Cut - Count .. Cut - 1));
function P_Positions_Swapped
(Left : P.Map;
-- and its previous version C'Old) for expressing properties, which is not
-- possible if cursors encapsulate an access to the underlying container.
--- Iteration over maps is done using the Iterable aspect which is SPARK
--- compatible. For of iteration ranges over keys instead of elements.
+-- Iteration over maps is done using the Iterable aspect, which is SPARK
+-- compatible. "For of" iteration ranges over keys instead of elements.
with Ada.Containers.Functional_Vectors;
with Ada.Containers.Functional_Maps;
K.Get (K_Right, P.Get (P_Right, C))));
function Model (Container : Map) return M.Map with
- -- The highlevel model of a map is a map from keys to elements. Neither
+ -- The high-level model of a map is a map from keys to elements. Neither
-- cursors nor order of elements are represented in this model. Keys are
-- modeled up to equivalence.
function Positions (Container : Map) return P.Map with
-- The Positions map is used to model cursors. It only contains valid
- -- cursors and map them to their position in the container.
+ -- cursors and maps them to their position in the container.
Ghost,
Global => null,
Post =>
not P.Has_Key (Positions'Result, No_Element)
- -- Positions of cursors are smaller than the container's length.
+ -- Positions of cursors are smaller than the container's length
and then
(for all I of Positions'Result =>
procedure Lift_Abstraction_Level (Container : Map) with
-- Lift_Abstraction_Level is a ghost procedure that does nothing but
- -- assume that we can access to the same elements by iterating over
+ -- assume that we can access the same elements by iterating over
-- positions or cursors.
-- This information is not generally useful except when switching from
- -- a lowlevel, cursor aware view of a container, to a highlevel
- -- position based view.
+ -- a low-level, cursor-aware view of a container, to a high-level,
+ -- position-based view.
Ghost,
Global => null,
Pre => Has_Element (Container, Position),
Post =>
- -- Order of keys and cursors are preserved
+ -- Order of keys and cursors is preserved
Keys (Container) = Keys (Container)'Old
and Positions (Container) = Positions (Container)'Old
- -- New_Item is now associated to the key at position Position in
+ -- New_Item is now associated with the key at position Position in
-- Container.
and Element (Container, Position) = New_Item
- -- Elements associated to other keys are preserved
+ -- Elements associated with other keys are preserved
and M.Same_Keys (Model (Container), Model (Container)'Old)
and M.Elements_Equal_Except
Model (Container)'Old,
Key)
- -- Mapping from cursors to keys are preserved
+ -- Mapping from cursors to keys is preserved
and Mapping_Preserved
(K_Left => Keys (Container)'Old,
Model (Container)'Old,
Key)
- -- Mapping from cursors to keys are preserved
+ -- Mapping from cursors to keys is preserved
and Mapping_Preserved
(K_Left => Keys (Container)'Old,
Keys (Container),
P.Get (Positions (Container), Find (Container, Key)))
- -- Elements associated to other keys are preserved
+ -- Elements associated with other keys are preserved
and M.Same_Keys (Model (Container), Model (Container)'Old)
and M.Elements_Equal_Except
Model (Container)'Old,
Key)
- -- Mapping from cursors to keys are preserved
+ -- Mapping from cursors to keys is preserved
and Mapping_Preserved
(K_Left => Keys (Container)'Old,
Keys (Container),
P.Get (Positions (Container), Find (Container, Key)))
- -- New_Item is now associated to the Key in Container
+ -- New_Item is now associated with the Key in Container
and Element (Model (Container), Key) = New_Item
- -- Elements associated to other keys are preserved
+ -- Elements associated with other keys are preserved
and M.Same_Keys (Model (Container), Model (Container)'Old)
and M.Elements_Equal_Except
Model (Container),
Key)
- -- Mapping from cursors to keys are preserved
+ -- Mapping from cursors to keys is preserved
and Mapping_Preserved
(K_Left => Keys (Container),
Model (Container),
Key)
- -- Mapping from cursors to keys are preserved
+ -- Mapping from cursors to keys is preserved
and Mapping_Preserved
(K_Left => Keys (Container),
Model (Container),
Key (Container, Position)'Old)
- -- Mapping from cursors to keys are preserved
+ -- Mapping from cursors to keys is preserved
and Mapping_Preserved
(K_Left => Keys (Container),
(not Contains (Model (Container), Key) =>
Find'Result = No_Element,
- -- Otherwise, Find returns a valid cusror in Container
+ -- Otherwise, Find returns a valid cursor in Container
others =>
P.Has_Key (Positions (Container), Find'Result)
-- Maps are empty when default initialized.
-- "For in" quantification over maps should not be used.
-- "For of" quantification over maps iterates over keys.
- -- Note that, for proof, for of quantification is understood modulo
+ -- Note that, for proof, "for of" quantification is understood modulo
-- equivalence (quantification includes keys equivalent to keys of the
-- map).
-- --
-- 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 --
-- terms of the GNU General Public License as published by the Free Soft- --
procedure Lock is
begin
- Nodes.Locked := True;
- Flags.Locked := True;
- Orig_Nodes.Locked := True;
Nodes.Release;
+ Nodes.Locked := True;
Flags.Release;
+ Flags.Locked := True;
Orig_Nodes.Release;
+ Orig_Nodes.Locked := True;
end Lock;
----------------
-- --
-- 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 --
-- terms of the GNU General Public License as published by the Free Soft- --
procedure Lock is
begin
- Elists.Locked := True;
- Elmts.Locked := True;
Elists.Release;
+ Elists.Locked := True;
Elmts.Release;
+ Elmts.Locked := True;
end Lock;
--------------------
-- Replace occurrences of System'To_Address by calls to
-- System.Storage_Elements.To_Address
+ procedure Expand_SPARK_Freeze_Type (E : Entity_Id);
+ -- Build the DIC procedure of a type when needed, if not already done
+
procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
-- Perform object-declaration-specific expansion
when N_Object_Renaming_Declaration =>
Expand_SPARK_N_Object_Renaming_Declaration (N);
+ when N_Freeze_Entity =>
+ if Is_Type (Entity (N)) then
+ Expand_SPARK_Freeze_Type (Entity (N));
+ end if;
+
-- In SPARK mode, no other constructs require expansion
when others =>
end if;
end Expand_SPARK_N_Attribute_Reference;
+ ------------------------------
+ -- Expand_SPARK_Freeze_Type --
+ ------------------------------
+
+ procedure Expand_SPARK_Freeze_Type (E : Entity_Id) is
+ begin
+ -- When a DIC is inherited by a tagged type, it may need to be
+ -- specialized to the descendant type, hence build a separate DIC
+ -- procedure for it as done during regular expansion for compilation.
+
+ if Has_DIC (E)
+ and then Is_Tagged_Type (E)
+ then
+ Build_DIC_Procedure_Body (E, For_Freeze => True);
+ end if;
+ end Expand_SPARK_Freeze_Type;
+
---------------------------------------
-- Expand_SPARK_N_Object_Declaration --
---------------------------------------
For_Freeze : Boolean := False);
-- Create the body of the procedure which verifies the assertion expression
-- of pragma Default_Initial_Condition at run time. Flag For_Freeze should
- -- be set when the body is construction as part of the freezing actions for
+ -- be set when the body is constructed as part of the freezing actions for
-- Typ.
procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id);
-- --
-- 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 --
-- terms of the GNU General Public License as published by the Free Soft- --
procedure Lock is
begin
- SFN_Table.Locked := True;
SFN_Table.Release;
+ SFN_Table.Locked := True;
end Lock;
-------------------
begin
-- Note that Num can be negative
+ pragma Assert (not T.Locked);
Set_Last (T, T.P.Last + Table_Index_Type'Base (Num));
end Allocate;
procedure Append (T : in out Instance; New_Val : Table_Component_Type) is
begin
+ pragma Assert (not T.Locked);
Set_Item (T, T.P.Last + 1, New_Val);
end Append;
procedure Decrement_Last (T : in out Instance) is
begin
+ pragma Assert (not T.Locked);
Allocate (T, -1);
end Decrement_Last;
----------
procedure Free (T : in out Instance) is
+ pragma Assert (not T.Locked);
subtype Alloc_Type is Table_Type (First .. T.P.Last_Allocated);
type Alloc_Ptr is access all Alloc_Type;
procedure Increment_Last (T : in out Instance) is
begin
+ pragma Assert (not T.Locked);
Allocate (T, 1);
end Increment_Last;
procedure Init (T : in out Instance) is
begin
+ pragma Assert (not T.Locked);
Free (T);
end Init;
procedure Move (From, To : in out Instance) is
begin
+ pragma Assert (not From.Locked);
+ pragma Assert (not To.Locked);
pragma Assert (Is_Empty (To));
To := From;
-------------
procedure Release (T : in out Instance) is
+ pragma Assert (not T.Locked);
Old_Last_Allocated : constant Table_Last_Type := T.P.Last_Allocated;
function New_Last_Allocated return Table_Last_Type;
Index : Valid_Table_Index_Type;
Item : Table_Component_Type)
is
+ pragma Assert (not T.Locked);
Item_Copy : constant Table_Component_Type := Item;
begin
-- If Set_Last is going to reallocate the table, we make a copy of Item,
procedure Set_Last (T : in out Instance; New_Val : Table_Last_Type) is
begin
+ pragma Assert (not T.Locked);
if New_Val > T.P.Last_Allocated then
Grow (T, New_Val);
end if;
-- SCO_Unit_Table and SCO_Table in scos.h.
Locked : Boolean := False;
- -- Table expansion is permitted only if this is False. A client may set
- -- Locked to True, in which case any attempt to expand the table will
- -- cause an assertion failure. Note that while a table is locked, its
- -- address in memory remains fixed and unchanging.
+ -- Table reallocation is permitted only if this is False. A client may
+ -- set Locked to True, in which case any operation that might expand or
+ -- shrink the table will cause an assertion failure. While a table is
+ -- locked, its address in memory remains fixed and unchanging.
P : Table_Private;
end record;
procedure Lock is
begin
- Ignored_Ghost_Units.Locked := True;
Ignored_Ghost_Units.Release;
+ Ignored_Ghost_Units.Locked := True;
end Lock;
-----------------------------------
-- --
-- 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 --
-- terms of the GNU General Public License as published by the Free Soft- --
procedure Lock is
begin
- Pending_Instantiations.Locked := True;
- Inlined_Bodies.Locked := True;
- Successors.Locked := True;
- Inlined.Locked := True;
Pending_Instantiations.Release;
+ Pending_Instantiations.Locked := True;
Inlined_Bodies.Release;
+ Inlined_Bodies.Locked := True;
Successors.Release;
+ Successors.Locked := True;
Inlined.Release;
+ Inlined.Locked := True;
end Lock;
--------------------------------
-- --
-- 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 --
-- terms of the GNU General Public License as published by the Free Soft- --
procedure Lock is
begin
- Linker_Option_Lines.Locked := True;
- Load_Stack.Locked := True;
- Units.Locked := True;
Linker_Option_Lines.Release;
+ Linker_Option_Lines.Locked := True;
Load_Stack.Release;
+ Load_Stack.Locked := True;
Units.Release;
+ Units.Locked := True;
end Lock;
---------------
begin
Name_Chars.Set_Last (Name_Chars.Last + Name_Chars_Reserve);
Name_Entries.Set_Last (Name_Entries.Last + Name_Entries_Reserve);
- Name_Chars.Locked := True;
- Name_Entries.Locked := True;
Name_Chars.Release;
+ Name_Chars.Locked := True;
Name_Entries.Release;
+ Name_Entries.Locked := True;
end Lock;
----------------
procedure Unlock is
begin
- Name_Chars.Set_Last (Name_Chars.Last - Name_Chars_Reserve);
- Name_Entries.Set_Last (Name_Entries.Last - Name_Entries_Reserve);
Name_Chars.Locked := False;
- Name_Entries.Locked := False;
+ Name_Chars.Set_Last (Name_Chars.Last - Name_Chars_Reserve);
Name_Chars.Release;
+ Name_Entries.Locked := False;
+ Name_Entries.Set_Last (Name_Entries.Last - Name_Entries_Reserve);
Name_Entries.Release;
end Unlock;
-- --
-- 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 --
-- terms of the GNU General Public License as published by the Free Soft- --
procedure Lock is
begin
- Lists.Locked := True;
Lists.Release;
-
- Prev_Node.Locked := True;
- Next_Node.Locked := True;
-
+ Lists.Locked := True;
Prev_Node.Release;
+ Prev_Node.Locked := True;
Next_Node.Release;
+ Next_Node.Locked := True;
end Lock;
----------------
procedure Lock is
begin
- Scope_Stack.Locked := True;
Scope_Stack.Release;
+ Scope_Stack.Locked := True;
end Lock;
----------------
procedure Lock is
begin
- Source_File.Locked := True;
Source_File.Release;
+ Source_File.Locked := True;
end Lock;
----------------------
-- --
-- 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 --
-- terms of the GNU General Public License as published by the Free Soft- --
procedure Lock is
begin
- String_Chars.Locked := True;
- Strings.Locked := True;
String_Chars.Release;
+ String_Chars.Locked := True;
Strings.Release;
+ Strings.Locked := True;
end Lock;
----------
Table : Table_Ptr renames Tab.Table;
Locked : Boolean renames Tab.Locked;
- -- Table expansion is permitted only if this switch is set to False. A
- -- client may set Locked to True, in which case any attempt to expand
- -- the table will cause an assertion failure. Note that while a table
- -- is locked, its address in memory remains fixed and unchanging. This
- -- feature is used to control table expansion during Gigi processing.
- -- Gigi assumes that tables other than the Uint and Ureal tables do
- -- not move during processing, which means that they cannot be expanded.
- -- The Locked flag is used to enforce this restriction.
function Is_Empty return Boolean renames Tab.Is_Empty;
projects / gcc.git / commitdiff