Skip to content

R
riscv-gcc-1
Commit 27eaddda by Hristian Kirtchev Committed by Arnaud Charlet
Options

exp_util.adb, [...]: Minor reformatting and code cleanups. 

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

	* exp_util.adb, a-cfdlli.adb, a-cfdlli.ads, exp_ch9.adb, g-dyntab.adb,
	sem_dim.adb, a-cfinve.adb, a-cfinve.ads, a-cofove.adb, a-cofove.ads:
	Minor reformatting and code cleanups.

From-SVN: r247319
parent 6dd86c75
Showing with 169 additions and 188 deletions
gcc/ada/ChangeLog
2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* exp_util.adb, a-cfdlli.adb, a-cfdlli.ads, exp_ch9.adb, g-dyntab.adb,
sem_dim.adb, a-cfinve.adb, a-cfinve.ads, a-cofove.adb, a-cofove.ads:
Minor reformatting and code cleanups.
2017-04-27 Ed Schonberg <schonberg@adacore.com> 2017-04-27 Ed Schonberg <schonberg@adacore.com>
* freeze.adb (Build_Inherited_Condition_Pragmas): New procedure, * freeze.adb (Build_Inherited_Condition_Pragmas): New procedure,
......
gcc/ada/a-cfdlli.adb
...@@ -39,9 +39,7 @@ is ...@@ -39,9 +39,7 @@ is
New_Item : Element_Type; New_Item : Element_Type;
New_Node : out Count_Type); New_Node : out Count_Type);
procedure Free procedure Free (Container : in out List; X : Count_Type);
(Container : in out List;
X : Count_Type);
procedure Insert_Internal procedure Insert_Internal
(Container : in out List; (Container : in out List;
...@@ -109,10 +107,7 @@ is ...@@ -109,10 +107,7 @@ is
-- Append -- -- Append --
------------ ------------
procedure Append procedure Append (Container : in out List; New_Item : Element_Type) is
(Container : in out List;
New_Item : Element_Type)
is
begin begin
Insert (Container, No_Element, New_Item, 1); Insert (Container, No_Element, New_Item, 1);
end Append; end Append;
...@@ -430,9 +425,7 @@ is ...@@ -430,9 +425,7 @@ is
From := Container.First; From := Container.First;
end if; end if;
if Position.Node /= 0 and then if Position.Node /= 0 and then not Has_Element (Container, Position) then
not Has_Element (Container, Position)
then
raise Constraint_Error with "Position cursor has no element"; raise Constraint_Error with "Position cursor has no element";
end if; end if;
...@@ -496,33 +489,17 @@ is ...@@ -496,33 +489,17 @@ is
Left : M.Sequence; Left : M.Sequence;
Right : M.Sequence) return Boolean Right : M.Sequence) return Boolean
is is
begin Elem : Element_Type;
for I in 1 .. M.Length (Container) loop
declare
Found : Boolean := False;
J : Count_Type := 0;
begin begin
while not Found and J < M.Length (Left) loop for Index in 1 .. M.Length (Container) loop
J := J + 1; Elem := Element (Container, Index);
if Element (Container, I) = Element (Left, J) then
Found := True;
end if;
end loop;
J := 0; if not M.Contains (Left, 1, M.Length (Left), Elem)
and then not M.Contains (Right, 1, M.Length (Right), Elem)
while not Found and J < M.Length (Right) loop then
J := J + 1;
if Element (Container, I) = Element (Right, J) then
Found := True;
end if;
end loop;
if not Found then
return False; return False;
end if; end if;
end;
end loop; end loop;
return True; return True;
...@@ -579,8 +556,7 @@ is ...@@ -579,8 +556,7 @@ is
end if; end if;
for I in 1 .. L loop for I in 1 .. L loop
if Element (Left, I) /= Element (Right, L - I + 1) if Element (Left, I) /= Element (Right, L - I + 1) then
then
return False; return False;
end if; end if;
end loop; end loop;
...@@ -638,7 +614,7 @@ is ...@@ -638,7 +614,7 @@ is
end Model; end Model;
----------------------- -----------------------
-- Mapping_preserved -- -- Mapping_Preserved --
----------------------- -----------------------
function Mapping_Preserved function Mapping_Preserved
...@@ -748,7 +724,8 @@ is ...@@ -748,7 +724,8 @@ is
for C of Right loop for C of Right loop
if not P.Has_Key (Left, C) if not P.Has_Key (Left, C)
or else (C /= X and C /= Y or else (C /= X
and C /= Y
and P.Get (Left, C) /= P.Get (Right, C)) and P.Get (Left, C) /= P.Get (Right, C))
then then
return False; return False;
...@@ -933,8 +910,7 @@ is ...@@ -933,8 +910,7 @@ is
begin begin
if Target'Address = Source'Address then if Target'Address = Source'Address then
raise Program_Error with raise Program_Error with "Target and Source denote same container";
"Target and Source denote same container";
end if; end if;
LI := First (Target); LI := First (Target);
...@@ -1540,8 +1516,7 @@ is ...@@ -1540,8 +1516,7 @@ is
begin begin
if Target'Address = Source'Address then if Target'Address = Source'Address then
raise Program_Error with raise Program_Error with "Target and Source denote same container";
"Target and Source denote same container";
end if; end if;
if Before.Node /= 0 then if Before.Node /= 0 then
...@@ -1576,8 +1551,7 @@ is ...@@ -1576,8 +1551,7 @@ is
begin begin
if Target'Address = Source'Address then if Target'Address = Source'Address then
raise Program_Error with raise Program_Error with "Target and Source denote same container";
"Target and Source denote same container";
end if; end if;
if Position.Node = 0 then if Position.Node = 0 then
...@@ -1820,15 +1794,11 @@ is ...@@ -1820,15 +1794,11 @@ is
return False; return False;
end if; end if;
if N (Position.Node).Prev = 0 if N (Position.Node).Prev = 0 and then Position.Node /= L.First then
and then Position.Node /= L.First
then
return False; return False;
end if; end if;
if N (Position.Node).Next = 0 if N (Position.Node).Next = 0 and then Position.Node /= L.Last then
and then Position.Node /= L.Last
then
return False; return False;
end if; end if;
......
gcc/ada/a-cfdlli.ads
...@@ -992,7 +992,8 @@ is ...@@ -992,7 +992,8 @@ is
Pre => Has_Element (Container, I) and then Has_Element (Container, J), Pre => Has_Element (Container, I) and then Has_Element (Container, J),
Post => Post =>
M_Elements_Swapped M_Elements_Swapped
(Model (Container)'Old, Model (Container), (Model (Container)'Old,
Model (Container),
X => P.Get (Positions (Container)'Old, I), X => P.Get (Positions (Container)'Old, I),
Y => P.Get (Positions (Container)'Old, J)) Y => P.Get (Positions (Container)'Old, J))
...@@ -1007,7 +1008,8 @@ is ...@@ -1007,7 +1008,8 @@ is
Pre => Has_Element (Container, I) and then Has_Element (Container, J), Pre => Has_Element (Container, I) and then Has_Element (Container, J),
Post => Post =>
M_Elements_Swapped M_Elements_Swapped
(Model (Container'Old), Model (Container), (Model (Container'Old),
Model (Container),
X => P.Get (Positions (Container)'Old, I), X => P.Get (Positions (Container)'Old, I),
Y => P.Get (Positions (Container)'Old, J)) Y => P.Get (Positions (Container)'Old, J))
and P_Positions_Swapped and P_Positions_Swapped
...@@ -1088,7 +1090,8 @@ is ...@@ -1088,7 +1090,8 @@ is
and M_Elements_Included and M_Elements_Included
(Left => Model (Target), (Left => Model (Target),
L_Fst => P.Get (Positions (Target)'Old, Before), L_Fst => P.Get (Positions (Target)'Old, Before),
L_Lst => P.Get (Positions (Target)'Old, Before) - 1 + L_Lst =>
P.Get (Positions (Target)'Old, Before) - 1 +
Length (Source)'Old, Length (Source)'Old,
Right => Model (Source)'Old, Right => Model (Source)'Old,
R_Lst => Length (Source)'Old) R_Lst => Length (Source)'Old)
...@@ -1179,7 +1182,8 @@ is ...@@ -1179,7 +1182,8 @@ is
-- The element located at Position in Source is moved to Target -- The element located at Position in Source is moved to Target
and Element (Model (Target), P.Get (Positions (Target), Position)) = and Element (Model (Target),
P.Get (Positions (Target), Position)) =
Element (Model (Source)'Old, Element (Model (Source)'Old,
P.Get (Positions (Source)'Old, Position'Old)) P.Get (Positions (Source)'Old, Position'Old))
...@@ -1227,7 +1231,8 @@ is ...@@ -1227,7 +1231,8 @@ is
-- The last element of Container is the one that was previously at -- The last element of Container is the one that was previously at
-- Position. -- Position.
and Element (Model (Container), Length (Container)) = and Element (Model (Container),
Length (Container)) =
Element (Model (Container)'Old, Element (Model (Container)'Old,
P.Get (Positions (Container)'Old, Position)) P.Get (Positions (Container)'Old, Position))
...@@ -1285,9 +1290,11 @@ is ...@@ -1285,9 +1290,11 @@ is
-- The element previously at Position is now before Before -- The element previously at Position is now before Before
and Element (Model (Container), and Element
(Model (Container),
P.Get (Positions (Container)'Old, Before)) = P.Get (Positions (Container)'Old, Before)) =
Element (Model (Container)'Old, Element
(Model (Container)'Old,
P.Get (Positions (Container)'Old, Position)) P.Get (Positions (Container)'Old, Position))
-- Cursors from Container continue designating the same elements -- Cursors from Container continue designating the same elements
...@@ -1422,7 +1429,8 @@ is ...@@ -1422,7 +1429,8 @@ is
-- The element designated by the result of Find is Item -- The element designated by the result of Find is Item
and Element (Model (Container), and Element
(Model (Container),
P.Get (Positions (Container), Find'Result)) = Item P.Get (Positions (Container), Find'Result)) = Item
-- The result of Find is located after Position -- The result of Find is located after Position
...@@ -1476,9 +1484,9 @@ is ...@@ -1476,9 +1484,9 @@ is
-- The element designated by the result of Find is Item -- The element designated by the result of Find is Item
and Element (Model (Container), and Element
P.Get (Positions (Container), (Model (Container),
Reverse_Find'Result)) = Item P.Get (Positions (Container), Reverse_Find'Result)) = Item
-- The result of Find is located before Position -- The result of Find is located before Position
...@@ -1544,11 +1552,13 @@ is ...@@ -1544,11 +1552,13 @@ is
Post => Post =>
Length (Container) = Length (Container)'Old Length (Container) = Length (Container)'Old
and M_Elements_Sorted (Model (Container)) and M_Elements_Sorted (Model (Container))
and M_Elements_Included (Left => Model (Container)'Old, and M_Elements_Included
(Left => Model (Container)'Old,
L_Lst => Length (Container), L_Lst => Length (Container),
Right => Model (Container), Right => Model (Container),
R_Lst => Length (Container)) R_Lst => Length (Container))
and M_Elements_Included (Left => Model (Container), and M_Elements_Included
(Left => Model (Container),
L_Lst => Length (Container), L_Lst => Length (Container),
Right => Model (Container)'Old, Right => Model (Container)'Old,
R_Lst => Length (Container)); R_Lst => Length (Container));
...@@ -1562,16 +1572,20 @@ is ...@@ -1562,16 +1572,20 @@ is
and Length (Source) = 0 and Length (Source) = 0
and (if M_Elements_Sorted (Model (Target)'Old) and (if M_Elements_Sorted (Model (Target)'Old)
and M_Elements_Sorted (Model (Source)'Old) and M_Elements_Sorted (Model (Source)'Old)
then M_Elements_Sorted (Model (Target))) then
and M_Elements_Included (Left => Model (Target)'Old, M_Elements_Sorted (Model (Target)))
and M_Elements_Included
(Left => Model (Target)'Old,
L_Lst => Length (Target)'Old, L_Lst => Length (Target)'Old,
Right => Model (Target), Right => Model (Target),
R_Lst => Length (Target)) R_Lst => Length (Target))
and M_Elements_Included (Left => Model (Source)'Old, and M_Elements_Included
(Left => Model (Source)'Old,
L_Lst => Length (Source)'Old, L_Lst => Length (Source)'Old,
Right => Model (Target), Right => Model (Target),
R_Lst => Length (Target)) R_Lst => Length (Target))
and M_Elements_In_Union (Model (Target), and M_Elements_In_Union
(Model (Target),
Model (Source)'Old, Model (Source)'Old,
Model (Target)'Old); Model (Target)'Old);
end Generic_Sorting; end Generic_Sorting;
......
gcc/ada/a-cfinve.ads
...@@ -195,6 +195,7 @@ is ...@@ -195,6 +195,7 @@ is
I : Index_Type) return Element_Type renames M.Get; I : Index_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;
...@@ -213,7 +214,8 @@ is ...@@ -213,7 +214,8 @@ is
Global => null, Global => null,
Post => Post =>
Formal_Indefinite_Vectors.Length (To_Vector'Result) = Length Formal_Indefinite_Vectors.Length (To_Vector'Result) = Length
and M.Constant_Range (Container => Model (To_Vector'Result), and M.Constant_Range
(Container => Model (To_Vector'Result),
Fst => Index_Type'First, Fst => Index_Type'First,
Lst => Last_Index (To_Vector'Result), Lst => Last_Index (To_Vector'Result),
Item => New_Item); Item => New_Item);
...@@ -221,8 +223,11 @@ is ...@@ -221,8 +223,11 @@ is
function Capacity (Container : Vector) return Capacity_Range with function Capacity (Container : Vector) return Capacity_Range with
Global => null, Global => null,
Post => Post =>
Capacity'Result = (if Bounded then Container.Capacity Capacity'Result =
else Capacity_Range'Last); (if Bounded then
Container.Capacity
else
Capacity_Range'Last);
pragma Annotate (GNATprove, Inline_For_Proof, Capacity); pragma Annotate (GNATprove, Inline_For_Proof, Capacity);
procedure Reserve_Capacity procedure Reserve_Capacity
...@@ -257,8 +262,10 @@ is ...@@ -257,8 +262,10 @@ is
Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)), Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)),
Post => Post =>
Model (Copy'Result) = Model (Source) Model (Copy'Result) = Model (Source)
and (if Capacity = 0 then Copy'Result.Capacity = Length (Source) and (if Capacity = 0 then
else Copy'Result.Capacity = Capacity); Copy'Result.Capacity = Length (Source)
else
Copy'Result.Capacity = Capacity);
procedure Move (Target : in out Vector; Source : in out Vector) procedure Move (Target : in out Vector; Source : in out Vector)
with with
...@@ -411,10 +418,7 @@ is ...@@ -411,10 +418,7 @@ is
Lst => Last_Index (Container)'Old, Lst => Last_Index (Container)'Old,
Offset => Count); Offset => Count);
procedure Prepend procedure Prepend (Container : in out Vector; New_Item : Vector) with
(Container : in out Vector;
New_Item : Vector)
with
Global => null, Global => null,
Pre => Length (Container) <= Capacity (Container) - Length (New_Item), Pre => Length (Container) <= Capacity (Container) - Length (New_Item),
Post => Post =>
...@@ -437,10 +441,7 @@ is ...@@ -437,10 +441,7 @@ is
Lst => Last_Index (Container)'Old, Lst => Last_Index (Container)'Old,
Offset => Length (New_Item)); Offset => Length (New_Item));
procedure Prepend procedure Prepend (Container : in out Vector; New_Item : Element_Type) with
(Container : in out Vector;
New_Item : Element_Type)
with
Global => null, Global => null,
Pre => Length (Container) < Capacity (Container), Pre => Length (Container) < Capacity (Container),
Post => Post =>
...@@ -486,10 +487,7 @@ is ...@@ -486,10 +487,7 @@ is
Lst => Last_Index (Container)'Old, Lst => Last_Index (Container)'Old,
Offset => Count); Offset => Count);
procedure Append procedure Append (Container : in out Vector; New_Item : Vector) with
(Container : in out Vector;
New_Item : Vector)
with
Global => null, Global => null,
Pre => Pre =>
Length (Container) <= Capacity (Container) - Length (New_Item), Length (Container) <= Capacity (Container) - Length (New_Item),
...@@ -512,10 +510,7 @@ is ...@@ -512,10 +510,7 @@ is
Count_Type Count_Type
(Last_Index (Container)'Old - Index_Type'First + 1))); (Last_Index (Container)'Old - Index_Type'First + 1)));
procedure Append procedure Append (Container : in out Vector; New_Item : Element_Type) with
(Container : in out Vector;
New_Item : Element_Type)
with
Global => null, Global => null,
Pre => Length (Container) < Capacity (Container), Pre => Length (Container) < Capacity (Container),
Post => Post =>
...@@ -554,10 +549,7 @@ is ...@@ -554,10 +549,7 @@ is
Last_Index (Container)'Old + Index_Type'Base (Count), Last_Index (Container)'Old + Index_Type'Base (Count),
Item => New_Item)); Item => New_Item));
procedure Delete procedure Delete (Container : in out Vector; Index : Extended_Index) with
(Container : in out Vector;
Index : Extended_Index)
with
Global => null, Global => null,
Pre => Index in First_Index (Container) .. Last_Index (Container), Pre => Index in First_Index (Container) .. Last_Index (Container),
Post => Post =>
...@@ -619,9 +611,7 @@ is ...@@ -619,9 +611,7 @@ is
Lst => Last_Index (Container), Lst => Last_Index (Container),
Offset => Count)); Offset => Count));
procedure Delete_First procedure Delete_First (Container : in out Vector) with
(Container : in out Vector)
with
Global => null, Global => null,
Pre => Length (Container) > 0, Pre => Length (Container) > 0,
Post => Post =>
...@@ -636,10 +626,7 @@ is ...@@ -636,10 +626,7 @@ is
Lst => Last_Index (Container), Lst => Last_Index (Container),
Offset => 1); Offset => 1);
procedure Delete_First procedure Delete_First (Container : in out Vector; Count : Count_Type) with
(Container : in out Vector;
Count : Count_Type)
with
Global => null, Global => null,
Contract_Cases => Contract_Cases =>
...@@ -659,9 +646,7 @@ is ...@@ -659,9 +646,7 @@ is
Lst => Last_Index (Container), Lst => Last_Index (Container),
Offset => Count)); Offset => Count));
procedure Delete_Last procedure Delete_Last (Container : in out Vector) with
(Container : in out Vector)
with
Global => null, Global => null,
Pre => Length (Container) > 0, Pre => Length (Container) > 0,
Post => Post =>
...@@ -671,10 +656,7 @@ is ...@@ -671,10 +656,7 @@ is
and Model (Container) < Model (Container)'Old; and Model (Container) < Model (Container)'Old;
procedure Delete_Last procedure Delete_Last (Container : in out Vector; Count : Count_Type) with
(Container : in out Vector;
Count : Count_Type)
with
Global => null, Global => null,
Contract_Cases => Contract_Cases =>
...@@ -693,9 +675,14 @@ is ...@@ -693,9 +675,14 @@ is
Global => null, Global => null,
Post => M_Elements_Reversed (Model (Container)'Old, Model (Container)); Post => M_Elements_Reversed (Model (Container)'Old, Model (Container));
procedure Swap (Container : in out Vector; I, J : Index_Type) with procedure Swap
(Container : in out Vector;
I : Index_Type;
J : Index_Type)
with
Global => null, Global => null,
Pre => I in First_Index (Container) .. Last_Index (Container) Pre =>
I in First_Index (Container) .. Last_Index (Container)
and then J in First_Index (Container) .. Last_Index (Container), and then J in First_Index (Container) .. Last_Index (Container),
Post => Post =>
M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J); M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J);
...@@ -799,8 +786,10 @@ is ...@@ -799,8 +786,10 @@ is
(Container => Model (Container), (Container => Model (Container),
Fst => Reverse_Find_Index'Result + 1, Fst => Reverse_Find_Index'Result + 1,
Lst => Lst =>
(if Index <= Last_Index (Container) then Index (if Index <= Last_Index (Container) then
else Last_Index (Container)), Index
else
Last_Index (Container)),
Item => Item)); Item => Item));
function Contains function Contains
...@@ -809,7 +798,9 @@ is ...@@ -809,7 +798,9 @@ is
with with
Global => null, Global => null,
Post => Post =>
Contains'Result = M.Contains (Container => Model (Container), Contains'Result =
M.Contains
(Container => Model (Container),
Fst => Index_Type'First, Fst => Index_Type'First,
Lst => Last_Index (Container), Lst => Last_Index (Container),
Item => Item); Item => Item);
...@@ -847,11 +838,13 @@ is ...@@ -847,11 +838,13 @@ is
Post => Post =>
Length (Container) = Length (Container)'Old Length (Container) = Length (Container)'Old
and M_Elements_Sorted (Model (Container)) and M_Elements_Sorted (Model (Container))
and M_Elements_Included (Left => Model (Container)'Old, and M_Elements_Included
(Left => Model (Container)'Old,
L_Lst => Last_Index (Container), L_Lst => Last_Index (Container),
Right => Model (Container), Right => Model (Container),
R_Lst => Last_Index (Container)) R_Lst => Last_Index (Container))
and M_Elements_Included (Left => Model (Container), and M_Elements_Included
(Left => Model (Container),
L_Lst => Last_Index (Container), L_Lst => Last_Index (Container),
Right => Model (Container)'Old, Right => Model (Container)'Old,
R_Lst => Last_Index (Container)); R_Lst => Last_Index (Container));
...@@ -865,16 +858,20 @@ is ...@@ -865,16 +858,20 @@ is
and Length (Source) = 0 and Length (Source) = 0
and (if M_Elements_Sorted (Model (Target)'Old) and (if M_Elements_Sorted (Model (Target)'Old)
and M_Elements_Sorted (Model (Source)'Old) and M_Elements_Sorted (Model (Source)'Old)
then M_Elements_Sorted (Model (Target))) then
and M_Elements_Included (Left => Model (Target)'Old, M_Elements_Sorted (Model (Target)))
and M_Elements_Included
(Left => Model (Target)'Old,
L_Lst => Last_Index (Target)'Old, L_Lst => Last_Index (Target)'Old,
Right => Model (Target), Right => Model (Target),
R_Lst => Last_Index (Target)) R_Lst => Last_Index (Target))
and M_Elements_Included (Left => Model (Source)'Old, and M_Elements_Included
(Left => Model (Source)'Old,
L_Lst => Last_Index (Source)'Old, L_Lst => Last_Index (Source)'Old,
Right => Model (Target), Right => Model (Target),
R_Lst => Last_Index (Target)) R_Lst => Last_Index (Target))
and M_Elements_In_Union (Model (Target), and M_Elements_In_Union
(Model (Target),
Model (Source)'Old, Model (Source)'Old,
Model (Target)'Old); Model (Target)'Old);
end Generic_Sorting; end Generic_Sorting;
...@@ -904,9 +901,11 @@ private ...@@ -904,9 +901,11 @@ private
type Elements_Array_Ptr is access all Elements_Array; type Elements_Array_Ptr is access all Elements_Array;
type Vector (Capacity : Capacity_Range) is limited record type Vector (Capacity : Capacity_Range) is limited record
-- In the bounded case, the elements are stored in Elements. In the -- In the bounded case, the elements are stored in Elements. In the
-- unbounded case, the elements are initially stored in Elements, until -- unbounded case, the elements are initially stored in Elements, until
-- we run out of room, then we switch to Elements_Ptr. -- we run out of room, then we switch to Elements_Ptr.
Last : Extended_Index := No_Index; Last : Extended_Index := No_Index;
Elements_Ptr : Elements_Array_Ptr := null; Elements_Ptr : Elements_Array_Ptr := null;
Elements : aliased Elements_Array (1 .. Capacity); Elements : aliased Elements_Array (1 .. Capacity);
......
gcc/ada/a-cofove.ads
...@@ -189,6 +189,7 @@ is ...@@ -189,6 +189,7 @@ is
I : Index_Type) return Element_Type renames M.Get; I : Index_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;
...@@ -207,7 +208,8 @@ is ...@@ -207,7 +208,8 @@ is
Global => null, Global => null,
Post => Post =>
Formal_Vectors.Length (To_Vector'Result) = Length Formal_Vectors.Length (To_Vector'Result) = Length
and M.Constant_Range (Container => Model (To_Vector'Result), and M.Constant_Range
(Container => Model (To_Vector'Result),
Fst => Index_Type'First, Fst => Index_Type'First,
Lst => Last_Index (To_Vector'Result), Lst => Last_Index (To_Vector'Result),
Item => New_Item); Item => New_Item);
...@@ -215,8 +217,11 @@ is ...@@ -215,8 +217,11 @@ is
function Capacity (Container : Vector) return Capacity_Range with function Capacity (Container : Vector) return Capacity_Range with
Global => null, Global => null,
Post => Post =>
Capacity'Result = (if Bounded then Container.Capacity Capacity'Result =
else Capacity_Range'Last); (if Bounded then
Container.Capacity
else
Capacity_Range'Last);
pragma Annotate (GNATprove, Inline_For_Proof, Capacity); pragma Annotate (GNATprove, Inline_For_Proof, Capacity);
procedure Reserve_Capacity procedure Reserve_Capacity
...@@ -251,8 +256,10 @@ is ...@@ -251,8 +256,10 @@ is
Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)), Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)),
Post => Post =>
Model (Copy'Result) = Model (Source) Model (Copy'Result) = Model (Source)
and (if Capacity = 0 then Copy'Result.Capacity = Length (Source) and (if Capacity = 0 then
else Copy'Result.Capacity = Capacity); Copy'Result.Capacity = Length (Source)
else
Copy'Result.Capacity = Capacity);
procedure Move (Target : in out Vector; Source : in out Vector) procedure Move (Target : in out Vector; Source : in out Vector)
with with
...@@ -405,10 +412,7 @@ is ...@@ -405,10 +412,7 @@ is
Lst => Last_Index (Container)'Old, Lst => Last_Index (Container)'Old,
Offset => Count); Offset => Count);
procedure Prepend procedure Prepend (Container : in out Vector; New_Item : Vector) with
(Container : in out Vector;
New_Item : Vector)
with
Global => null, Global => null,
Pre => Length (Container) <= Capacity (Container) - Length (New_Item), Pre => Length (Container) <= Capacity (Container) - Length (New_Item),
Post => Post =>
...@@ -431,10 +435,7 @@ is ...@@ -431,10 +435,7 @@ is
Lst => Last_Index (Container)'Old, Lst => Last_Index (Container)'Old,
Offset => Length (New_Item)); Offset => Length (New_Item));
procedure Prepend procedure Prepend (Container : in out Vector; New_Item : Element_Type) with
(Container : in out Vector;
New_Item : Element_Type)
with
Global => null, Global => null,
Pre => Length (Container) < Capacity (Container), Pre => Length (Container) < Capacity (Container),
Post => Post =>
...@@ -480,10 +481,7 @@ is ...@@ -480,10 +481,7 @@ is
Lst => Last_Index (Container)'Old, Lst => Last_Index (Container)'Old,
Offset => Count); Offset => Count);
procedure Append procedure Append (Container : in out Vector; New_Item : Vector) with
(Container : in out Vector;
New_Item : Vector)
with
Global => null, Global => null,
Pre => Pre =>
Length (Container) <= Capacity (Container) - Length (New_Item), Length (Container) <= Capacity (Container) - Length (New_Item),
...@@ -506,10 +504,7 @@ is ...@@ -506,10 +504,7 @@ is
Count_Type Count_Type
(Last_Index (Container)'Old - Index_Type'First + 1))); (Last_Index (Container)'Old - Index_Type'First + 1)));
procedure Append procedure Append (Container : in out Vector; New_Item : Element_Type) with
(Container : in out Vector;
New_Item : Element_Type)
with
Global => null, Global => null,
Pre => Length (Container) < Capacity (Container), Pre => Length (Container) < Capacity (Container),
Post => Post =>
...@@ -548,10 +543,7 @@ is ...@@ -548,10 +543,7 @@ is
Last_Index (Container)'Old + Index_Type'Base (Count), Last_Index (Container)'Old + Index_Type'Base (Count),
Item => New_Item)); Item => New_Item));
procedure Delete procedure Delete (Container : in out Vector; Index : Extended_Index) with
(Container : in out Vector;
Index : Extended_Index)
with
Global => null, Global => null,
Pre => Index in First_Index (Container) .. Last_Index (Container), Pre => Index in First_Index (Container) .. Last_Index (Container),
Post => Post =>
...@@ -613,9 +605,7 @@ is ...@@ -613,9 +605,7 @@ is
Lst => Last_Index (Container), Lst => Last_Index (Container),
Offset => Count)); Offset => Count));
procedure Delete_First procedure Delete_First (Container : in out Vector) with
(Container : in out Vector)
with
Global => null, Global => null,
Pre => Length (Container) > 0, Pre => Length (Container) > 0,
Post => Post =>
...@@ -630,10 +620,7 @@ is ...@@ -630,10 +620,7 @@ is
Lst => Last_Index (Container), Lst => Last_Index (Container),
Offset => 1); Offset => 1);
procedure Delete_First procedure Delete_First (Container : in out Vector; Count : Count_Type) with
(Container : in out Vector;
Count : Count_Type)
with
Global => null, Global => null,
Contract_Cases => Contract_Cases =>
...@@ -653,9 +640,7 @@ is ...@@ -653,9 +640,7 @@ is
Lst => Last_Index (Container), Lst => Last_Index (Container),
Offset => Count)); Offset => Count));
procedure Delete_Last procedure Delete_Last (Container : in out Vector) with
(Container : in out Vector)
with
Global => null, Global => null,
Pre => Length (Container) > 0, Pre => Length (Container) > 0,
Post => Post =>
...@@ -665,10 +650,7 @@ is ...@@ -665,10 +650,7 @@ is
and Model (Container) < Model (Container)'Old; and Model (Container) < Model (Container)'Old;
procedure Delete_Last procedure Delete_Last (Container : in out Vector; Count : Count_Type) with
(Container : in out Vector;
Count : Count_Type)
with
Global => null, Global => null,
Contract_Cases => Contract_Cases =>
...@@ -687,9 +669,14 @@ is ...@@ -687,9 +669,14 @@ is
Global => null, Global => null,
Post => M_Elements_Reversed (Model (Container)'Old, Model (Container)); Post => M_Elements_Reversed (Model (Container)'Old, Model (Container));
procedure Swap (Container : in out Vector; I, J : Index_Type) with procedure Swap
(Container : in out Vector;
I : Index_Type;
J : Index_Type)
with
Global => null, Global => null,
Pre => I in First_Index (Container) .. Last_Index (Container) Pre =>
I in First_Index (Container) .. Last_Index (Container)
and then J in First_Index (Container) .. Last_Index (Container), and then J in First_Index (Container) .. Last_Index (Container),
Post => Post =>
M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J); M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J);
...@@ -793,8 +780,10 @@ is ...@@ -793,8 +780,10 @@ is
(Container => Model (Container), (Container => Model (Container),
Fst => Reverse_Find_Index'Result + 1, Fst => Reverse_Find_Index'Result + 1,
Lst => Lst =>
(if Index <= Last_Index (Container) then Index (if Index <= Last_Index (Container) then
else Last_Index (Container)), Index
else
Last_Index (Container)),
Item => Item)); Item => Item));
function Contains function Contains
...@@ -803,7 +792,9 @@ is ...@@ -803,7 +792,9 @@ is
with with
Global => null, Global => null,
Post => Post =>
Contains'Result = M.Contains (Container => Model (Container), Contains'Result =
M.Contains
(Container => Model (Container),
Fst => Index_Type'First, Fst => Index_Type'First,
Lst => Last_Index (Container), Lst => Last_Index (Container),
Item => Item); Item => Item);
...@@ -841,11 +832,13 @@ is ...@@ -841,11 +832,13 @@ is
Post => Post =>
Length (Container) = Length (Container)'Old Length (Container) = Length (Container)'Old
and M_Elements_Sorted (Model (Container)) and M_Elements_Sorted (Model (Container))
and M_Elements_Included (Left => Model (Container)'Old, and M_Elements_Included
(Left => Model (Container)'Old,
L_Lst => Last_Index (Container), L_Lst => Last_Index (Container),
Right => Model (Container), Right => Model (Container),
R_Lst => Last_Index (Container)) R_Lst => Last_Index (Container))
and M_Elements_Included (Left => Model (Container), and M_Elements_Included
(Left => Model (Container),
L_Lst => Last_Index (Container), L_Lst => Last_Index (Container),
Right => Model (Container)'Old, Right => Model (Container)'Old,
R_Lst => Last_Index (Container)); R_Lst => Last_Index (Container));
...@@ -859,16 +852,20 @@ is ...@@ -859,16 +852,20 @@ is
and Length (Source) = 0 and Length (Source) = 0
and (if M_Elements_Sorted (Model (Target)'Old) and (if M_Elements_Sorted (Model (Target)'Old)
and M_Elements_Sorted (Model (Source)'Old) and M_Elements_Sorted (Model (Source)'Old)
then M_Elements_Sorted (Model (Target))) then
and M_Elements_Included (Left => Model (Target)'Old, M_Elements_Sorted (Model (Target)))
and M_Elements_Included
(Left => Model (Target)'Old,
L_Lst => Last_Index (Target)'Old, L_Lst => Last_Index (Target)'Old,
Right => Model (Target), Right => Model (Target),
R_Lst => Last_Index (Target)) R_Lst => Last_Index (Target))
and M_Elements_Included (Left => Model (Source)'Old, and M_Elements_Included
(Left => Model (Source)'Old,
L_Lst => Last_Index (Source)'Old, L_Lst => Last_Index (Source)'Old,
Right => Model (Target), Right => Model (Target),
R_Lst => Last_Index (Target)) R_Lst => Last_Index (Target))
and M_Elements_In_Union (Model (Target), and M_Elements_In_Union
(Model (Target),
Model (Source)'Old, Model (Source)'Old,
Model (Target)'Old); Model (Target)'Old);
end Generic_Sorting; end Generic_Sorting;
...@@ -891,9 +888,11 @@ private ...@@ -891,9 +888,11 @@ private
type Elements_Array_Ptr is access all Elements_Array; type Elements_Array_Ptr is access all Elements_Array;
type Vector (Capacity : Capacity_Range) is limited record type Vector (Capacity : Capacity_Range) is limited record
-- In the bounded case, the elements are stored in Elements. In the -- In the bounded case, the elements are stored in Elements. In the
-- unbounded case, the elements are initially stored in Elements, until -- unbounded case, the elements are initially stored in Elements, until
-- we run out of room, then we switch to Elements_Ptr. -- we run out of room, then we switch to Elements_Ptr.
Last : Extended_Index := No_Index; Last : Extended_Index := No_Index;
Elements_Ptr : Elements_Array_Ptr := null; Elements_Ptr : Elements_Array_Ptr := null;
Elements : aliased Elements_Array (1 .. Capacity); Elements : aliased Elements_Array (1 .. Capacity);
......
gcc/ada/exp_ch9.adb
...@@ -7509,21 +7509,16 @@ package body Exp_Ch9 is ...@@ -7509,21 +7509,16 @@ package body Exp_Ch9 is
Cancel_Param := Make_Defining_Identifier (Loc, Name_uC); Cancel_Param := Make_Defining_Identifier (Loc, Name_uC);
-- Insert declaration of C in declarations of existing block -- Insert the declaration of C in the declarations of the existing
-- block. The variable is initialized to something (True or False,
-- does not matter) to prevent CodePeer from complaining about a
-- possible read of an uninitialized variable.
Prepend_To (Decls, Prepend_To (Decls,
Make_Object_Declaration (Loc, Make_Object_Declaration (Loc,
Defining_Identifier => Cancel_Param, Defining_Identifier => Cancel_Param,
Object_Definition => Object_Definition => New_Occurrence_Of (Standard_Boolean, Loc),
New_Occurrence_Of (Standard_Boolean, Loc), Expression => New_Occurrence_Of (Standard_False, Loc),
Expression =>
New_Occurrence_Of (Standard_False, Loc),
-- True would work equally well here. This initialization
-- should be dead, but only because of things (e.g.,
-- abortion deferral) that CodePeer doesn't know about.
-- We want to avoid CodePeer complaints about a possible read
-- of an uninitialized variable when this variable is read,
-- so we initialize it here.
Has_Init_Expression => True)); Has_Init_Expression => True));
-- Remove and save the call to Call_Simple -- Remove and save the call to Call_Simple
......
gcc/ada/exp_util.adb
...@@ -1114,13 +1114,11 @@ package body Exp_Util is ...@@ -1114,13 +1114,11 @@ package body Exp_Util is
if Present (New_E) then if Present (New_E) then
Rewrite (N, New_Occurrence_Of (New_E, Sloc (N))); Rewrite (N, New_Occurrence_Of (New_E, Sloc (N)));
-- If the entity is an overridden primitive and we are not -- If the entity is an overridden primitive and we are not in
-- in proof mode, we must build a wrapper for the current -- GNATprove mode, we must build a wrapper for the current
-- inherited operation. -- inherited operation.
if Is_Subprogram (New_E) if Is_Subprogram (New_E) and then not GNATprove_Mode then
and then not GNATprove_Mode
then
Needs_Wrapper := True; Needs_Wrapper := True;
end if; end if;
end if; end if;
......
gcc/ada/sem_dim.adb
...@@ -2154,9 +2154,9 @@ package body Sem_Dim is ...@@ -2154,9 +2154,9 @@ package body Sem_Dim is
if Dim_Of_Expr /= Dim_Of_Etyp then if Dim_Of_Expr /= Dim_Of_Etyp then
-- Numeric literal case. Issue a warning if the object type is not -- Numeric literal case. Issue a warning if the object type is
-- dimensionless to indicate the literal is treated as if its -- not dimensionless to indicate the literal is treated as if
-- dimension matches the type dimension. -- its dimension matches the type dimension.
if Nkind_In (Original_Node (Expr), N_Real_Literal, if Nkind_In (Original_Node (Expr), N_Real_Literal,
N_Integer_Literal) N_Integer_Literal)
...@@ -2171,8 +2171,8 @@ package body Sem_Dim is ...@@ -2171,8 +2171,8 @@ package body Sem_Dim is
Set_Dimensions (Id, Dim_Of_Expr); Set_Dimensions (Id, Dim_Of_Expr);
-- Expression may have been constant-folded. If nominal type -- Expression may have been constant-folded. If nominal type has
-- has dimensions, verify that expression has same type. -- dimensions, verify that expression has same type.
elsif Exists (Dim_Of_Etyp) and then Etype (Expr) = Etyp then elsif Exists (Dim_Of_Etyp) and then Etype (Expr) = Etyp then
null; null;
...@@ -2184,8 +2184,8 @@ package body Sem_Dim is ...@@ -2184,8 +2184,8 @@ package body Sem_Dim is
end if; end if;
end if; end if;
-- Remove dimensions in expression after checking consistency -- Remove dimensions in expression after checking consistency with
-- with given type. -- given type.
Remove_Dimensions (Expr); Remove_Dimensions (Expr);
end if; end if;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment