Commit e77e2429 by Arnaud Charlet

[multiple changes]

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

	* exp_prag.adb, a-cofuse.adb, a-cofuse.ads, einfo.adb, sem_prag.adb,
	cstand.adb, par-prag.adb, a-cofuve.adb, a-cofuve.ads, a-cofuma.adb,
	a-cofuma.ads, a-cofuba.adb, a-cofuba.ads: Minor reformatting.

2017-04-27  Tristan Gingold  <gingold@adacore.com>

	* s-excmac-gcc.ads, s-excmac-gcc.adb,
	s-excmac-arm.ads, s-excmac-arm.adb (New_Occurrence): Rewrite it in
	Ada95.

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

	* exp_ch7.adb (Establish_Transient_Scope): Rewrite
	the loop which detects potential enclosing transient scopes. The
	loop now terminates much earlier as transient scopes are bounded
	by packages and subprograms.

2017-04-27  Claire Dross  <dross@adacore.com>

	* a-cfdlli.adb, a-cfdlli.ads (=): Generic parameter removed to
	allow the use of regular equality over elements in contracts.
	(Cursor): Type is now public so that it can be used in
	model functions.
	(Formal_Model): Ghost package containing
	model functions that are used in subprogram contracts.
	(Current_To_Last): Removed, model functions should be used
	instead.
	(First_To_Previous): Removed, model functions should
	be used instead.
	(Strict_Equal): Removed, model functions
	should be used instead.
	(Append): Default parameter value
	replaced by new wrapper to allow more precise contracts.
	(Insert): Default parameter value replaced by new wrapper to
	allow more precise contracts.
	(Delete): Default parameter
	value replaced by new wrapper to allow more precise contracts.
	(Prepend): Default parameter value replaced by new wrapper to
	allow more precise contracts.
	(Delete_First): Default parameter
	value replaced by new wrapper to allow more precise contracts.
	(Delete_Last): Default parameter value replaced by new wrapper
	to allow more precise contracts.

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

	* exp_spark.adb (Expand_SPARK): Perform specialized expansion
	for object declarations.
	(Expand_SPARK_N_Object_Declaration): New routine.
	* sem_elab.adb (Check_A_Call): Include calls to the
	Default_Initial_Condition procedure of a type under the SPARK
	elaboration checks umbrella.

From-SVN: r247299
parent 7a71a7c4
2017-04-27 Hristian Kirtchev <kirtchev@adacore.com> 2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* exp_prag.adb, a-cofuse.adb, a-cofuse.ads, einfo.adb, sem_prag.adb,
cstand.adb, par-prag.adb, a-cofuve.adb, a-cofuve.ads, a-cofuma.adb,
a-cofuma.ads, a-cofuba.adb, a-cofuba.ads: Minor reformatting.
2017-04-27 Tristan Gingold <gingold@adacore.com>
* s-excmac-gcc.ads, s-excmac-gcc.adb,
s-excmac-arm.ads, s-excmac-arm.adb (New_Occurrence): Rewrite it in
Ada95.
2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch7.adb (Establish_Transient_Scope): Rewrite
the loop which detects potential enclosing transient scopes. The
loop now terminates much earlier as transient scopes are bounded
by packages and subprograms.
2017-04-27 Claire Dross <dross@adacore.com>
* a-cfdlli.adb, a-cfdlli.ads (=): Generic parameter removed to
allow the use of regular equality over elements in contracts.
(Cursor): Type is now public so that it can be used in
model functions.
(Formal_Model): Ghost package containing
model functions that are used in subprogram contracts.
(Current_To_Last): Removed, model functions should be used
instead.
(First_To_Previous): Removed, model functions should
be used instead.
(Strict_Equal): Removed, model functions
should be used instead.
(Append): Default parameter value
replaced by new wrapper to allow more precise contracts.
(Insert): Default parameter value replaced by new wrapper to
allow more precise contracts.
(Delete): Default parameter
value replaced by new wrapper to allow more precise contracts.
(Prepend): Default parameter value replaced by new wrapper to
allow more precise contracts.
(Delete_First): Default parameter
value replaced by new wrapper to allow more precise contracts.
(Delete_Last): Default parameter value replaced by new wrapper
to allow more precise contracts.
2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* exp_spark.adb (Expand_SPARK): Perform specialized expansion
for object declarations.
(Expand_SPARK_N_Object_Declaration): New routine.
* sem_elab.adb (Check_A_Call): Include calls to the
Default_Initial_Condition procedure of a type under the SPARK
elaboration checks umbrella.
2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* sem.adb (Analyze): Diagnose an illegal iterated component * sem.adb (Analyze): Diagnose an illegal iterated component
association. association.
* sem_util.ads, sem_util.adb * sem_util.ads, sem_util.adb
......
...@@ -35,11 +35,12 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -35,11 +35,12 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
function To_Count (Idx : Extended_Index) return Count_Type function To_Count (Idx : Extended_Index) return Count_Type
is (Count_Type is (Count_Type
(Extended_Index'Pos (Idx) (Extended_Index'Pos (Idx) -
- Extended_Index'Pos (Extended_Index'First))); Extended_Index'Pos (Extended_Index'First)));
function To_Index (Position : Count_Type) return Extended_Index function To_Index (Position : Count_Type) return Extended_Index
is (Extended_Index'Val is (Extended_Index'Val
(Position + Extended_Index'Pos (Extended_Index'First))); (Position + Extended_Index'Pos (Extended_Index'First)));
-- Conversion functions between Index_Type and Count_Type -- Conversion functions between Index_Type and Count_Type
function Find (C : Container; E : access Element_Type) return Count_Type; function Find (C : Container; E : access Element_Type) return Count_Type;
...@@ -50,7 +51,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -50,7 +51,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
-- "=" -- -- "=" --
--------- ---------
function "=" (C1, C2 : Container) return Boolean is function "=" (C1 : Container; C2 : Container) return Boolean is
begin begin
if C1.Elements'Length /= C2.Elements'Length then if C1.Elements'Length /= C2.Elements'Length then
return False; return False;
...@@ -61,6 +62,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -61,6 +62,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
return False; return False;
end if; end if;
end loop; end loop;
return True; return True;
end "="; end "=";
...@@ -68,13 +70,14 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -68,13 +70,14 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
-- "<=" -- -- "<=" --
---------- ----------
function "<=" (C1, C2 : Container) return Boolean is function "<=" (C1 : Container; C2 : Container) return Boolean is
begin begin
for I in C1.Elements'Range loop for I in C1.Elements'Range loop
if Find (C2, C1.Elements (I)) = 0 then if Find (C2, C1.Elements (I)) = 0 then
return False; return False;
end if; end if;
end loop; end loop;
return True; return True;
end "<="; end "<=";
...@@ -90,6 +93,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -90,6 +93,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
A : constant Element_Array_Access := A : constant Element_Array_Access :=
new Element_Array'(1 .. C.Elements'Last + 1 => <>); new Element_Array'(1 .. C.Elements'Last + 1 => <>);
P : Count_Type := 0; P : Count_Type := 0;
begin begin
for J in 1 .. C.Elements'Last + 1 loop for J in 1 .. C.Elements'Last + 1 loop
if J /= To_Count (I) then if J /= To_Count (I) then
...@@ -99,6 +103,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -99,6 +103,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
A (J) := new Element_Type'(E); A (J) := new Element_Type'(E);
end if; end if;
end loop; end loop;
return Container'(Elements => A); return Container'(Elements => A);
end Add; end Add;
...@@ -113,6 +118,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -113,6 +118,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
return I; return I;
end if; end if;
end loop; end loop;
return 0; return 0;
end Find; end Find;
...@@ -130,10 +136,11 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -130,10 +136,11 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
-- Intersection -- -- Intersection --
------------------ ------------------
function Intersection (C1, C2 : Container) return Container is function Intersection (C1 : Container; C2 : Container) return Container is
A : constant Element_Array_Access := A : constant Element_Array_Access :=
new Element_Array'(1 .. Num_Overlaps (C1, C2) => <>); new Element_Array'(1 .. Num_Overlaps (C1, C2) => <>);
P : Count_Type := 0; P : Count_Type := 0;
begin begin
for I in C1.Elements'Range loop for I in C1.Elements'Range loop
if Find (C2, C1.Elements (I)) > 0 then if Find (C2, C1.Elements (I)) > 0 then
...@@ -141,6 +148,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -141,6 +148,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
A (P) := C1.Elements (I); A (P) := C1.Elements (I);
end if; end if;
end loop; end loop;
return Container'(Elements => A); return Container'(Elements => A);
end Intersection; end Intersection;
...@@ -154,14 +162,16 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -154,14 +162,16 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
-- Num_Overlaps -- -- Num_Overlaps --
--------------------- ---------------------
function Num_Overlaps (C1, C2 : Container) return Count_Type is function Num_Overlaps (C1 : Container; C2 : Container) return Count_Type is
P : Count_Type := 0; P : Count_Type := 0;
begin begin
for I in C1.Elements'Range loop for I in C1.Elements'Range loop
if Find (C2, C1.Elements (I)) > 0 then if Find (C2, C1.Elements (I)) > 0 then
P := P + 1; P := P + 1;
end if; end if;
end loop; end loop;
return P; return P;
end Num_Overlaps; end Num_Overlaps;
...@@ -173,6 +183,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -173,6 +183,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
A : constant Element_Array_Access := A : constant Element_Array_Access :=
new Element_Array'(1 .. C.Elements'Last - 1 => <>); new Element_Array'(1 .. C.Elements'Last - 1 => <>);
P : Count_Type := 0; P : Count_Type := 0;
begin begin
for J in C.Elements'Range loop for J in C.Elements'Range loop
if J /= To_Count (I) then if J /= To_Count (I) then
...@@ -180,6 +191,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -180,6 +191,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
A (P) := C.Elements (J); A (P) := C.Elements (J);
end if; end if;
end loop; end loop;
return Container'(Elements => A); return Container'(Elements => A);
end Remove; end Remove;
...@@ -187,11 +199,14 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -187,11 +199,14 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
-- Set -- -- Set --
--------- ---------
function Set (C : Container; I : Index_Type; E : Element_Type) function Set
return Container (C : Container;
I : Index_Type;
E : Element_Type) return Container
is is
Result : constant Container := Result : constant Container :=
Container'(Elements => new Element_Array'(C.Elements.all)); Container'(Elements => new Element_Array'(C.Elements.all));
begin begin
Result.Elements (To_Count (I)) := new Element_Type'(E); Result.Elements (To_Count (I)) := new Element_Type'(E);
return Result; return Result;
...@@ -201,7 +216,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -201,7 +216,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
-- Union -- -- Union --
----------- -----------
function Union (C1, C2 : Container) return Container is function Union (C1 : Container; C2 : Container) return Container is
N : constant Count_Type := Num_Overlaps (C1, C2); N : constant Count_Type := Num_Overlaps (C1, C2);
begin begin
...@@ -216,8 +231,10 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -216,8 +231,10 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
declare declare
L : constant Count_Type := Length (C1) - N + Length (C2); L : constant Count_Type := Length (C1) - N + Length (C2);
A : constant Element_Array_Access := A : constant Element_Array_Access :=
new Element_Array'(C1.Elements.all & (Length (C1) + 1 .. L => <>)); new Element_Array'
(C1.Elements.all & (Length (C1) + 1 .. L => <>));
P : Count_Type := Length (C1); P : Count_Type := Length (C1);
begin begin
for I in C2.Elements'Range loop for I in C2.Elements'Range loop
if Find (C1, C2.Elements (I)) = 0 then if Find (C1, C2.Elements (I)) = 0 then
...@@ -225,6 +242,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -225,6 +242,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
A (P) := C2.Elements (I); A (P) := C2.Elements (I);
end if; end if;
end loop; end loop;
return Container'(Elements => A); return Container'(Elements => A);
end; end;
end Union; end Union;
......
...@@ -41,6 +41,7 @@ private generic ...@@ -41,6 +41,7 @@ private generic
type Element_Type (<>) is private; type Element_Type (<>) is private;
with function "=" (Left, Right : Element_Type) return Boolean is <>; with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Functional_Base with SPARK_Mode => Off is package Ada.Containers.Functional_Base with SPARK_Mode => Off is
subtype Extended_Index is Index_Type'Base range subtype Extended_Index is Index_Type'Base range
...@@ -48,7 +49,7 @@ package Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -48,7 +49,7 @@ package Ada.Containers.Functional_Base with SPARK_Mode => Off is
type Container is private; type Container is private;
function "=" (C1, C2 : Container) return Boolean; function "=" (C1 : Container; C2 : Container) return Boolean;
-- Return True if C1 and C2 contain the same elements at the same position -- Return True if C1 and C2 contain the same elements at the same position
function Length (C : Container) return Count_Type; function Length (C : Container) return Count_Type;
...@@ -57,8 +58,10 @@ package Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -57,8 +58,10 @@ package Ada.Containers.Functional_Base with SPARK_Mode => Off is
function Get (C : Container; I : Index_Type) return Element_Type; function Get (C : Container; I : Index_Type) return Element_Type;
-- Access to the element at index I in C -- Access to the element at index I in C
function Set (C : Container; I : Index_Type; E : Element_Type) function Set
return Container; (C : Container;
I : Index_Type;
E : Element_Type) return Container;
-- Return a new container which is equal to C except for the element at -- Return a new container which is equal to C except for the element at
-- index I, which is set to E. -- index I, which is set to E.
...@@ -79,17 +82,17 @@ package Ada.Containers.Functional_Base with SPARK_Mode => Off is ...@@ -79,17 +82,17 @@ package Ada.Containers.Functional_Base with SPARK_Mode => Off is
-- Set Operations -- -- Set Operations --
-------------------- --------------------
function "<=" (C1, C2 : Container) return Boolean; function "<=" (C1 : Container; C2 : Container) return Boolean;
-- Return True if every element of C1 is in C2 -- Return True if every element of C1 is in C2
function Num_Overlaps (C1, C2 : Container) return Count_Type; function Num_Overlaps (C1 : Container; C2 : Container) return Count_Type;
-- Return the number of elements that are in both C1 and C2 -- Return the number of elements that are in both C1 and C2
function Union (C1, C2 : Container) return Container; function Union (C1 : Container; C2 : Container) return Container;
-- Return a container which is C1 plus all the elements of C2 that are not -- Return a container which is C1 plus all the elements of C2 that are not
-- in C1. -- in C1.
function Intersection (C1, C2 : Container) return Container; function Intersection (C1 : Container; C2 : Container) return Container;
-- Return a container which is C1 minus all the elements that are also in -- Return a container which is C1 minus all the elements that are also in
-- C2. -- C2.
......
...@@ -38,15 +38,16 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is ...@@ -38,15 +38,16 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
-- "=" -- -- "=" --
--------- ---------
function "=" (M1, M2 : Map) return Boolean is function "=" (M1 : Map; M2 : Map) return Boolean is
(M1.Keys <= M2.Keys and M2 <= M1); (M1.Keys <= M2.Keys and M2 <= M1);
---------- ----------
-- "<=" -- -- "<=" --
---------- ----------
function "<=" (M1, M2 : Map) return Boolean is function "<=" (M1 : Map; M2 : Map) return Boolean is
I2 : Count_Type; I2 : Count_Type;
begin begin
for I1 in 1 .. Length (M1.Keys) loop for I1 in 1 .. Length (M1.Keys) loop
I2 := Find (M2.Keys, Get (M1.Keys, I1)); I2 := Find (M2.Keys, Get (M1.Keys, I1));
...@@ -84,7 +85,10 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is ...@@ -84,7 +85,10 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
------------ ------------
function Is_Add function Is_Add
(M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean (M : Map;
K : Key_Type;
E : Element_Type;
Result : Map) return Boolean
is is
begin begin
if Mem (M, K) or not Mem (Result, K) or Get (Result, K) /= E then if Mem (M, K) or not Mem (Result, K) or Get (Result, K) /= E then
...@@ -120,16 +124,19 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is ...@@ -120,16 +124,19 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
------------ ------------
function Is_Set function Is_Set
(M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean (M : Map;
K : Key_Type;
E : Element_Type;
Result : Map) return Boolean
is is
(Mem (M, K) (Mem (M, K)
and then Mem (Result, K) and then Mem (Result, K)
and then Get (Result, K) = E and then Get (Result, K) = E
and then (for all KK of M => Mem (Result, KK) and then (for all KK of M =>
and then Mem (Result, KK)
(if K /= KK and then
then Get (Result, KK) = Get (M, KK))) (if K /= KK then Get (Result, KK) = Get (M, KK)))
and then (for all K of Result => Mem (M, K))); and then (for all K of Result => Mem (M, K)));
------------ ------------
-- Length -- -- Length --
...@@ -155,4 +162,5 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is ...@@ -155,4 +162,5 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
function Set (M : Map; K : Key_Type; E : Element_Type) return Map is function Set (M : Map; K : Key_Type; E : Element_Type) return Map is
(Keys => M.Keys, Elements => Set (M.Elements, Find (M.Keys, K), E)); (Keys => M.Keys, Elements => Set (M.Elements, Find (M.Keys, K), E));
end Ada.Containers.Functional_Maps; end Ada.Containers.Functional_Maps;
...@@ -37,6 +37,7 @@ generic ...@@ -37,6 +37,7 @@ generic
type Element_Type (<>) is private; type Element_Type (<>) is private;
with function Equivalent_Keys (Left, Right : Key_Type) return Boolean; with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
with function "=" (Left, Right : Element_Type) return Boolean is <>; with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Functional_Maps with SPARK_Mode is package Ada.Containers.Functional_Maps with SPARK_Mode is
pragma Assertion_Policy (Post => Ignore); pragma Assertion_Policy (Post => Ignore);
...@@ -58,6 +59,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is ...@@ -58,6 +59,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
function Mem (M : Map; K : Key_Type) return Boolean with function Mem (M : Map; K : Key_Type) return Boolean with
Global => null; Global => null;
function Get (M : Map; K : Key_Type) return Element_Type with function Get (M : Map; K : Key_Type) return Element_Type with
Global => null, Global => null,
Pre => Mem (M, K); Pre => Mem (M, K);
...@@ -65,21 +67,21 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is ...@@ -65,21 +67,21 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
function Length (M : Map) return Count_Type with function Length (M : Map) return Count_Type with
Global => null; Global => null;
function "<=" (M1, M2 : Map) return Boolean with function "<=" (M1 : Map; M2 : Map) return Boolean with
-- Map inclusion -- Map inclusion
Global => null, Global => null,
Post => "<="'Result = Post => "<="'Result =
(for all K of M1 => Mem (M2, K) (for all K of M1 =>
and then Get (M2, K) = Get (M1, K)); Mem (M2, K) and then Get (M2, K) = Get (M1, K));
function "=" (M1, M2 : Map) return Boolean with function "=" (M1 : Map; M2 : Map) return Boolean with
-- Extensional equality over maps -- Extensional equality over maps
Global => null, Global => null,
Post => "="'Result = Post => "="'Result =
((for all K of M1 => Mem (M2, K) and then Get (M2, K) = Get (M1, K)) ((for all K of M1 => Mem (M2, K) and then Get (M2, K) = Get (M1, K))
and (for all K of M2 => Mem (M1, K))); and (for all K of M2 => Mem (M1, K)));
pragma Warnings (Off, "unused variable ""K"""); pragma Warnings (Off, "unused variable ""K""");
function Is_Empty (M : Map) return Boolean with function Is_Empty (M : Map) return Boolean with
...@@ -89,18 +91,23 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is ...@@ -89,18 +91,23 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
pragma Warnings (On, "unused variable ""K"""); pragma Warnings (On, "unused variable ""K""");
function Is_Add function Is_Add
(M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean (M : Map;
K : Key_Type;
E : Element_Type;
Result : Map) return Boolean
-- Returns True if Result is M augmented with the mapping K -> E -- Returns True if Result is M augmented with the mapping K -> E
with with
Global => null, Global => null,
Post => Is_Add'Result = Post =>
Is_Add'Result =
(not Mem (M, K) (not Mem (M, K)
and then (Mem (Result, K) and then Get (Result, K) = E and then Mem (Result, K)
and then (for all K of M => Mem (Result, K) and then Get (Result, K) = E
and then Get (Result, K) = Get (M, K)) and then (for all K of M =>
Mem (Result, K) and then Get (Result, K) = Get (M, K))
and then (for all KK of Result => and then (for all KK of Result =>
Equivalent_Keys (KK, K) or Mem (M, KK)))); Equivalent_Keys (KK, K) or Mem (M, KK)));
function Add (M : Map; K : Key_Type; E : Element_Type) return Map with function Add (M : Map; K : Key_Type; E : Element_Type) return Map with
-- Returns M augmented with the mapping K -> E. -- Returns M augmented with the mapping K -> E.
...@@ -137,8 +144,8 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is ...@@ -137,8 +144,8 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
Global => null, Global => null,
Pre => Mem (M, K), Pre => Mem (M, K),
Post => Length (M) = Length (Set'Result) Post =>
and Is_Set (M, K, E, Set'Result); Length (M) = Length (Set'Result) and Is_Set (M, K, E, Set'Result);
--------------------------- ---------------------------
-- Iteration Primitives -- -- Iteration Primitives --
...@@ -148,11 +155,14 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is ...@@ -148,11 +155,14 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
function Iter_First (M : Map) return Private_Key with function Iter_First (M : Map) return Private_Key with
Global => null; Global => null;
function Iter_Has_Element (M : Map; K : Private_Key) return Boolean with function Iter_Has_Element (M : Map; K : Private_Key) return Boolean with
Global => null; Global => null;
function Iter_Next (M : Map; K : Private_Key) return Private_Key with function Iter_Next (M : Map; K : Private_Key) return Private_Key with
Global => null, Global => null,
Pre => Iter_Has_Element (M, K); Pre => Iter_Has_Element (M, K);
function Iter_Element (M : Map; K : Private_Key) return Key_Type with function Iter_Element (M : Map; K : Private_Key) return Key_Type with
Global => null, Global => null,
Pre => Iter_Has_Element (M, K); Pre => Iter_Has_Element (M, K);
...@@ -162,18 +172,19 @@ private ...@@ -162,18 +172,19 @@ private
pragma SPARK_Mode (Off); pragma SPARK_Mode (Off);
function "=" (Left, Right : Key_Type) return Boolean function "="
renames Equivalent_Keys; (Left : Key_Type;
Right : Key_Type) return Boolean renames Equivalent_Keys;
subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last; subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
package Element_Containers is new Ada.Containers.Functional_Base package Element_Containers is new Ada.Containers.Functional_Base
(Element_Type => Element_Type, (Element_Type => Element_Type,
Index_Type => Positive_Count_Type); Index_Type => Positive_Count_Type);
package Key_Containers is new Ada.Containers.Functional_Base package Key_Containers is new Ada.Containers.Functional_Base
(Element_Type => Key_Type, (Element_Type => Key_Type,
Index_Type => Positive_Count_Type); Index_Type => Positive_Count_Type);
type Map is record type Map is record
Keys : Key_Containers.Container; Keys : Key_Containers.Container;
......
...@@ -38,14 +38,15 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is ...@@ -38,14 +38,15 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
-- "=" -- -- "=" --
--------- ---------
function "=" (S1, S2 : Set) return Boolean is function "=" (S1 : Set; S2 : Set) return Boolean is
(S1.Content <= S2.Content and S2.Content <= S1.Content); (S1.Content <= S2.Content and S2.Content <= S1.Content);
---------- ----------
-- "<=" -- -- "<=" --
---------- ----------
function "<=" (S1, S2 : Set) return Boolean is (S1.Content <= S2.Content); function "<=" (S1 : Set; S2 : Set) return Boolean is
(S1.Content <= S2.Content);
--------- ---------
-- Add -- -- Add --
...@@ -58,7 +59,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is ...@@ -58,7 +59,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
-- Intersection -- -- Intersection --
------------------ ------------------
function Intersection (S1, S2 : Set) return Set is function Intersection (S1 : Set; S2 : Set) return Set is
(Content => Intersection (S1.Content, S2.Content)); (Content => Intersection (S1.Content, S2.Content));
------------ ------------
...@@ -68,8 +69,8 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is ...@@ -68,8 +69,8 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
function Is_Add (S : Set; E : Element_Type; Result : Set) return Boolean function Is_Add (S : Set; E : Element_Type; Result : Set) return Boolean
is is
(Mem (Result, E) (Mem (Result, E)
and (for all F of Result => Mem (S, F) or F = E) and (for all F of Result => Mem (S, F) or F = E)
and (for all E of S => Mem (Result, E))); and (for all E of S => Mem (Result, E)));
-------------- --------------
-- Is_Empty -- -- Is_Empty --
...@@ -81,20 +82,24 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is ...@@ -81,20 +82,24 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
-- Is_Intersection -- -- Is_Intersection --
--------------------- ---------------------
function Is_Intersection (S1, S2, Result : Set) return Boolean is function Is_Intersection
(S1 : Set;
S2 : Set;
Result : Set) return Boolean
is
((for all E of Result => ((for all E of Result =>
Mem (S1, E) and Mem (S2, E)) Mem (S1, E)
and (for all E of S1 => and Mem (S2, E))
(if Mem (S2, E) then Mem (Result, E)))); and (for all E of S1 => (if Mem (S2, E) then Mem (Result, E))));
-------------- --------------
-- Is_Union -- -- Is_Union --
-------------- --------------
function Is_Union (S1, S2, Result : Set) return Boolean is function Is_Union (S1 : Set; S2 : Set; Result : Set) return Boolean is
((for all E of Result => Mem (S1, E) or Mem (S2, E)) ((for all E of Result => Mem (S1, E) or Mem (S2, E))
and (for all E of S1 => Mem (Result, E)) and (for all E of S1 => Mem (Result, E))
and (for all E of S2 => Mem (Result, E))); and (for all E of S2 => Mem (Result, E)));
------------ ------------
-- Length -- -- Length --
...@@ -107,14 +112,14 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is ...@@ -107,14 +112,14 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
--------- ---------
function Mem (S : Set; E : Element_Type) return Boolean is function Mem (S : Set; E : Element_Type) return Boolean is
(Find (S.Content, E) > 0); (Find (S.Content, E) > 0);
------------------ ------------------
-- Num_Overlaps -- -- Num_Overlaps --
------------------ ------------------
function Num_Overlaps (S1, S2 : Set) return Count_Type is function Num_Overlaps (S1 : Set; S2 : Set) return Count_Type is
(Num_Overlaps (S1.Content, S2.Content)); (Num_Overlaps (S1.Content, S2.Content));
------------ ------------
-- Remove -- -- Remove --
...@@ -127,6 +132,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is ...@@ -127,6 +132,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
-- Union -- -- Union --
----------- -----------
function Union (S1, S2 : Set) return Set is function Union (S1 : Set; S2 : Set) return Set is
(Content => Union (S1.Content, S2.Content)); (Content => Union (S1.Content, S2.Content));
end Ada.Containers.Functional_Sets; end Ada.Containers.Functional_Sets;
...@@ -35,6 +35,7 @@ private with Ada.Containers.Functional_Base; ...@@ -35,6 +35,7 @@ private with Ada.Containers.Functional_Base;
generic generic
type Element_Type (<>) is private; type Element_Type (<>) is private;
with function "=" (Left, Right : Element_Type) return Boolean is <>; with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Functional_Sets with SPARK_Mode is package Ada.Containers.Functional_Sets with SPARK_Mode is
pragma Assertion_Policy (Post => Ignore); pragma Assertion_Policy (Post => Ignore);
...@@ -59,19 +60,20 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -59,19 +60,20 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
function Length (S : Set) return Count_Type with function Length (S : Set) return Count_Type with
Global => null; Global => null;
function "<=" (S1, S2 : Set) return Boolean with function "<=" (S1 : Set; S2 : Set) return Boolean with
-- Set inclusion -- Set inclusion
Global => null, Global => null,
Post => "<="'Result = (for all E of S1 => Mem (S2, E)); Post => "<="'Result = (for all E of S1 => Mem (S2, E));
function "=" (S1, S2 : Set) return Boolean with function "=" (S1 : Set; S2 : Set) return Boolean with
-- Extensional equality over sets -- Extensional equality over sets
Global => null, Global => null,
Post => Post =>
"="'Result = ((for all E of S1 => Mem (S2, E)) "="'Result =
and (for all E of S2 => Mem (S1, E))); ((for all E of S1 => Mem (S2, E))
and (for all E of S2 => Mem (S1, E)));
pragma Warnings (Off, "unused variable ""E"""); pragma Warnings (Off, "unused variable ""E""");
function Is_Empty (S : Set) return Boolean with function Is_Empty (S : Set) return Boolean with
...@@ -86,10 +88,12 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -86,10 +88,12 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
with with
Global => null, Global => null,
Post => Is_Add'Result = Post =>
(Mem (Result, E) and not Mem (S, E) Is_Add'Result =
and (for all F of Result => Mem (S, F) or F = E) (Mem (Result, E)
and (for all E of S => Mem (Result, E))); and not Mem (S, E)
and (for all F of Result => Mem (S, F) or F = E)
and (for all E of S => Mem (Result, E)));
function Add (S : Set; E : Element_Type) return Set with function Add (S : Set; E : Element_Type) return Set with
-- Returns S augmented with E. -- Returns S augmented with E.
...@@ -98,8 +102,9 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -98,8 +102,9 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
Global => null, Global => null,
Pre => not Mem (S, E) and Length (S) < Count_Type'Last, Pre => not Mem (S, E) and Length (S) < Count_Type'Last,
Post => Length (Add'Result) = Length (S) + 1 Post =>
and Is_Add (S, E, Add'Result); Length (Add'Result) = Length (S) + 1
and Is_Add (S, E, Add'Result);
function Remove (S : Set; E : Element_Type) return Set with function Remove (S : Set; E : Element_Type) return Set with
-- Returns S without E. -- Returns S without E.
...@@ -108,59 +113,67 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -108,59 +113,67 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
Global => null, Global => null,
Pre => Mem (S, E), Pre => Mem (S, E),
Post => Length (Remove'Result) = Length (S) - 1 Post =>
and Is_Add (Remove'Result, E, S); Length (Remove'Result) = Length (S) - 1
and Is_Add (Remove'Result, E, S);
function Is_Intersection (S1, S2, Result : Set) return Boolean with function Is_Intersection
(S1 : Set;
S2 : Set;
Result : Set) return Boolean
with
-- Returns True if Result is the intersection of S1 and S2 -- Returns True if Result is the intersection of S1 and S2
Global => null, Global => null,
Post => Is_Intersection'Result = Post =>
((for all E of Result => Is_Intersection'Result =
Mem (S1, E) and Mem (S2, E)) ((for all E of Result => Mem (S1, E) and Mem (S2, E))
and (for all E of S1 => and (for all E of S1 => (if Mem (S2, E) then Mem (Result, E))));
(if Mem (S2, E) then Mem (Result, E))));
function Num_Overlaps (S1, S2 : Set) return Count_Type with function Num_Overlaps (S1 : Set; S2 : Set) return Count_Type with
-- Number of elements that are both in S1 and S2 -- Number of elements that are both in S1 and S2
Global => null, Global => null,
Post => Num_Overlaps'Result <= Length (S1) Post =>
and Num_Overlaps'Result <= Length (S2) Num_Overlaps'Result <= Length (S1)
and (if Num_Overlaps'Result = 0 then and Num_Overlaps'Result <= Length (S2)
(for all E of S1 => not Mem (S2, E))); and (if Num_Overlaps'Result = 0 then
(for all E of S1 => not Mem (S2, E)));
function Intersection (S1, S2 : Set) return Set with function Intersection (S1 : Set; S2 : Set) return Set with
-- Returns the intersection of S1 and S2. -- Returns the intersection of S1 and S2.
-- Intersection (S1, S2, Result) should be used instead of -- Intersection (S1, S2, Result) should be used instead of
-- Result = Intersection (S1, S2) whenever possible both for execution and -- Result = Intersection (S1, S2) whenever possible both for execution and
-- for proof. -- for proof.
Global => null, Global => null,
Post => Length (Intersection'Result) = Num_Overlaps (S1, S2) Post =>
and Is_Intersection (S1, S2, Intersection'Result); Length (Intersection'Result) = Num_Overlaps (S1, S2)
and Is_Intersection (S1, S2, Intersection'Result);
function Is_Union (S1, S2, Result : Set) return Boolean with function Is_Union (S1 : Set; S2 : Set; Result : Set) return Boolean with
-- Returns True if Result is the union of S1 and S2 -- Returns True if Result is the union of S1 and S2
Global => null, Global => null,
Post => Is_Union'Result = Post =>
((for all E of Result => Mem (S1, E) or Mem (S2, E)) Is_Union'Result =
and (for all E of S1 => Mem (Result, E)) ((for all E of Result => Mem (S1, E) or Mem (S2, E))
and (for all E of S2 => Mem (Result, E))); and (for all E of S1 => Mem (Result, E))
and (for all E of S2 => Mem (Result, E)));
function Union (S1, S2 : Set) return Set with function Union (S1 : Set; S2 : Set) return Set with
-- Returns the union of S1 and S2. -- Returns the union of S1 and S2.
-- Is_Union (S1, S2, Result) should be used instead of -- Is_Union (S1, S2, Result) should be used instead of
-- Result = Union (S1, S2) whenever possible both for execution and for -- Result = Union (S1, S2) whenever possible both for execution and for
-- proof. -- proof.
Global => null, Global => null,
Pre => Length (S1) - Num_Overlaps (S1, S2) <= Pre =>
Count_Type'Last - Length (S2), Length (S1) - Num_Overlaps (S1, S2) <= Count_Type'Last - Length (S2),
Post => Length (Union'Result) = Length (S1) - Num_Overlaps (S1, S2) Post =>
+ Length (S2) Length (Union'Result) =
and Is_Union (S1, S2, Union'Result); Length (S1) - Num_Overlaps (S1, S2) + Length (S2)
and Is_Union (S1, S2, Union'Result);
--------------------------- ---------------------------
-- Iteration Primitives -- -- Iteration Primitives --
...@@ -170,11 +183,14 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -170,11 +183,14 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
function Iter_First (S : Set) return Private_Key with function Iter_First (S : Set) return Private_Key with
Global => null; Global => null;
function Iter_Has_Element (S : Set; K : Private_Key) return Boolean with function Iter_Has_Element (S : Set; K : Private_Key) return Boolean with
Global => null; Global => null;
function Iter_Next (S : Set; K : Private_Key) return Private_Key with function Iter_Next (S : Set; K : Private_Key) return Private_Key with
Global => null, Global => null,
Pre => Iter_Has_Element (S, K); Pre => Iter_Has_Element (S, K);
function Iter_Element (S : Set; K : Private_Key) return Element_Type with function Iter_Element (S : Set; K : Private_Key) return Element_Type with
Global => null, Global => null,
Pre => Iter_Has_Element (S, K); Pre => Iter_Has_Element (S, K);
......
...@@ -37,25 +37,25 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is ...@@ -37,25 +37,25 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
-- "=" -- -- "=" --
--------- ---------
function "=" (S1, S2 : Sequence) return Boolean is function "=" (S1 : Sequence; S2 : Sequence) return Boolean is
(S1.Content = S2.Content); (S1.Content = S2.Content);
--------- ---------
-- "<" -- -- "<" --
--------- ---------
function "<" (S1, S2 : Sequence) return Boolean is function "<" (S1 : Sequence; S2 : Sequence) return Boolean is
(Length (S1.Content) < Length (S2.Content) (Length (S1.Content) < Length (S2.Content)
and then (for all I in Index_Type'First .. Last (S1) => and then (for all I in Index_Type'First .. Last (S1) =>
Get (S1.Content, I) = Get (S2.Content, I))); Get (S1.Content, I) = Get (S2.Content, I)));
---------- ----------
-- "<=" -- -- "<=" --
---------- ----------
function "<=" (S1, S2 : Sequence) return Boolean is function "<=" (S1 : Sequence; S2 : Sequence) return Boolean is
(Length (S1.Content) <= Length (S2.Content) (Length (S1.Content) <= Length (S2.Content)
and then (for all I in Index_Type'First .. Last (S1) => and then (for all I in Index_Type'First .. Last (S1) =>
Get (S1.Content, I) = Get (S2.Content, I))); Get (S1.Content, I) = Get (S2.Content, I)));
--------- ---------
...@@ -83,7 +83,8 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is ...@@ -83,7 +83,8 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
function Insert function Insert
(S : Sequence; (S : Sequence;
N : Index_Type; N : Index_Type;
E : Element_Type) return Sequence is E : Element_Type) return Sequence
is
(Content => Add (S.Content, N, E)); (Content => Add (S.Content, N, E));
------------ ------------
...@@ -91,24 +92,30 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is ...@@ -91,24 +92,30 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
------------ ------------
function Is_Add function Is_Add
(S : Sequence; E : Element_Type; Result : Sequence) return Boolean is (S : Sequence;
E : Element_Type;
Result : Sequence) return Boolean
is
(Length (Result) = Length (S) + 1 (Length (Result) = Length (S) + 1
and then Get (Result, Index_Type'Val and then Get (Result, Index_Type'Val
((Index_Type'Pos (Index_Type'First) - 1) + ((Index_Type'Pos (Index_Type'First) - 1) +
Length (Result))) = E Length (Result))) = E
and then and then
(for all M in Index_Type'First .. (for all M in Index_Type'First ..
(Index_Type'Val (Index_Type'Val
((Index_Type'Pos (Index_Type'First) - 1) + Length (S))) => ((Index_Type'Pos (Index_Type'First) - 1) + Length (S))) =>
Get (Result, M) = Get (S, M))); Get (Result, M) = Get (S, M)));
------------ ------------
-- Is_Set -- -- Is_Set --
------------ ------------
function Is_Set function Is_Set
(S : Sequence; N : Index_Type; E : Element_Type; Result : Sequence) (S : Sequence;
return Boolean is N : Index_Type;
E : Element_Type;
Result : Sequence) return Boolean
is
(N in Index_Type'First .. (N in Index_Type'First ..
(Index_Type'Val (Index_Type'Val
((Index_Type'Pos (Index_Type'First) - 1) + Length (S))) ((Index_Type'Pos (Index_Type'First) - 1) + Length (S)))
...@@ -145,7 +152,11 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is ...@@ -145,7 +152,11 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
-- Set -- -- Set --
--------- ---------
function Set (S : Sequence; N : Index_Type; E : Element_Type) function Set
return Sequence is (S : Sequence;
N : Index_Type;
E : Element_Type) return Sequence
is
(Content => Set (S.Content, N, E)); (Content => Set (S.Content, N, E));
end Ada.Containers.Functional_Vectors; end Ada.Containers.Functional_Vectors;
...@@ -39,6 +39,7 @@ generic ...@@ -39,6 +39,7 @@ generic
type Element_Type (<>) is private; type Element_Type (<>) is private;
with function "=" (Left, Right : Element_Type) return Boolean is <>; with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Functional_Vectors with SPARK_Mode is package Ada.Containers.Functional_Vectors with SPARK_Mode is
pragma Assertion_Policy (Post => Ignore); pragma Assertion_Policy (Post => Ignore);
...@@ -64,13 +65,15 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -64,13 +65,15 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
function Length (S : Sequence) return Count_Type with function Length (S : Sequence) return Count_Type with
Global => null, Global => null,
Post => (Index_Type'Pos (Index_Type'First) - 1) + Length'Result <= Post =>
Index_Type'Pos (Index_Type'Last); (Index_Type'Pos (Index_Type'First) - 1) + Length'Result <=
Index_Type'Pos (Index_Type'Last);
function Last (S : Sequence) return Extended_Index with function Last (S : Sequence) return Extended_Index with
Global => null, Global => null,
Post => Last'Result = Post =>
Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) + Length (S)); Last'Result =
Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) + Length (S));
function First return Extended_Index is (Index_Type'First); function First return Extended_Index is (Index_Type'First);
...@@ -81,42 +84,48 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -81,42 +84,48 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
Global => null, Global => null,
Pre => N in Index_Type'First .. Last (S); Pre => N in Index_Type'First .. Last (S);
function "=" (S1, S2 : Sequence) return Boolean with function "=" (S1 : Sequence; S2 : Sequence) return Boolean with
-- Extensional equality over sequences -- Extensional equality over sequences
Global => null, Global => null,
Post => "="'Result = Post =>
(Length (S1) = Length (S2) "="'Result =
and then (for all N in Index_Type'First .. Last (S1) => (Length (S1) = Length (S2)
Get (S1, N) = Get (S2, N))); and then (for all N in Index_Type'First .. Last (S1) =>
Get (S1, N) = Get (S2, N)));
function "<" (S1, S2 : Sequence) return Boolean with function "<" (S1 : Sequence; S2 : Sequence) return Boolean with
-- S1 is a strict subsequence of S2 -- S1 is a strict subsequence of S2
Global => null, Global => null,
Post => "<"'Result = Post =>
(Length (S1) < Length (S2) "<"'Result =
and then (for all N in Index_Type'First .. Last (S1) => (Length (S1) < Length (S2)
Get (S1, N) = Get (S2, N))); and then (for all N in Index_Type'First .. Last (S1) =>
Get (S1, N) = Get (S2, N)));
function "<=" (S1, S2 : Sequence) return Boolean with function "<=" (S1 : Sequence; S2 : Sequence) return Boolean with
-- S1 is a subsequence of S2 -- S1 is a subsequence of S2
Global => null, Global => null,
Post => "<="'Result = Post =>
(Length (S1) <= Length (S2) "<="'Result =
and then (for all N in Index_Type'First .. Last (S1) => (Length (S1) <= Length (S2)
Get (S1, N) = Get (S2, N))); and then (for all N in Index_Type'First .. Last (S1) =>
Get (S1, N) = Get (S2, N)));
function Is_Set function Is_Set
(S : Sequence; N : Index_Type; E : Element_Type; Result : Sequence) (S : Sequence;
return Boolean N : Index_Type;
E : Element_Type;
Result : Sequence) return Boolean
-- Returns True if Result is S, where the Nth element has been replaced by -- Returns True if Result is S, where the Nth element has been replaced by
-- E. -- E.
with with
Global => null, Global => null,
Post => Is_Set'Result = Post =>
Is_Set'Result =
(N in Index_Type'First .. Last (S) (N in Index_Type'First .. Last (S)
and then Length (Result) = Length (S) and then Length (Result) = Length (S)
and then Get (Result, N) = E and then Get (Result, N) = E
...@@ -124,7 +133,9 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -124,7 +133,9 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
(if M /= N then Get (Result, M) = Get (S, M)))); (if M /= N then Get (Result, M) = Get (S, M))));
function Set function Set
(S : Sequence; N : Index_Type; E : Element_Type) return Sequence (S : Sequence;
N : Index_Type;
E : Element_Type) return Sequence
-- Returns S, where the Nth element has been replaced by E. -- Returns S, where the Nth element has been replaced by E.
-- Is_Set (S, N, E, Result) should be used instead of -- Is_Set (S, N, E, Result) should be used instead of
-- Result = Set (S, N, E) whenever possible both for execution and for -- Result = Set (S, N, E) whenever possible both for execution and for
...@@ -136,12 +147,15 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -136,12 +147,15 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
Post => Is_Set (S, N, E, Set'Result); Post => Is_Set (S, N, E, Set'Result);
function Is_Add function Is_Add
(S : Sequence; E : Element_Type; Result : Sequence) return Boolean (S : Sequence;
E : Element_Type;
Result : Sequence) return Boolean
-- Returns True if Result is S appended with E -- Returns True if Result is S appended with E
with with
Global => null, Global => null,
Post => Is_Add'Result = Post =>
Is_Add'Result =
(Length (Result) = Length (S) + 1 (Length (Result) = Length (S) + 1
and then Get (Result, Last (Result)) = E and then Get (Result, Last (Result)) = E
and then (for all M in Index_Type'First .. Last (S) => and then (for all M in Index_Type'First .. Last (S) =>
...@@ -164,30 +178,42 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -164,30 +178,42 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
-- Returns S with E inserted at index I -- Returns S with E inserted at index I
Global => null, Global => null,
Pre => Length (S) < Count_Type'Last and then Last (S) < Index_Type'Last Pre =>
and then N <= Extended_Index'Succ (Last (S)), Length (S) < Count_Type'Last
Post => Length (Insert'Result) = Length (S) + 1 and then Last (S) < Index_Type'Last
and then Get (Insert'Result, N) = E and then N <= Extended_Index'Succ (Last (S)),
and then (for all M in Index_Type'First .. Extended_Index'Pred (N) => Post =>
Get (Insert'Result, M) = Get (S, M)) Length (Insert'Result) = Length (S) + 1
and then (for all M in Extended_Index'Succ (N) .. Last (Insert'Result) => and then Get (Insert'Result, N) = E
Get (Insert'Result, M) = Get (S, Extended_Index'Pred (M))) and then
and then (for all M in N .. Last (S) => (for all M in Index_Type'First .. Extended_Index'Pred (N) =>
Get (Insert'Result, Extended_Index'Succ (M)) = Get (S, M)); Get (Insert'Result, M) = Get (S, M))
and then
(for all M in Extended_Index'Succ (N) .. Last (Insert'Result) =>
Get (Insert'Result, M) = Get (S, Extended_Index'Pred (M)))
and then
(for all M in N .. Last (S) =>
Get (Insert'Result, Extended_Index'Succ (M)) = Get (S, M));
function Remove (S : Sequence; N : Index_Type) return Sequence with function Remove (S : Sequence; N : Index_Type) return Sequence with
-- Returns S without the element at index N -- Returns S without the element at index N
Global => null, Global => null,
Pre => Length (S) < Count_Type'Last and Last (S) < Index_Type'Last Pre =>
and N in Index_Type'First .. Last (S), Length (S) < Count_Type'Last
Post => Length (Remove'Result) = Length (S) - 1 and Last (S) < Index_Type'Last
and then (for all M in Index_Type'First .. Extended_Index'Pred (N) => and N in Index_Type'First .. Last (S),
Get (Remove'Result, M) = Get (S, M)) Post =>
and then (for all M in N .. Last (Remove'Result) => Length (Remove'Result) = Length (S) - 1
Get (Remove'Result, M) = Get (S, Extended_Index'Succ (M))) and then
and then (for all M in Extended_Index'Succ (N) .. Last (S) => (for all M in Index_Type'First .. Extended_Index'Pred (N) =>
Get (Remove'Result, Extended_Index'Pred (M)) = Get (S, M)); Get (Remove'Result, M) = Get (S, M))
and then
(for all M in N .. Last (Remove'Result) =>
Get (Remove'Result, M) = Get (S, Extended_Index'Succ (M)))
and then
(for all M in Extended_Index'Succ (N) .. Last (S) =>
Get (Remove'Result, Extended_Index'Pred (M)) = Get (S, M));
--------------------------- ---------------------------
-- Iteration Primitives -- -- Iteration Primitives --
...@@ -195,6 +221,7 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -195,6 +221,7 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
function Iter_First (S : Sequence) return Extended_Index with function Iter_First (S : Sequence) return Extended_Index with
Global => null; Global => null;
function Iter_Has_Element (S : Sequence; I : Extended_Index) return Boolean function Iter_Has_Element (S : Sequence; I : Extended_Index) return Boolean
with with
Global => null, Global => null,
...@@ -218,18 +245,22 @@ private ...@@ -218,18 +245,22 @@ private
Content : Containers.Container; Content : Containers.Container;
end record; end record;
function Iter_First (S : function Iter_First (S : Sequence) return Extended_Index is
Sequence) return Extended_Index (Index_Type'First);
is (Index_Type'First);
function Iter_Next (S : Sequence; I : Extended_Index) return Extended_Index function Iter_Next
(S : Sequence;
I : Extended_Index) return Extended_Index
is is
(if I = Extended_Index'Last then Extended_Index'First (if I = Extended_Index'Last then Extended_Index'First
else Extended_Index'Succ (I)); else Extended_Index'Succ (I));
function Iter_Has_Element (S : Sequence; I : Extended_Index) return Boolean function Iter_Has_Element
(S : Sequence;
I : Extended_Index) return Boolean
is is
(I in Index_Type'First .. (I in Index_Type'First ..
(Index_Type'Val (Index_Type'Val
((Index_Type'Pos (Index_Type'First) - 1) + Length (S)))); ((Index_Type'Pos (Index_Type'First) - 1) + Length (S))));
end Ada.Containers.Functional_Vectors; end Ada.Containers.Functional_Vectors;
...@@ -1176,7 +1176,7 @@ package body CStand is ...@@ -1176,7 +1176,7 @@ package body CStand is
-- Any_Integer is given reasonable and consistent type and size values) -- Any_Integer is given reasonable and consistent type and size values)
Any_Type := New_Standard_Entity ("any type"); Any_Type := New_Standard_Entity ("any type");
Decl := New_Node (N_Full_Type_Declaration, Stloc); Decl := New_Node (N_Full_Type_Declaration, Stloc);
Set_Defining_Identifier (Decl, Any_Type); Set_Defining_Identifier (Decl, Any_Type);
Set_Scope (Any_Type, Standard_Standard); Set_Scope (Any_Type, Standard_Standard);
Build_Signed_Integer_Type (Any_Type, Standard_Integer_Size); Build_Signed_Integer_Type (Any_Type, Standard_Integer_Size);
...@@ -1194,7 +1194,8 @@ package body CStand is ...@@ -1194,7 +1194,8 @@ package body CStand is
Set_Etype (Any_Access, Any_Access); Set_Etype (Any_Access, Any_Access);
Init_Size (Any_Access, System_Address_Size); Init_Size (Any_Access, System_Address_Size);
Set_Elem_Alignment (Any_Access); Set_Elem_Alignment (Any_Access);
Set_Directly_Designated_Type (Any_Access, Any_Type); Set_Directly_Designated_Type
(Any_Access, Any_Type);
Any_Character := New_Standard_Entity ("a character type"); Any_Character := New_Standard_Entity ("a character type");
Set_Ekind (Any_Character, E_Enumeration_Type); Set_Ekind (Any_Character, E_Enumeration_Type);
......
...@@ -10977,8 +10977,11 @@ package body Einfo is ...@@ -10977,8 +10977,11 @@ package body Einfo is
procedure Write_Field38_Name (Id : Entity_Id) is procedure Write_Field38_Name (Id : Entity_Id) is
begin begin
case Ekind (Id) is case Ekind (Id) is
when E_Function | E_Procedure => when E_Function
| E_Procedure
=>
Write_Str ("class-wide clone"); Write_Str ("class-wide clone");
when others => when others =>
Write_Str ("Field38??"); Write_Str ("Field38??");
end case; end case;
......
...@@ -4043,22 +4043,42 @@ package body Exp_Ch7 is ...@@ -4043,22 +4043,42 @@ package body Exp_Ch7 is
procedure Establish_Transient_Scope (N : Node_Id; Sec_Stack : Boolean) is procedure Establish_Transient_Scope (N : Node_Id; Sec_Stack : Boolean) is
Loc : constant Source_Ptr := Sloc (N); Loc : constant Source_Ptr := Sloc (N);
Iter_Loop : Entity_Id; Iter_Loop : Entity_Id;
Scop_Id : Entity_Id;
Scop_Rec : Scope_Stack_Entry;
Wrap_Node : Node_Id; Wrap_Node : Node_Id;
begin begin
-- Do not create a transient scope if we are already inside one -- Do not create a new transient scope if there is an existing transient
-- scope on the stack.
for S in reverse Scope_Stack.First .. Scope_Stack.Last loop for Index in reverse Scope_Stack.First .. Scope_Stack.Last loop
if Scope_Stack.Table (S).Is_Transient then Scop_Rec := Scope_Stack.Table (Index);
Scop_Id := Scop_Rec.Entity;
-- The current scope is transient. If the scope being established
-- needs to manage the secondary stack, then the existing scope
-- overtakes that function.
if Scop_Rec.Is_Transient then
if Sec_Stack then if Sec_Stack then
Set_Uses_Sec_Stack (Scope_Stack.Table (S).Entity); Set_Uses_Sec_Stack (Scop_Id);
end if; end if;
return; return;
-- If we encounter Standard there are no enclosing transient scopes -- Prevent the search from going too far because transient blocks
-- are bounded by packages and subprogram scopes. Reaching Standard
elsif Scope_Stack.Table (S).Entity = Standard_Standard then -- should be impossible without hitting one of the other cases first
-- unless Standard was manually pushed.
elsif Scop_Id = Standard_Standard
or else Ekind_In (Scop_Id, E_Entry,
E_Entry_Family,
E_Function,
E_Package,
E_Procedure,
E_Subprogram_Body)
then
exit; exit;
end if; end if;
end loop; end loop;
......
...@@ -172,7 +172,7 @@ package body Exp_Prag is ...@@ -172,7 +172,7 @@ package body Exp_Prag is
if Should_Ignore_Pragma_Sem (N) if Should_Ignore_Pragma_Sem (N)
or else (Prag_Id = Pragma_Default_Scalar_Storage_Order or else (Prag_Id = Pragma_Default_Scalar_Storage_Order
and then Ignore_Rep_Clauses) and then Ignore_Rep_Clauses)
then then
Rewrite (N, Make_Null_Statement (Sloc (N))); Rewrite (N, Make_Null_Statement (Sloc (N)));
return; return;
......
...@@ -6,7 +6,7 @@ ...@@ -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- --
...@@ -33,6 +33,7 @@ with Namet; use Namet; ...@@ -33,6 +33,7 @@ with Namet; use Namet;
with Nlists; use Nlists; with Nlists; use Nlists;
with Nmake; use Nmake; with Nmake; use Nmake;
with Rtsfind; use Rtsfind; with Rtsfind; use Rtsfind;
with Sem; use Sem;
with Sem_Eval; use Sem_Eval; with Sem_Eval; use Sem_Eval;
with Sem_Res; use Sem_Res; with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util; with Sem_Util; use Sem_Util;
...@@ -48,10 +49,13 @@ package body Exp_SPARK is ...@@ -48,10 +49,13 @@ package body Exp_SPARK is
-- Local Subprograms -- -- Local Subprograms --
----------------------- -----------------------
procedure Expand_SPARK_Attribute_Reference (N : Node_Id); procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
-- Replace occurrences of System'To_Address by calls to -- Replace occurrences of System'To_Address by calls to
-- System.Storage_Elements.To_Address -- System.Storage_Elements.To_Address
procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
-- Perform object declaration-specific expansion
procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id); procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
-- Perform name evaluation for a renamed object -- Perform name evaluation for a renamed object
...@@ -81,19 +85,16 @@ package body Exp_SPARK is ...@@ -81,19 +85,16 @@ package body Exp_SPARK is
=> =>
Qualify_Entity_Names (N); Qualify_Entity_Names (N);
when N_Expanded_Name
| N_Identifier
=>
Expand_SPARK_Potential_Renaming (N);
when N_Object_Renaming_Declaration =>
Expand_SPARK_N_Object_Renaming_Declaration (N);
-- Replace occurrences of System'To_Address by calls to -- Replace occurrences of System'To_Address by calls to
-- System.Storage_Elements.To_Address -- System.Storage_Elements.To_Address
when N_Attribute_Reference => when N_Attribute_Reference =>
Expand_SPARK_Attribute_Reference (N); Expand_SPARK_N_Attribute_Reference (N);
when N_Expanded_Name
| N_Identifier
=>
Expand_SPARK_Potential_Renaming (N);
-- Loop iterations over arrays need to be expanded, to avoid getting -- Loop iterations over arrays need to be expanded, to avoid getting
-- two names referring to the same object in memory (the array and -- two names referring to the same object in memory (the array and
...@@ -115,6 +116,12 @@ package body Exp_SPARK is ...@@ -115,6 +116,12 @@ package body Exp_SPARK is
end if; end if;
end; end;
when N_Object_Declaration =>
Expand_SPARK_N_Object_Declaration (N);
when N_Object_Renaming_Declaration =>
Expand_SPARK_N_Object_Renaming_Declaration (N);
-- In SPARK mode, no other constructs require expansion -- In SPARK mode, no other constructs require expansion
when others => when others =>
...@@ -122,11 +129,11 @@ package body Exp_SPARK is ...@@ -122,11 +129,11 @@ package body Exp_SPARK is
end case; end case;
end Expand_SPARK; end Expand_SPARK;
-------------------------------------- ----------------------------------------
-- Expand_SPARK_Attribute_Reference -- -- Expand_SPARK_N_Attribute_Reference --
-------------------------------------- ----------------------------------------
procedure Expand_SPARK_Attribute_Reference (N : Node_Id) is procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is
Aname : constant Name_Id := Attribute_Name (N); Aname : constant Name_Id := Attribute_Name (N);
Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname); Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname);
Loc : constant Source_Ptr := Sloc (N); Loc : constant Source_Ptr := Sloc (N);
...@@ -224,7 +231,31 @@ package body Exp_SPARK is ...@@ -224,7 +231,31 @@ package body Exp_SPARK is
end if; end if;
end; end;
end if; end if;
end Expand_SPARK_Attribute_Reference; end Expand_SPARK_N_Attribute_Reference;
---------------------------------------
-- Expand_SPARK_N_Object_Declaration --
---------------------------------------
procedure Expand_SPARK_N_Object_Declaration (N : Node_Id) is
Def_Id : constant Entity_Id := Defining_Identifier (N);
Loc : constant Source_Ptr := Sloc (N);
Typ : constant Entity_Id := Etype (Def_Id);
begin
-- If the object declaration denotes a variable without initialization
-- whose type is subject to pragma Default_Initial_Condition, create
-- and analyze a dummy call to the DIC procedure of the type in order
-- to detect potential elaboration issues.
if Comes_From_Source (Def_Id)
and then Has_DIC (Typ)
and then Present (DIC_Procedure (Typ))
and then not Has_Init_Expression (N)
then
Analyze (Build_DIC_Call (Loc, Def_Id, Typ));
end if;
end Expand_SPARK_N_Object_Declaration;
------------------------------------------------ ------------------------------------------------
-- Expand_SPARK_N_Object_Renaming_Declaration -- -- Expand_SPARK_N_Object_Renaming_Declaration --
......
...@@ -297,7 +297,7 @@ begin ...@@ -297,7 +297,7 @@ begin
if Should_Ignore_Pragma_Par (Prag_Name) if Should_Ignore_Pragma_Par (Prag_Name)
or else (Prag_Id = Pragma_Default_Scalar_Storage_Order or else (Prag_Id = Pragma_Default_Scalar_Storage_Order
and then Ignore_Rep_Clauses) and then Ignore_Rep_Clauses)
then then
return Pragma_Node; return Pragma_Node;
end if; end if;
......
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- S Y S T E M . E X C E P T I O N S . M A C H I N E --
-- --
-- B o d y --
-- --
-- Copyright (C) 2013-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- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
-- --
-- GNAT was originally developed by the GNAT team at New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc. --
-- --
------------------------------------------------------------------------------
package body System.Exceptions.Machine is
function New_Occurrence return GNAT_GCC_Exception_Access is
Res : GNAT_GCC_Exception_Access;
begin
Res := new GNAT_GCC_Exception;
Res.Header.Class := GNAT_Exception_Class;
Res.Header.Unwinder_Cache. Reserved1 := 0;
return Res;
end New_Occurrence;
end System.Exceptions.Machine;
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- S p e c -- -- S p e c --
-- -- -- --
-- Copyright (C) 2013, Free Software Foundation, Inc. -- -- Copyright (C) 2013-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- --
...@@ -174,13 +174,7 @@ package System.Exceptions.Machine is ...@@ -174,13 +174,7 @@ package System.Exceptions.Machine is
Ada.Unchecked_Conversion Ada.Unchecked_Conversion
(GCC_Exception_Access, GNAT_GCC_Exception_Access); (GCC_Exception_Access, GNAT_GCC_Exception_Access);
function New_Occurrence return GNAT_GCC_Exception_Access is function New_Occurrence return GNAT_GCC_Exception_Access;
(new GNAT_GCC_Exception'
(Header => (Class => GNAT_Exception_Class,
Unwinder_Cache => (Reserved1 => 0,
others => <>),
others => <>),
Occurrence => <>));
-- Allocate and initialize a machine occurrence -- Allocate and initialize a machine occurrence
end System.Exceptions.Machine; end System.Exceptions.Machine;
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- S Y S T E M . E X C E P T I O N S . M A C H I N E --
-- --
-- B o d y --
-- --
-- Copyright (C) 2013-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- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
-- --
-- GNAT was originally developed by the GNAT team at New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc. --
-- --
------------------------------------------------------------------------------
package body System.Exceptions.Machine is
function New_Occurrence return GNAT_GCC_Exception_Access is
Res : GNAT_GCC_Exception_Access;
begin
Res := new GNAT_GCC_Exception;
Res.Header := (Class => GNAT_Exception_Class,
Cleanup => Null_Address,
others => 0);
return Res;
end New_Occurrence;
end System.Exceptions.Machine;
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- S p e c -- -- S p e c --
-- -- -- --
-- Copyright (C) 2013-2014, Free Software Foundation, Inc. -- -- Copyright (C) 2013-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- --
...@@ -179,12 +179,7 @@ package System.Exceptions.Machine is ...@@ -179,12 +179,7 @@ package System.Exceptions.Machine is
Ada.Unchecked_Conversion Ada.Unchecked_Conversion
(GCC_Exception_Access, GNAT_GCC_Exception_Access); (GCC_Exception_Access, GNAT_GCC_Exception_Access);
function New_Occurrence return GNAT_GCC_Exception_Access is function New_Occurrence return GNAT_GCC_Exception_Access;
(new GNAT_GCC_Exception'
(Header => (Class => GNAT_Exception_Class,
Cleanup => Null_Address,
others => 0),
Occurrence => <>));
-- Allocate and initialize a machine occurrence -- Allocate and initialize a machine occurrence
end System.Exceptions.Machine; end System.Exceptions.Machine;
...@@ -644,12 +644,6 @@ package body Sem_Elab is ...@@ -644,12 +644,6 @@ package body Sem_Elab is
Loc : constant Source_Ptr := Sloc (N); Loc : constant Source_Ptr := Sloc (N);
SPARK_Elab_Errors : constant Boolean :=
SPARK_Mode = On
and then Dynamic_Elaboration_Checks;
-- Flag set when an entity is called or a variable is read during SPARK
-- dynamic elaboration.
Variable_Case : constant Boolean := Variable_Case : constant Boolean :=
Nkind (N) in N_Has_Entity Nkind (N) in N_Has_Entity
and then Present (Entity (N)) and then Present (Entity (N))
...@@ -693,6 +687,14 @@ package body Sem_Elab is ...@@ -693,6 +687,14 @@ package body Sem_Elab is
-- non-visible unit. This is the scope that is to be investigated to -- non-visible unit. This is the scope that is to be investigated to
-- see whether an elaboration check is required. -- see whether an elaboration check is required.
Is_DIC : Boolean;
-- Flag set when the subprogram being invoked the procedure generated
-- for pragma Default_Initial_Condition.
SPARK_Elab_Errors : Boolean;
-- Flag set when an entity is called or a variable is read during SPARK
-- dynamic elaboration.
-- Start of processing for Check_A_Call -- Start of processing for Check_A_Call
begin begin
...@@ -1025,6 +1027,17 @@ package body Sem_Elab is ...@@ -1025,6 +1027,17 @@ package body Sem_Elab is
return; return;
end if; end if;
-- Determine whether the Default_Initial_Condition procedure of some
-- type is being invoked.
Is_DIC := Ekind (Ent) = E_Procedure and then Is_DIC_Procedure (Ent);
-- Checks related to Default_Initial_Condition fall under the SPARK
-- umbrella because this is a SPARK-specific annotation.
SPARK_Elab_Errors :=
SPARK_Mode = On and (Is_DIC or Dynamic_Elaboration_Checks);
-- Now check if an Elaborate_All (or dynamic check) is needed -- Now check if an Elaborate_All (or dynamic check) is needed
if (Elab_Info_Messages or Elab_Warnings or SPARK_Elab_Errors) if (Elab_Info_Messages or Elab_Warnings or SPARK_Elab_Errors)
...@@ -1080,7 +1093,7 @@ package body Sem_Elab is ...@@ -1080,7 +1093,7 @@ package body Sem_Elab is
-- Default_Initial_Condition. This prevents the internal name -- Default_Initial_Condition. This prevents the internal name
-- of the procedure from appearing in the error message. -- of the procedure from appearing in the error message.
if Is_Nontrivial_DIC_Procedure (Ent) then if Is_DIC then
Error_Msg_N Error_Msg_N
("call to Default_Initial_Condition during elaboration in " ("call to Default_Initial_Condition during elaboration in "
& "SPARK", N); & "SPARK", N);
......
...@@ -3426,7 +3426,7 @@ package body Sem_Prag is ...@@ -3426,7 +3426,7 @@ package body Sem_Prag is
-------------------- --------------------
procedure Analyze_Pragma (N : Node_Id) is procedure Analyze_Pragma (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N); Loc : constant Source_Ptr := Sloc (N);
Pname : Name_Id := Pragma_Name (N); Pname : Name_Id := Pragma_Name (N);
-- Name of the source pragma, or name of the corresponding aspect for -- Name of the source pragma, or name of the corresponding aspect for
...@@ -10535,7 +10535,7 @@ package body Sem_Prag is ...@@ -10535,7 +10535,7 @@ package body Sem_Prag is
if Should_Ignore_Pragma_Sem (N) if Should_Ignore_Pragma_Sem (N)
or else (Prag_Id = Pragma_Default_Scalar_Storage_Order or else (Prag_Id = Pragma_Default_Scalar_Storage_Order
and then Ignore_Rep_Clauses) and then Ignore_Rep_Clauses)
then then
return; return;
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