mirror of
git://gcc.gnu.org/git/gcc.git
synced 2025-03-26 16:51:01 +08:00
[multiple changes]
2017-04-27 Eric Botcazou <ebotcazou@adacore.com> * fe.h (Warn_On_Questionable_Layout): Declare. * warnsw.ads (Warn_On_Record_Holes): Move down. (Warn_On_Questionable_Layout): New boolean variable. (Warning_Record): Add Warn_On_Questionable_Layout field. * warnsw.adb (All_Warnings): Set Warn_On_Questionable_Layout. (Restore_Warnings): Likewise. (Save_Warnings): Likewise. (Set_Dot_Warning_Switch): Handle 'q' and 'Q' letters. * gcc-interface/decl.c (gnat_to_gnu_entity): Adjust call to components_to_record. (gnu_field_to_gnat): New function. (warn_on_field_placement): Likewise. (components_to_record): Add GNAT_RECORD_TYPE and remove REORDER parameters. Rename local variables and adjust recursive call. Rework final scan of the field list and implement warnings on the problematic placement of specific sorts of fields. 2017-04-27 Bob Duff <duff@adacore.com> * errout.adb, exp_aggr.adb, exp_attr.adb, exp_code.adb, fname.adb, * fname.ads, freeze.adb, inline.adb, lib.adb, lib.ads, lib-list.adb, * lib-load.adb, lib-writ.adb, par.adb, restrict.adb, rtsfind.adb, * sem.adb, sem_cat.adb, sem_ch10.adb, sem_ch12.adb, sem_ch3.adb, * sem_ch4.adb, sem_ch6.adb, sem_ch8.adb, sem_ch9.adb, sem_elab.adb, * sem_intr.adb, sem_res.adb, sem_util.adb, sem_warn.adb, sprint.adb: For efficiency, cache results of Is_Internal_File_Name and Is_Predefined_File_Name in the Units table. This avoids a lot of repeated text processing. 2017-04-27 Emmanuel Briot <briot@adacore.com> * g-comlin.adb (Sort_Sections): remove useless test. 2017-04-27 Claire Dross <dross@adacore.com> * a-cfhase.adb, a-cfhase.ads (=): Generic parameter removed to allow the use of regular equality over elements in contracts. (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. (No_Overlap): Removed, model functions should be used instead. (Equivalent_Keys): Functions over cursors are removed. They were awkward with explicit container parameters. * a-cforse.adb, a-cforse.ads (=): Generic parameter removed to allow the use of regular equality over elements in contracts. (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. (No_Overlap): Removed, model functions should be used instead. 2017-04-27 Yannick Moy <moy@adacore.com> * gnat1drv.adb: Code cleanup. 2017-04-27 Ed Schonberg <schonberg@adacore.com> * exp_util.adb (Replace_Entity): The prefix of a 'Result attribute reference in a post- condition is the subprogram to which the condition applies. If the condition is inherited by a type extension, the prefix becomes a reference to the inherited operation, but there is no need to create a wrapper for this operation, because 'Result is expanded independently when elaborating the postconditions. From-SVN: r247338
This commit is contained in:
parent
a216846295
commit
8ab31c0c31
@ -1,3 +1,73 @@
|
||||
2017-04-27 Eric Botcazou <ebotcazou@adacore.com>
|
||||
|
||||
* fe.h (Warn_On_Questionable_Layout): Declare.
|
||||
* warnsw.ads (Warn_On_Record_Holes): Move down.
|
||||
(Warn_On_Questionable_Layout): New boolean variable.
|
||||
(Warning_Record): Add Warn_On_Questionable_Layout field.
|
||||
* warnsw.adb (All_Warnings): Set Warn_On_Questionable_Layout.
|
||||
(Restore_Warnings): Likewise.
|
||||
(Save_Warnings): Likewise.
|
||||
(Set_Dot_Warning_Switch): Handle 'q' and 'Q' letters.
|
||||
* gcc-interface/decl.c (gnat_to_gnu_entity): Adjust call to
|
||||
components_to_record.
|
||||
(gnu_field_to_gnat): New function.
|
||||
(warn_on_field_placement): Likewise.
|
||||
(components_to_record): Add GNAT_RECORD_TYPE and remove REORDER
|
||||
parameters. Rename local variables and adjust recursive call.
|
||||
Rework final scan of the field list and implement warnings on the
|
||||
problematic placement of specific sorts of fields.
|
||||
|
||||
2017-04-27 Bob Duff <duff@adacore.com>
|
||||
|
||||
* errout.adb, exp_aggr.adb, exp_attr.adb, exp_code.adb, fname.adb,
|
||||
* fname.ads, freeze.adb, inline.adb, lib.adb, lib.ads, lib-list.adb,
|
||||
* lib-load.adb, lib-writ.adb, par.adb, restrict.adb, rtsfind.adb,
|
||||
* sem.adb, sem_cat.adb, sem_ch10.adb, sem_ch12.adb, sem_ch3.adb,
|
||||
* sem_ch4.adb, sem_ch6.adb, sem_ch8.adb, sem_ch9.adb, sem_elab.adb,
|
||||
* sem_intr.adb, sem_res.adb, sem_util.adb, sem_warn.adb, sprint.adb:
|
||||
For efficiency, cache results of Is_Internal_File_Name and
|
||||
Is_Predefined_File_Name in the Units table. This avoids a lot
|
||||
of repeated text processing.
|
||||
|
||||
2017-04-27 Emmanuel Briot <briot@adacore.com>
|
||||
|
||||
* g-comlin.adb (Sort_Sections): remove useless test.
|
||||
|
||||
2017-04-27 Claire Dross <dross@adacore.com>
|
||||
|
||||
* a-cfhase.adb, a-cfhase.ads (=): Generic parameter removed to
|
||||
allow the use of regular equality over elements in contracts.
|
||||
(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.
|
||||
(No_Overlap): Removed, model functions should be used instead.
|
||||
(Equivalent_Keys): Functions over cursors are removed. They were
|
||||
awkward with explicit container parameters.
|
||||
* a-cforse.adb, a-cforse.ads (=): Generic parameter removed to
|
||||
allow the use of regular equality over elements in contracts.
|
||||
(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.
|
||||
(No_Overlap): Removed, model functions should be used instead.
|
||||
|
||||
2017-04-27 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* gnat1drv.adb: Code cleanup.
|
||||
|
||||
2017-04-27 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* exp_util.adb (Replace_Entity): The prefix of a 'Result
|
||||
attribute reference in a post- condition is the subprogram to
|
||||
which the condition applies. If the condition is inherited
|
||||
by a type extension, the prefix becomes a reference to the
|
||||
inherited operation, but there is no need to create a wrapper
|
||||
for this operation, because 'Result is expanded independently
|
||||
when elaborating the postconditions.
|
||||
|
||||
2017-04-27 Bob Duff <duff@adacore.com>
|
||||
|
||||
* sinput.adb: Minor code cleanup.
|
||||
|
@ -847,6 +847,45 @@ is
|
||||
|
||||
package body Generic_Sorting with SPARK_Mode => Off is
|
||||
|
||||
------------------
|
||||
-- Formal_Model --
|
||||
------------------
|
||||
|
||||
package body Formal_Model is
|
||||
|
||||
-----------------------
|
||||
-- M_Elements_Sorted --
|
||||
-----------------------
|
||||
|
||||
function M_Elements_Sorted (Container : M.Sequence) return Boolean is
|
||||
begin
|
||||
if M.Length (Container) = 0 then
|
||||
return True;
|
||||
end if;
|
||||
|
||||
declare
|
||||
E1 : Element_Type := Element (Container, 1);
|
||||
|
||||
begin
|
||||
for I in 2 .. M.Length (Container) loop
|
||||
declare
|
||||
E2 : constant Element_Type := Element (Container, I);
|
||||
|
||||
begin
|
||||
if E2 < E1 then
|
||||
return False;
|
||||
end if;
|
||||
|
||||
E1 := E2;
|
||||
end;
|
||||
end loop;
|
||||
end;
|
||||
|
||||
return True;
|
||||
end M_Elements_Sorted;
|
||||
|
||||
end Formal_Model;
|
||||
|
||||
---------------
|
||||
-- Is_Sorted --
|
||||
---------------
|
||||
@ -867,37 +906,6 @@ is
|
||||
return True;
|
||||
end Is_Sorted;
|
||||
|
||||
-----------------------
|
||||
-- M_Elements_Sorted --
|
||||
-----------------------
|
||||
|
||||
function M_Elements_Sorted (Container : M.Sequence) return Boolean is
|
||||
begin
|
||||
if M.Length (Container) = 0 then
|
||||
return True;
|
||||
end if;
|
||||
|
||||
declare
|
||||
E1 : Element_Type := Element (Container, 1);
|
||||
|
||||
begin
|
||||
for I in 2 .. M.Length (Container) loop
|
||||
declare
|
||||
E2 : constant Element_Type := Element (Container, I);
|
||||
|
||||
begin
|
||||
if E2 < E1 then
|
||||
return False;
|
||||
end if;
|
||||
|
||||
E1 := E2;
|
||||
end;
|
||||
end loop;
|
||||
end;
|
||||
|
||||
return True;
|
||||
end M_Elements_Sorted;
|
||||
|
||||
-----------
|
||||
-- Merge --
|
||||
-----------
|
||||
|
@ -1408,8 +1408,8 @@ is
|
||||
Has_Element (Container, Position) or else Position = No_Element,
|
||||
Contract_Cases =>
|
||||
|
||||
-- If Item is not is not contained in Container after Position, Find
|
||||
-- returns No_Element.
|
||||
-- If Item is not contained in Container after Position, Find returns
|
||||
-- No_Element.
|
||||
|
||||
(not M.Contains
|
||||
(Container => Model (Container),
|
||||
@ -1423,7 +1423,7 @@ is
|
||||
=>
|
||||
Find'Result = No_Element,
|
||||
|
||||
-- Otherwise, Find returns a valid cusror in Container
|
||||
-- Otherwise, Find returns a valid cursor in Container
|
||||
|
||||
others =>
|
||||
P.Has_Key (Positions (Container), Find'Result)
|
||||
@ -1463,8 +1463,8 @@ is
|
||||
Has_Element (Container, Position) or else Position = No_Element,
|
||||
Contract_Cases =>
|
||||
|
||||
-- If Item is not is not contained in Container before Position, Find
|
||||
-- returns No_Element.
|
||||
-- If Item is not contained in Container before Position, Find returns
|
||||
-- No_Element.
|
||||
|
||||
(not M.Contains
|
||||
(Container => Model (Container),
|
||||
@ -1478,7 +1478,7 @@ is
|
||||
=>
|
||||
Reverse_Find'Result = No_Element,
|
||||
|
||||
-- Otherwise, Find returns a valid cusror in Container
|
||||
-- Otherwise, Find returns a valid cursor in Container
|
||||
|
||||
others =>
|
||||
P.Has_Key (Positions (Container), Reverse_Find'Result)
|
||||
@ -1533,16 +1533,21 @@ is
|
||||
with function "<" (Left, Right : Element_Type) return Boolean is <>;
|
||||
|
||||
package Generic_Sorting with SPARK_Mode is
|
||||
function M_Elements_Sorted (Container : M.Sequence) return Boolean with
|
||||
Ghost,
|
||||
Global => null,
|
||||
Post =>
|
||||
M_Elements_Sorted'Result =
|
||||
(for all I in 1 .. M.Length (Container) =>
|
||||
(for all J in I .. M.Length (Container) =>
|
||||
Element (Container, I) = Element (Container, J)
|
||||
or Element (Container, I) < Element (Container, J)));
|
||||
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
|
||||
|
||||
package Formal_Model with Ghost is
|
||||
function M_Elements_Sorted (Container : M.Sequence) return Boolean
|
||||
with
|
||||
Global => null,
|
||||
Post =>
|
||||
M_Elements_Sorted'Result =
|
||||
(for all I in 1 .. M.Length (Container) =>
|
||||
(for all J in I .. M.Length (Container) =>
|
||||
Element (Container, I) = Element (Container, J)
|
||||
or Element (Container, I) < Element (Container, J)));
|
||||
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
|
||||
|
||||
end Formal_Model;
|
||||
use Formal_Model;
|
||||
|
||||
function Is_Sorted (Container : List) return Boolean with
|
||||
Global => null,
|
||||
|
@ -366,6 +366,39 @@ is
|
||||
|
||||
package body Formal_Model is
|
||||
|
||||
----------
|
||||
-- Find --
|
||||
----------
|
||||
|
||||
function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
|
||||
is
|
||||
begin
|
||||
for I in 1 .. K.Length (Container) loop
|
||||
if Equivalent_Keys (Key, K.Get (Container, I)) then
|
||||
return I;
|
||||
end if;
|
||||
end loop;
|
||||
return 0;
|
||||
end Find;
|
||||
|
||||
---------------------
|
||||
-- K_Keys_Included --
|
||||
---------------------
|
||||
|
||||
function K_Keys_Included (Left : K.Sequence;
|
||||
Right : K.Sequence) return Boolean
|
||||
is
|
||||
begin
|
||||
for I in 1 .. K.Length (Left) loop
|
||||
if not K.Contains (Right, 1, K.Length (Right), K.Get (Left, I))
|
||||
then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
|
||||
return True;
|
||||
end K_Keys_Included;
|
||||
|
||||
----------
|
||||
-- Keys --
|
||||
----------
|
||||
|
@ -56,7 +56,9 @@ generic
|
||||
type Element_Type is private;
|
||||
|
||||
with function Hash (Key : Key_Type) return Hash_Type;
|
||||
with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
|
||||
with function Equivalent_Keys
|
||||
(Left : Key_Type;
|
||||
Right : Key_Type) return Boolean is "=";
|
||||
|
||||
package Ada.Containers.Formal_Hashed_Maps with
|
||||
SPARK_Mode
|
||||
@ -117,6 +119,30 @@ is
|
||||
(Left : K.Sequence;
|
||||
Right : K.Sequence) return Boolean renames K."<=";
|
||||
|
||||
function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
|
||||
-- Search for Key in Container
|
||||
|
||||
with
|
||||
Global => null,
|
||||
Post =>
|
||||
(if Find'Result > 0 then
|
||||
Find'Result <= K.Length (Container)
|
||||
and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
|
||||
|
||||
function K_Keys_Included
|
||||
(Left : K.Sequence;
|
||||
Right : K.Sequence) return Boolean
|
||||
-- Return True if Right contains all the keys of Left
|
||||
|
||||
with
|
||||
Global => null,
|
||||
Post =>
|
||||
K_Keys_Included'Result =
|
||||
(for all I in 1 .. K.Length (Left) =>
|
||||
Find (Right, K.Get (Left, I)) > 0
|
||||
and then K.Get (Right, Find (Right, K.Get (Left, I))) =
|
||||
K.Get (Left, I));
|
||||
|
||||
package P is new Ada.Containers.Functional_Maps
|
||||
(Key_Type => Cursor,
|
||||
Element_Type => Positive_Count_Type,
|
||||
@ -137,7 +163,6 @@ is
|
||||
P_Left : P.Map;
|
||||
P_Right : P.Map) return Boolean
|
||||
with
|
||||
Ghost,
|
||||
Global => null,
|
||||
Post =>
|
||||
(if Mapping_Preserved'Result then
|
||||
@ -146,6 +171,10 @@ is
|
||||
|
||||
P.Keys_Included (P_Left, P_Right)
|
||||
|
||||
-- Right contains all the keys of Left
|
||||
|
||||
and K_Keys_Included (K_Left, K_Right)
|
||||
|
||||
-- Mappings from cursors to elements induced by K_Left, P_Left
|
||||
-- and K_Right, P_Right are the same.
|
||||
|
||||
@ -179,10 +208,15 @@ is
|
||||
-- It contains all the keys contained in Model
|
||||
|
||||
and (for all Key of Model (Container) =>
|
||||
(for some L of Keys'Result => Equivalent_Keys (L, Key)))
|
||||
(Find (Keys'Result, Key) > 0
|
||||
and then Equivalent_Keys
|
||||
(K.Get (Keys'Result, Find (Keys'Result, Key)), Key)))
|
||||
|
||||
-- It has no duplicate
|
||||
|
||||
and (for all I in 1 .. Length (Container) =>
|
||||
Find (Keys'Result, K.Get (Keys'Result, I)) = I)
|
||||
|
||||
and (for all I in 1 .. Length (Container) =>
|
||||
(for all J in 1 .. Length (Container) =>
|
||||
(if Equivalent_Keys
|
||||
@ -259,7 +293,14 @@ is
|
||||
with
|
||||
Global => null,
|
||||
Pre => Capacity <= Container.Capacity,
|
||||
Post => Model (Container) = Model (Container)'Old;
|
||||
Post =>
|
||||
Model (Container) = Model (Container)'Old
|
||||
and Length (Container)'Old = Length (Container)
|
||||
|
||||
-- Actual keys are preserved
|
||||
|
||||
and K_Keys_Included (Keys (Container), Keys (Container)'Old)
|
||||
and K_Keys_Included (Keys (Container)'Old, Keys (Container));
|
||||
|
||||
function Is_Empty (Container : Map) return Boolean with
|
||||
Global => null,
|
||||
@ -278,8 +319,8 @@ is
|
||||
|
||||
-- Actual keys are preserved
|
||||
|
||||
and (for all Key of Keys (Source) =>
|
||||
Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key);
|
||||
and K_Keys_Included (Keys (Target), Keys (Source))
|
||||
and K_Keys_Included (Keys (Source), Keys (Target));
|
||||
|
||||
function Copy
|
||||
(Source : Map;
|
||||
@ -355,8 +396,8 @@ is
|
||||
|
||||
-- Actual keys are preserved
|
||||
|
||||
and (for all Key of Keys (Source)'Old =>
|
||||
Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key);
|
||||
and K_Keys_Included (Keys (Target), Keys (Source)'Old)
|
||||
and K_Keys_Included (Keys (Source)'Old, Keys (Target));
|
||||
|
||||
procedure Insert
|
||||
(Container : in out Map;
|
||||
@ -700,7 +741,7 @@ is
|
||||
Global => null,
|
||||
Contract_Cases =>
|
||||
|
||||
-- If Key is not is not contained in Container, Find returns No_Element
|
||||
-- If Key is not contained in Container, Find returns No_Element
|
||||
|
||||
(not Contains (Model (Container), Key) =>
|
||||
Find'Result = No_Element,
|
||||
@ -709,6 +750,8 @@ is
|
||||
|
||||
others =>
|
||||
P.Has_Key (Positions (Container), Find'Result)
|
||||
and P.Get (Positions (Container), Find'Result) =
|
||||
Find (Keys (Container), Key)
|
||||
|
||||
-- The key designated by the result of Find is Key
|
||||
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 2010-2015, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 2010-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- --
|
||||
@ -263,35 +263,6 @@ is
|
||||
return Target;
|
||||
end Copy;
|
||||
|
||||
---------------------
|
||||
-- Current_To_Last --
|
||||
---------------------
|
||||
|
||||
function Current_To_Last (Container : Set; Current : Cursor) return Set is
|
||||
Curs : Cursor := First (Container);
|
||||
C : Set (Container.Capacity, Container.Modulus) :=
|
||||
Copy (Container, Container.Capacity);
|
||||
Node : Count_Type;
|
||||
|
||||
begin
|
||||
if Curs = No_Element then
|
||||
Clear (C);
|
||||
return C;
|
||||
|
||||
elsif Current /= No_Element and not Has_Element (Container, Current) then
|
||||
raise Constraint_Error;
|
||||
|
||||
else
|
||||
while Curs.Node /= Current.Node loop
|
||||
Node := Curs.Node;
|
||||
Delete (C, Curs);
|
||||
Curs := Next (Container, (Node => Node));
|
||||
end loop;
|
||||
|
||||
return C;
|
||||
end if;
|
||||
end Current_To_Last;
|
||||
|
||||
---------------------
|
||||
-- Default_Modulus --
|
||||
---------------------
|
||||
@ -521,83 +492,6 @@ is
|
||||
return Is_Equivalent (Left, Right);
|
||||
end Equivalent_Sets;
|
||||
|
||||
-------------------------
|
||||
-- Equivalent_Elements --
|
||||
-------------------------
|
||||
|
||||
function Equivalent_Elements
|
||||
(Left : Set;
|
||||
CLeft : Cursor;
|
||||
Right : Set;
|
||||
CRight : Cursor) return Boolean
|
||||
is
|
||||
begin
|
||||
if not Has_Element (Left, CLeft) then
|
||||
raise Constraint_Error with
|
||||
"Left cursor of Equivalent_Elements has no element";
|
||||
end if;
|
||||
|
||||
if not Has_Element (Right, CRight) then
|
||||
raise Constraint_Error with
|
||||
"Right cursor of Equivalent_Elements has no element";
|
||||
end if;
|
||||
|
||||
pragma Assert (Vet (Left, CLeft),
|
||||
"bad Left cursor in Equivalent_Elements");
|
||||
pragma Assert (Vet (Right, CRight),
|
||||
"bad Right cursor in Equivalent_Elements");
|
||||
|
||||
declare
|
||||
LN : Node_Type renames Left.Nodes (CLeft.Node);
|
||||
RN : Node_Type renames Right.Nodes (CRight.Node);
|
||||
begin
|
||||
return Equivalent_Elements (LN.Element, RN.Element);
|
||||
end;
|
||||
end Equivalent_Elements;
|
||||
|
||||
function Equivalent_Elements
|
||||
(Left : Set;
|
||||
CLeft : Cursor;
|
||||
Right : Element_Type) return Boolean
|
||||
is
|
||||
begin
|
||||
if not Has_Element (Left, CLeft) then
|
||||
raise Constraint_Error with
|
||||
"Left cursor of Equivalent_Elements has no element";
|
||||
end if;
|
||||
|
||||
pragma Assert (Vet (Left, CLeft),
|
||||
"Left cursor in Equivalent_Elements is bad");
|
||||
|
||||
declare
|
||||
LN : Node_Type renames Left.Nodes (CLeft.Node);
|
||||
begin
|
||||
return Equivalent_Elements (LN.Element, Right);
|
||||
end;
|
||||
end Equivalent_Elements;
|
||||
|
||||
function Equivalent_Elements
|
||||
(Left : Element_Type;
|
||||
Right : Set;
|
||||
CRight : Cursor) return Boolean
|
||||
is
|
||||
begin
|
||||
if not Has_Element (Right, CRight) then
|
||||
raise Constraint_Error with
|
||||
"Right cursor of Equivalent_Elements has no element";
|
||||
end if;
|
||||
|
||||
pragma Assert
|
||||
(Vet (Right, CRight),
|
||||
"Right cursor of Equivalent_Elements is bad");
|
||||
|
||||
declare
|
||||
RN : Node_Type renames Right.Nodes (CRight.Node);
|
||||
begin
|
||||
return Equivalent_Elements (Left, RN.Element);
|
||||
end;
|
||||
end Equivalent_Elements;
|
||||
|
||||
---------------------
|
||||
-- Equivalent_Keys --
|
||||
---------------------
|
||||
@ -657,36 +551,221 @@ is
|
||||
return (Node => Node);
|
||||
end First;
|
||||
|
||||
-----------------------
|
||||
-- First_To_Previous --
|
||||
-----------------------
|
||||
------------------
|
||||
-- Formal_Model --
|
||||
------------------
|
||||
|
||||
function First_To_Previous
|
||||
(Container : Set;
|
||||
Current : Cursor) return Set
|
||||
is
|
||||
Curs : Cursor := Current;
|
||||
C : Set (Container.Capacity, Container.Modulus) :=
|
||||
Copy (Container, Container.Capacity);
|
||||
Node : Count_Type;
|
||||
package body Formal_Model is
|
||||
|
||||
begin
|
||||
if Curs = No_Element then
|
||||
return C;
|
||||
-------------------------
|
||||
-- E_Elements_Included --
|
||||
-------------------------
|
||||
|
||||
elsif not Has_Element (Container, Curs) then
|
||||
raise Constraint_Error;
|
||||
|
||||
else
|
||||
while Curs.Node /= 0 loop
|
||||
Node := Curs.Node;
|
||||
Delete (C, Curs);
|
||||
Curs := Next (Container, (Node => Node));
|
||||
function E_Elements_Included
|
||||
(Left : E.Sequence;
|
||||
Right : E.Sequence) return Boolean
|
||||
is
|
||||
begin
|
||||
for I in 1 .. E.Length (Left) loop
|
||||
if not E.Contains (Right, 1, E.Length (Right), E.Get (Left, I))
|
||||
then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
|
||||
return C;
|
||||
end if;
|
||||
end First_To_Previous;
|
||||
return True;
|
||||
end E_Elements_Included;
|
||||
|
||||
function E_Elements_Included
|
||||
(Left : E.Sequence;
|
||||
Model : M.Set;
|
||||
Right : E.Sequence) return Boolean
|
||||
is
|
||||
begin
|
||||
for I in 1 .. E.Length (Left) loop
|
||||
declare
|
||||
Item : constant Element_Type := E.Get (Left, I);
|
||||
begin
|
||||
if M.Contains (Model, Item) then
|
||||
if not E.Contains (Right, 1, E.Length (Right), Item) then
|
||||
return False;
|
||||
end if;
|
||||
end if;
|
||||
end;
|
||||
end loop;
|
||||
|
||||
return True;
|
||||
end E_Elements_Included;
|
||||
|
||||
function E_Elements_Included
|
||||
(Container : E.Sequence;
|
||||
Model : M.Set;
|
||||
Left : E.Sequence;
|
||||
Right : E.Sequence) return Boolean
|
||||
is
|
||||
begin
|
||||
for I in 1 .. E.Length (Container) loop
|
||||
declare
|
||||
Item : constant Element_Type := E.Get (Container, I);
|
||||
begin
|
||||
if M.Contains (Model, Item) then
|
||||
if not E.Contains (Left, 1, E.Length (Left), Item) then
|
||||
return False;
|
||||
end if;
|
||||
else
|
||||
if not E.Contains (Right, 1, E.Length (Right), Item) then
|
||||
return False;
|
||||
end if;
|
||||
end if;
|
||||
end;
|
||||
end loop;
|
||||
|
||||
return True;
|
||||
end E_Elements_Included;
|
||||
|
||||
----------
|
||||
-- Find --
|
||||
----------
|
||||
|
||||
function Find
|
||||
(Container : E.Sequence;
|
||||
Item : Element_Type) return Count_Type
|
||||
is
|
||||
begin
|
||||
for I in 1 .. E.Length (Container) loop
|
||||
if Equivalent_Elements (Item, E.Get (Container, I)) then
|
||||
return I;
|
||||
end if;
|
||||
end loop;
|
||||
return 0;
|
||||
end Find;
|
||||
|
||||
--------------
|
||||
-- Elements --
|
||||
--------------
|
||||
|
||||
function Elements (Container : Set) return E.Sequence is
|
||||
Position : Count_Type := HT_Ops.First (Container);
|
||||
R : E.Sequence;
|
||||
|
||||
begin
|
||||
-- Can't use First, Next or Element here, since they depend on models
|
||||
-- for their postconditions.
|
||||
|
||||
while Position /= 0 loop
|
||||
R := E.Add (R, Container.Nodes (Position).Element);
|
||||
Position := HT_Ops.Next (Container, Position);
|
||||
end loop;
|
||||
|
||||
return R;
|
||||
end Elements;
|
||||
|
||||
----------------------------
|
||||
-- Lift_Abstraction_Level --
|
||||
----------------------------
|
||||
|
||||
procedure Lift_Abstraction_Level (Container : Set) is null;
|
||||
|
||||
-----------------------
|
||||
-- Mapping_Preserved --
|
||||
-----------------------
|
||||
|
||||
function Mapping_Preserved
|
||||
(E_Left : E.Sequence;
|
||||
E_Right : E.Sequence;
|
||||
P_Left : P.Map;
|
||||
P_Right : P.Map) return Boolean
|
||||
is
|
||||
begin
|
||||
for C of P_Left loop
|
||||
if not P.Has_Key (P_Right, C)
|
||||
or else P.Get (P_Left, C) > E.Length (E_Left)
|
||||
or else P.Get (P_Right, C) > E.Length (E_Right)
|
||||
or else E.Get (E_Left, P.Get (P_Left, C)) /=
|
||||
E.Get (E_Right, P.Get (P_Right, C))
|
||||
then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
|
||||
return True;
|
||||
end Mapping_Preserved;
|
||||
|
||||
------------------------------
|
||||
-- Mapping_Preserved_Except --
|
||||
------------------------------
|
||||
|
||||
function Mapping_Preserved_Except
|
||||
(E_Left : E.Sequence;
|
||||
E_Right : E.Sequence;
|
||||
P_Left : P.Map;
|
||||
P_Right : P.Map;
|
||||
Position : Cursor) return Boolean
|
||||
is
|
||||
begin
|
||||
for C of P_Left loop
|
||||
if C /= Position
|
||||
and (not P.Has_Key (P_Right, C)
|
||||
or else P.Get (P_Left, C) > E.Length (E_Left)
|
||||
or else P.Get (P_Right, C) > E.Length (E_Right)
|
||||
or else E.Get (E_Left, P.Get (P_Left, C)) /=
|
||||
E.Get (E_Right, P.Get (P_Right, C)))
|
||||
then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
|
||||
return True;
|
||||
end Mapping_Preserved_Except;
|
||||
|
||||
-----------
|
||||
-- Model --
|
||||
-----------
|
||||
|
||||
function Model (Container : Set) return M.Set is
|
||||
Position : Count_Type := HT_Ops.First (Container);
|
||||
R : M.Set;
|
||||
|
||||
begin
|
||||
-- Can't use First, Next or Element here, since they depend on models
|
||||
-- for their postconditions.
|
||||
|
||||
while Position /= 0 loop
|
||||
R :=
|
||||
M.Add
|
||||
(Container => R,
|
||||
Item => Container.Nodes (Position).Element);
|
||||
|
||||
Position := HT_Ops.Next (Container, Position);
|
||||
end loop;
|
||||
|
||||
return R;
|
||||
end Model;
|
||||
|
||||
---------------
|
||||
-- Positions --
|
||||
---------------
|
||||
|
||||
function Positions (Container : Set) return P.Map is
|
||||
I : Count_Type := 1;
|
||||
Position : Count_Type := HT_Ops.First (Container);
|
||||
R : P.Map;
|
||||
|
||||
begin
|
||||
-- Can't use First, Next or Element here, since they depend on models
|
||||
-- for their postconditions.
|
||||
|
||||
while Position /= 0 loop
|
||||
R := P.Add (R, (Node => Position), I);
|
||||
pragma Assert (P.Length (R) = I);
|
||||
Position := HT_Ops.Next (Container, Position);
|
||||
I := I + 1;
|
||||
end loop;
|
||||
|
||||
return R;
|
||||
end Positions;
|
||||
|
||||
end Formal_Model;
|
||||
|
||||
----------
|
||||
-- Free --
|
||||
@ -715,6 +794,190 @@ is
|
||||
HT.Nodes (Node).Has_Element := True;
|
||||
end Generic_Allocate;
|
||||
|
||||
package body Generic_Keys with SPARK_Mode => Off is
|
||||
|
||||
-----------------------
|
||||
-- Local Subprograms --
|
||||
-----------------------
|
||||
|
||||
function Equivalent_Key_Node
|
||||
(Key : Key_Type;
|
||||
Node : Node_Type) return Boolean;
|
||||
pragma Inline (Equivalent_Key_Node);
|
||||
|
||||
--------------------------
|
||||
-- Local Instantiations --
|
||||
--------------------------
|
||||
|
||||
package Key_Keys is
|
||||
new Hash_Tables.Generic_Bounded_Keys
|
||||
(HT_Types => HT_Types,
|
||||
Next => Next,
|
||||
Set_Next => Set_Next,
|
||||
Key_Type => Key_Type,
|
||||
Hash => Hash,
|
||||
Equivalent_Keys => Equivalent_Key_Node);
|
||||
|
||||
--------------
|
||||
-- Contains --
|
||||
--------------
|
||||
|
||||
function Contains
|
||||
(Container : Set;
|
||||
Key : Key_Type) return Boolean
|
||||
is
|
||||
begin
|
||||
return Find (Container, Key) /= No_Element;
|
||||
end Contains;
|
||||
|
||||
------------
|
||||
-- Delete --
|
||||
------------
|
||||
|
||||
procedure Delete
|
||||
(Container : in out Set;
|
||||
Key : Key_Type)
|
||||
is
|
||||
X : Count_Type;
|
||||
|
||||
begin
|
||||
Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
|
||||
|
||||
if X = 0 then
|
||||
raise Constraint_Error with "attempt to delete key not in set";
|
||||
end if;
|
||||
|
||||
Free (Container, X);
|
||||
end Delete;
|
||||
|
||||
-------------
|
||||
-- Element --
|
||||
-------------
|
||||
|
||||
function Element
|
||||
(Container : Set;
|
||||
Key : Key_Type) return Element_Type
|
||||
is
|
||||
Node : constant Count_Type := Find (Container, Key).Node;
|
||||
|
||||
begin
|
||||
if Node = 0 then
|
||||
raise Constraint_Error with "key not in map";
|
||||
end if;
|
||||
|
||||
return Container.Nodes (Node).Element;
|
||||
end Element;
|
||||
|
||||
-------------------------
|
||||
-- Equivalent_Key_Node --
|
||||
-------------------------
|
||||
|
||||
function Equivalent_Key_Node
|
||||
(Key : Key_Type;
|
||||
Node : Node_Type) return Boolean
|
||||
is
|
||||
begin
|
||||
return Equivalent_Keys (Key, Generic_Keys.Key (Node.Element));
|
||||
end Equivalent_Key_Node;
|
||||
|
||||
-------------
|
||||
-- Exclude --
|
||||
-------------
|
||||
|
||||
procedure Exclude
|
||||
(Container : in out Set;
|
||||
Key : Key_Type)
|
||||
is
|
||||
X : Count_Type;
|
||||
begin
|
||||
Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
|
||||
Free (Container, X);
|
||||
end Exclude;
|
||||
|
||||
----------
|
||||
-- Find --
|
||||
----------
|
||||
|
||||
function Find
|
||||
(Container : Set;
|
||||
Key : Key_Type) return Cursor
|
||||
is
|
||||
Node : constant Count_Type := Key_Keys.Find (Container, Key);
|
||||
begin
|
||||
return (if Node = 0 then No_Element else (Node => Node));
|
||||
end Find;
|
||||
|
||||
------------------
|
||||
-- Formal_Model --
|
||||
------------------
|
||||
|
||||
package body Formal_Model is
|
||||
|
||||
-----------------------
|
||||
-- M_Included_Except --
|
||||
-----------------------
|
||||
|
||||
function M_Included_Except
|
||||
(Left : M.Set;
|
||||
Right : M.Set;
|
||||
Key : Key_Type) return Boolean
|
||||
is
|
||||
begin
|
||||
for E of Left loop
|
||||
if not Contains (Right, E)
|
||||
and not Equivalent_Keys (Generic_Keys.Key (E), Key)
|
||||
then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
return True;
|
||||
end M_Included_Except;
|
||||
|
||||
end Formal_Model;
|
||||
|
||||
---------
|
||||
-- Key --
|
||||
---------
|
||||
|
||||
function Key (Container : Set; Position : Cursor) return Key_Type is
|
||||
begin
|
||||
if not Has_Element (Container, Position) then
|
||||
raise Constraint_Error with
|
||||
"Position cursor has no element";
|
||||
end if;
|
||||
|
||||
pragma Assert
|
||||
(Vet (Container, Position), "bad cursor in function Key");
|
||||
|
||||
declare
|
||||
N : Node_Type renames Container.Nodes (Position.Node);
|
||||
begin
|
||||
return Key (N.Element);
|
||||
end;
|
||||
end Key;
|
||||
|
||||
-------------
|
||||
-- Replace --
|
||||
-------------
|
||||
|
||||
procedure Replace
|
||||
(Container : in out Set;
|
||||
Key : Key_Type;
|
||||
New_Item : Element_Type)
|
||||
is
|
||||
Node : constant Count_Type := Key_Keys.Find (Container, Key);
|
||||
|
||||
begin
|
||||
if Node = 0 then
|
||||
raise Constraint_Error with
|
||||
"attempt to replace key not in set";
|
||||
end if;
|
||||
|
||||
Replace_Element (Container, Node, New_Item);
|
||||
end Replace;
|
||||
|
||||
end Generic_Keys;
|
||||
|
||||
-----------------
|
||||
-- Has_Element --
|
||||
-----------------
|
||||
@ -1158,34 +1421,6 @@ is
|
||||
Node.Next := Next;
|
||||
end Set_Next;
|
||||
|
||||
------------------
|
||||
-- Strict_Equal --
|
||||
------------------
|
||||
|
||||
function Strict_Equal (Left, Right : Set) return Boolean is
|
||||
CuL : Cursor := First (Left);
|
||||
CuR : Cursor := First (Right);
|
||||
|
||||
begin
|
||||
if Length (Left) /= Length (Right) then
|
||||
return False;
|
||||
end if;
|
||||
|
||||
while CuL.Node /= 0 or CuR.Node /= 0 loop
|
||||
if CuL.Node /= CuR.Node
|
||||
or else Left.Nodes (CuL.Node).Element /=
|
||||
Right.Nodes (CuR.Node).Element
|
||||
then
|
||||
return False;
|
||||
end if;
|
||||
|
||||
CuL := Next (Left, CuL);
|
||||
CuR := Next (Right, CuR);
|
||||
end loop;
|
||||
|
||||
return True;
|
||||
end Strict_Equal;
|
||||
|
||||
--------------------------
|
||||
-- Symmetric_Difference --
|
||||
--------------------------
|
||||
@ -1386,160 +1621,4 @@ is
|
||||
end;
|
||||
end Vet;
|
||||
|
||||
package body Generic_Keys with SPARK_Mode => Off is
|
||||
|
||||
-----------------------
|
||||
-- Local Subprograms --
|
||||
-----------------------
|
||||
|
||||
function Equivalent_Key_Node
|
||||
(Key : Key_Type;
|
||||
Node : Node_Type) return Boolean;
|
||||
pragma Inline (Equivalent_Key_Node);
|
||||
|
||||
--------------------------
|
||||
-- Local Instantiations --
|
||||
--------------------------
|
||||
|
||||
package Key_Keys is
|
||||
new Hash_Tables.Generic_Bounded_Keys
|
||||
(HT_Types => HT_Types,
|
||||
Next => Next,
|
||||
Set_Next => Set_Next,
|
||||
Key_Type => Key_Type,
|
||||
Hash => Hash,
|
||||
Equivalent_Keys => Equivalent_Key_Node);
|
||||
|
||||
--------------
|
||||
-- Contains --
|
||||
--------------
|
||||
|
||||
function Contains
|
||||
(Container : Set;
|
||||
Key : Key_Type) return Boolean
|
||||
is
|
||||
begin
|
||||
return Find (Container, Key) /= No_Element;
|
||||
end Contains;
|
||||
|
||||
------------
|
||||
-- Delete --
|
||||
------------
|
||||
|
||||
procedure Delete
|
||||
(Container : in out Set;
|
||||
Key : Key_Type)
|
||||
is
|
||||
X : Count_Type;
|
||||
|
||||
begin
|
||||
Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
|
||||
|
||||
if X = 0 then
|
||||
raise Constraint_Error with "attempt to delete key not in set";
|
||||
end if;
|
||||
|
||||
Free (Container, X);
|
||||
end Delete;
|
||||
|
||||
-------------
|
||||
-- Element --
|
||||
-------------
|
||||
|
||||
function Element
|
||||
(Container : Set;
|
||||
Key : Key_Type) return Element_Type
|
||||
is
|
||||
Node : constant Count_Type := Find (Container, Key).Node;
|
||||
|
||||
begin
|
||||
if Node = 0 then
|
||||
raise Constraint_Error with "key not in map";
|
||||
end if;
|
||||
|
||||
return Container.Nodes (Node).Element;
|
||||
end Element;
|
||||
|
||||
-------------------------
|
||||
-- Equivalent_Key_Node --
|
||||
-------------------------
|
||||
|
||||
function Equivalent_Key_Node
|
||||
(Key : Key_Type;
|
||||
Node : Node_Type) return Boolean
|
||||
is
|
||||
begin
|
||||
return Equivalent_Keys (Key, Generic_Keys.Key (Node.Element));
|
||||
end Equivalent_Key_Node;
|
||||
|
||||
-------------
|
||||
-- Exclude --
|
||||
-------------
|
||||
|
||||
procedure Exclude
|
||||
(Container : in out Set;
|
||||
Key : Key_Type)
|
||||
is
|
||||
X : Count_Type;
|
||||
begin
|
||||
Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
|
||||
Free (Container, X);
|
||||
end Exclude;
|
||||
|
||||
----------
|
||||
-- Find --
|
||||
----------
|
||||
|
||||
function Find
|
||||
(Container : Set;
|
||||
Key : Key_Type) return Cursor
|
||||
is
|
||||
Node : constant Count_Type := Key_Keys.Find (Container, Key);
|
||||
begin
|
||||
return (if Node = 0 then No_Element else (Node => Node));
|
||||
end Find;
|
||||
|
||||
---------
|
||||
-- Key --
|
||||
---------
|
||||
|
||||
function Key (Container : Set; Position : Cursor) return Key_Type is
|
||||
begin
|
||||
if not Has_Element (Container, Position) then
|
||||
raise Constraint_Error with
|
||||
"Position cursor has no element";
|
||||
end if;
|
||||
|
||||
pragma Assert
|
||||
(Vet (Container, Position), "bad cursor in function Key");
|
||||
|
||||
declare
|
||||
N : Node_Type renames Container.Nodes (Position.Node);
|
||||
begin
|
||||
return Key (N.Element);
|
||||
end;
|
||||
end Key;
|
||||
|
||||
-------------
|
||||
-- Replace --
|
||||
-------------
|
||||
|
||||
procedure Replace
|
||||
(Container : in out Set;
|
||||
Key : Key_Type;
|
||||
New_Item : Element_Type)
|
||||
is
|
||||
Node : constant Count_Type := Key_Keys.Find (Container, Key);
|
||||
|
||||
begin
|
||||
if Node = 0 then
|
||||
raise Constraint_Error with
|
||||
"attempt to replace key not in set";
|
||||
end if;
|
||||
|
||||
Replace_Element (Container, Node, New_Item);
|
||||
end Replace;
|
||||
|
||||
end Generic_Keys;
|
||||
|
||||
end Ada.Containers.Formal_Hashed_Sets;
|
||||
|
1230
gcc/ada/a-cfhase.ads
1230
gcc/ada/a-cfhase.ads
File diff suppressed because it is too large
Load Diff
@ -641,6 +641,45 @@ is
|
||||
|
||||
package body Generic_Sorting with SPARK_Mode => Off is
|
||||
|
||||
------------------
|
||||
-- Formal_Model --
|
||||
------------------
|
||||
|
||||
package body Formal_Model is
|
||||
|
||||
-----------------------
|
||||
-- M_Elements_Sorted --
|
||||
-----------------------
|
||||
|
||||
function M_Elements_Sorted (Container : M.Sequence) return Boolean is
|
||||
begin
|
||||
if M.Length (Container) = 0 then
|
||||
return True;
|
||||
end if;
|
||||
|
||||
declare
|
||||
E1 : Element_Type := Element (Container, Index_Type'First);
|
||||
|
||||
begin
|
||||
for I in Index_Type'First + 1 .. M.Last (Container) loop
|
||||
declare
|
||||
E2 : constant Element_Type := Element (Container, I);
|
||||
|
||||
begin
|
||||
if E2 < E1 then
|
||||
return False;
|
||||
end if;
|
||||
|
||||
E1 := E2;
|
||||
end;
|
||||
end loop;
|
||||
end;
|
||||
|
||||
return True;
|
||||
end M_Elements_Sorted;
|
||||
|
||||
end Formal_Model;
|
||||
|
||||
---------------
|
||||
-- Is_Sorted --
|
||||
---------------
|
||||
@ -658,37 +697,6 @@ is
|
||||
return True;
|
||||
end Is_Sorted;
|
||||
|
||||
-----------------------
|
||||
-- M_Elements_Sorted --
|
||||
-----------------------
|
||||
|
||||
function M_Elements_Sorted (Container : M.Sequence) return Boolean is
|
||||
begin
|
||||
if M.Length (Container) = 0 then
|
||||
return True;
|
||||
end if;
|
||||
|
||||
declare
|
||||
E1 : Element_Type := Element (Container, Index_Type'First);
|
||||
|
||||
begin
|
||||
for I in Index_Type'First + 1 .. M.Last (Container) loop
|
||||
declare
|
||||
E2 : constant Element_Type := Element (Container, I);
|
||||
|
||||
begin
|
||||
if E2 < E1 then
|
||||
return False;
|
||||
end if;
|
||||
|
||||
E1 := E2;
|
||||
end;
|
||||
end loop;
|
||||
end;
|
||||
|
||||
return True;
|
||||
end M_Elements_Sorted;
|
||||
|
||||
----------
|
||||
-- Sort --
|
||||
----------
|
||||
|
@ -723,7 +723,7 @@ is
|
||||
Global => null,
|
||||
Contract_Cases =>
|
||||
|
||||
-- If Item is not is not contained in Container after Index, Find_Index
|
||||
-- If Item is not contained in Container after Index, Find_Index
|
||||
-- returns No_Index.
|
||||
|
||||
(Index > Last_Index (Container)
|
||||
@ -760,7 +760,7 @@ is
|
||||
Global => null,
|
||||
Contract_Cases =>
|
||||
|
||||
-- If Item is not is not contained in Container before Index,
|
||||
-- If Item is not contained in Container before Index,
|
||||
-- Reverse_Find_Index returns No_Index.
|
||||
|
||||
(not M.Contains
|
||||
@ -821,16 +821,22 @@ is
|
||||
generic
|
||||
with function "<" (Left, Right : Element_Type) return Boolean is <>;
|
||||
package Generic_Sorting with SPARK_Mode is
|
||||
function M_Elements_Sorted (Container : M.Sequence) return Boolean with
|
||||
Ghost,
|
||||
Global => null,
|
||||
Post =>
|
||||
M_Elements_Sorted'Result =
|
||||
(for all I in Index_Type'First .. M.Last (Container) =>
|
||||
(for all J in I .. M.Last (Container) =>
|
||||
Element (Container, I) = Element (Container, J)
|
||||
or Element (Container, I) < Element (Container, J)));
|
||||
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
|
||||
|
||||
package Formal_Model with Ghost is
|
||||
|
||||
function M_Elements_Sorted (Container : M.Sequence) return Boolean
|
||||
with
|
||||
Global => null,
|
||||
Post =>
|
||||
M_Elements_Sorted'Result =
|
||||
(for all I in Index_Type'First .. M.Last (Container) =>
|
||||
(for all J in I .. M.Last (Container) =>
|
||||
Element (Container, I) = Element (Container, J)
|
||||
or Element (Container, I) < Element (Container, J)));
|
||||
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
|
||||
|
||||
end Formal_Model;
|
||||
use Formal_Model;
|
||||
|
||||
function Is_Sorted (Container : Vector) return Boolean with
|
||||
Global => null,
|
||||
|
@ -514,6 +514,23 @@ is
|
||||
|
||||
package body Formal_Model is
|
||||
|
||||
----------
|
||||
-- Find --
|
||||
----------
|
||||
|
||||
function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
|
||||
is
|
||||
begin
|
||||
for I in 1 .. K.Length (Container) loop
|
||||
if Equivalent_Keys (Key, K.Get (Container, I)) then
|
||||
return I;
|
||||
elsif Key < K.Get (Container, I) then
|
||||
return 0;
|
||||
end if;
|
||||
end loop;
|
||||
return 0;
|
||||
end Find;
|
||||
|
||||
-------------------------
|
||||
-- K_Bigger_Than_Range --
|
||||
-------------------------
|
||||
|
@ -171,6 +171,16 @@ is
|
||||
Key)));
|
||||
pragma Annotate (GNATprove, Inline_For_Proof, K_Is_Find);
|
||||
|
||||
function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
|
||||
-- Search for Key in Container
|
||||
|
||||
with
|
||||
Global => null,
|
||||
Post =>
|
||||
(if Find'Result > 0 then
|
||||
Find'Result <= K.Length (Container)
|
||||
and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
|
||||
|
||||
package P is new Ada.Containers.Functional_Maps
|
||||
(Key_Type => Cursor,
|
||||
Element_Type => Positive_Count_Type,
|
||||
@ -240,17 +250,16 @@ is
|
||||
|
||||
-- It contains all the keys contained in Model
|
||||
|
||||
and
|
||||
(for all Key of Model (Container) =>
|
||||
(for some L of Keys'Result => Equivalent_Keys (L, Key)))
|
||||
and (for all Key of Model (Container) =>
|
||||
(Find (Keys'Result, Key) > 0
|
||||
and then Equivalent_Keys
|
||||
(K.Get (Keys'Result, Find (Keys'Result, Key)), Key)))
|
||||
|
||||
-- It is sorted in increasing order
|
||||
|
||||
and
|
||||
(for all I in 1 .. Length (Container) =>
|
||||
(for all J in 1 .. Length (Container) =>
|
||||
(K.Get (Keys'Result, I) < K.Get (Keys'Result, J)) =
|
||||
(I < J)));
|
||||
and (for all I in 1 .. Length (Container) =>
|
||||
Find (Keys'Result, K.Get (Keys'Result, I)) = I
|
||||
and K_Is_Find (Keys'Result, K.Get (Keys'Result, I), I));
|
||||
pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys);
|
||||
|
||||
function Positions (Container : Map) return P.Map with
|
||||
@ -482,7 +491,7 @@ is
|
||||
|
||||
-- Key now maps to New_Item
|
||||
|
||||
and Formal_Ordered_Maps.Key (Container, Find (Container, Key)) = Key
|
||||
and K.Get (Keys (Container), Find (Keys (Container), Key)) = Key
|
||||
and Element (Model (Container), Key) = New_Item
|
||||
|
||||
-- Other mappings are preserved
|
||||
@ -499,15 +508,14 @@ is
|
||||
(Left => Keys (Container)'Old,
|
||||
Right => Keys (Container),
|
||||
Fst => 1,
|
||||
Lst =>
|
||||
P.Get (Positions (Container), Find (Container, Key)) - 1)
|
||||
Lst => Find (Keys (Container), Key) - 1)
|
||||
|
||||
-- Other keys are shifted by 1
|
||||
|
||||
and K.Range_Shifted
|
||||
(Left => Keys (Container)'Old,
|
||||
Right => Keys (Container),
|
||||
Fst => P.Get (Positions (Container), Find (Container, Key)),
|
||||
Fst => Find (Keys (Container), Key),
|
||||
Lst => Length (Container)'Old,
|
||||
Offset => 1)
|
||||
|
||||
@ -516,7 +524,7 @@ is
|
||||
and P_Positions_Shifted
|
||||
(Positions (Container)'Old,
|
||||
Positions (Container),
|
||||
Cut => P.Get (Positions (Container), Find (Container, Key)));
|
||||
Cut => Find (Keys (Container), Key));
|
||||
|
||||
procedure Include
|
||||
(Container : in out Map;
|
||||
@ -541,13 +549,12 @@ is
|
||||
-- The key equivalent to Key in Container is replaced by Key
|
||||
|
||||
and K.Get
|
||||
(Keys (Container),
|
||||
P.Get (Positions (Container), Find (Container, Key))) = Key
|
||||
(Keys (Container), Find (Keys (Container), Key)) = Key
|
||||
|
||||
and K.Equal_Except
|
||||
(Keys (Container)'Old,
|
||||
Keys (Container),
|
||||
P.Get (Positions (Container), Find (Container, Key)))
|
||||
Find (Keys (Container), Key))
|
||||
|
||||
-- Elements associated with other keys are preserved
|
||||
|
||||
@ -573,8 +580,7 @@ is
|
||||
-- Key is inserted in Container
|
||||
|
||||
and K.Get
|
||||
(Keys (Container),
|
||||
P.Get (Positions (Container), Find (Container, Key))) = Key
|
||||
(Keys (Container), Find (Keys (Container), Key)) = Key
|
||||
|
||||
-- The keys of Container located before Key are preserved
|
||||
|
||||
@ -582,16 +588,14 @@ is
|
||||
(Left => Keys (Container)'Old,
|
||||
Right => Keys (Container),
|
||||
Fst => 1,
|
||||
Lst =>
|
||||
P.Get (Positions (Container), Find (Container, Key)) - 1)
|
||||
Lst => Find (Keys (Container), Key) - 1)
|
||||
|
||||
-- Other keys are shifted by 1
|
||||
|
||||
and K.Range_Shifted
|
||||
(Left => Keys (Container)'Old,
|
||||
Right => Keys (Container),
|
||||
Fst =>
|
||||
P.Get (Positions (Container), Find (Container, Key)),
|
||||
Fst => Find (Keys (Container), Key),
|
||||
Lst => Length (Container)'Old,
|
||||
Offset => 1)
|
||||
|
||||
@ -600,8 +604,7 @@ is
|
||||
and P_Positions_Shifted
|
||||
(Positions (Container)'Old,
|
||||
Positions (Container),
|
||||
Cut =>
|
||||
P.Get (Positions (Container), Find (Container, Key))));
|
||||
Cut => Find (Keys (Container), Key)));
|
||||
|
||||
procedure Replace
|
||||
(Container : in out Map;
|
||||
@ -610,7 +613,7 @@ is
|
||||
with
|
||||
Global => null,
|
||||
Pre => Contains (Container, Key),
|
||||
Post =>
|
||||
Post =>
|
||||
|
||||
-- Cursors are preserved
|
||||
|
||||
@ -618,12 +621,11 @@ is
|
||||
|
||||
-- The key equivalent to Key in Container is replaced by Key
|
||||
|
||||
and K.Get (Keys (Container),
|
||||
P.Get (Positions (Container), Find (Container, Key))) = Key
|
||||
and K.Get (Keys (Container), Find (Keys (Container), Key)) = Key
|
||||
and K.Equal_Except
|
||||
(Keys (Container)'Old,
|
||||
Keys (Container),
|
||||
P.Get (Positions (Container), Find (Container, Key)))
|
||||
Find (Keys (Container), Key))
|
||||
|
||||
-- New_Item is now associated with the Key in Container
|
||||
|
||||
@ -668,17 +670,14 @@ is
|
||||
(Left => Keys (Container)'Old,
|
||||
Right => Keys (Container),
|
||||
Fst => 1,
|
||||
Lst =>
|
||||
P.Get (Positions (Container), Find (Container, Key))'Old
|
||||
- 1)
|
||||
Lst => Find (Keys (Container), Key)'Old - 1)
|
||||
|
||||
-- The keys located after Key are shifted by 1
|
||||
|
||||
and K.Range_Shifted
|
||||
(Left => Keys (Container),
|
||||
Right => Keys (Container)'Old,
|
||||
Fst =>
|
||||
P.Get (Positions (Container), Find (Container, Key))'Old,
|
||||
Fst => Find (Keys (Container), Key)'Old,
|
||||
Lst => Length (Container),
|
||||
Offset => 1)
|
||||
|
||||
@ -687,9 +686,7 @@ is
|
||||
and P_Positions_Shifted
|
||||
(Positions (Container),
|
||||
Positions (Container)'Old,
|
||||
Cut =>
|
||||
P.Get
|
||||
(Positions (Container), Find (Container, Key))'Old));
|
||||
Cut => Find (Keys (Container), Key)'Old));
|
||||
|
||||
procedure Delete (Container : in out Map; Key : Key_Type) with
|
||||
Global => null,
|
||||
@ -715,16 +712,14 @@ is
|
||||
(Left => Keys (Container)'Old,
|
||||
Right => Keys (Container),
|
||||
Fst => 1,
|
||||
Lst =>
|
||||
P.Get (Positions (Container), Find (Container, Key))'Old - 1)
|
||||
Lst => Find (Keys (Container), Key)'Old - 1)
|
||||
|
||||
-- The keys located after Key are shifted by 1
|
||||
|
||||
and K.Range_Shifted
|
||||
(Left => Keys (Container),
|
||||
Right => Keys (Container)'Old,
|
||||
Fst =>
|
||||
P.Get (Positions (Container), Find (Container, Key))'Old,
|
||||
Fst => Find (Keys (Container), Key)'Old,
|
||||
Lst => Length (Container),
|
||||
Offset => 1)
|
||||
|
||||
@ -733,8 +728,7 @@ is
|
||||
and P_Positions_Shifted
|
||||
(Positions (Container),
|
||||
Positions (Container)'Old,
|
||||
Cut =>
|
||||
P.Get (Positions (Container), Find (Container, Key))'Old);
|
||||
Cut => Find (Keys (Container), Key)'Old);
|
||||
|
||||
procedure Delete (Container : in out Map; Position : in out Cursor) with
|
||||
Global => null,
|
||||
@ -960,29 +954,23 @@ is
|
||||
Global => null,
|
||||
Contract_Cases =>
|
||||
|
||||
-- If Key is not is not contained in Container, Find returns No_Element
|
||||
-- If Key is not contained in Container, Find returns No_Element
|
||||
|
||||
(not Contains (Model (Container), Key) =>
|
||||
not P.Has_Key (Positions (Container), Find'Result)
|
||||
and Find'Result = No_Element,
|
||||
|
||||
-- Otherwise, Find returns a valid cusror in Container
|
||||
-- Otherwise, Find returns a valid cursor in Container
|
||||
|
||||
others =>
|
||||
P.Has_Key (Positions (Container), Find'Result)
|
||||
and P.Get (Positions (Container), Find'Result) =
|
||||
Find (Keys (Container), Key)
|
||||
|
||||
-- The key designated by the result of Find is Key
|
||||
|
||||
and Equivalent_Keys
|
||||
(Formal_Ordered_Maps.Key (Container, Find'Result), Key)
|
||||
|
||||
-- Keys of Container are ordered
|
||||
|
||||
and K_Is_Find
|
||||
(Keys (Container),
|
||||
Key,
|
||||
P.Get (Positions (Container),
|
||||
Find'Result)));
|
||||
(Formal_Ordered_Maps.Key (Container, Find'Result), Key));
|
||||
|
||||
function Element (Container : Map; Key : Key_Type) return Element_Type with
|
||||
Global => null,
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 2010-2015, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 2010-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- --
|
||||
@ -360,34 +360,6 @@ is
|
||||
return Target;
|
||||
end Copy;
|
||||
|
||||
---------------------
|
||||
-- Current_To_Last --
|
||||
---------------------
|
||||
|
||||
function Current_To_Last (Container : Set; Current : Cursor) return Set is
|
||||
Curs : Cursor := First (Container);
|
||||
C : Set (Container.Capacity) := Copy (Container, Container.Capacity);
|
||||
Node : Count_Type;
|
||||
|
||||
begin
|
||||
if Curs = No_Element then
|
||||
Clear (C);
|
||||
return C;
|
||||
end if;
|
||||
|
||||
if Current /= No_Element and not Has_Element (Container, Current) then
|
||||
raise Constraint_Error;
|
||||
end if;
|
||||
|
||||
while Curs.Node /= Current.Node loop
|
||||
Node := Curs.Node;
|
||||
Delete (C, Curs);
|
||||
Curs := Next (Container, (Node => Node));
|
||||
end loop;
|
||||
|
||||
return C;
|
||||
end Current_To_Last;
|
||||
|
||||
------------
|
||||
-- Delete --
|
||||
------------
|
||||
@ -596,36 +568,6 @@ is
|
||||
end;
|
||||
end First_Element;
|
||||
|
||||
-----------------------
|
||||
-- First_To_Previous --
|
||||
-----------------------
|
||||
|
||||
function First_To_Previous
|
||||
(Container : Set;
|
||||
Current : Cursor) return Set
|
||||
is
|
||||
Curs : Cursor := Current;
|
||||
C : Set (Container.Capacity) := Copy (Container, Container.Capacity);
|
||||
Node : Count_Type;
|
||||
|
||||
begin
|
||||
if Curs = No_Element then
|
||||
return C;
|
||||
|
||||
elsif not Has_Element (Container, Curs) then
|
||||
raise Constraint_Error;
|
||||
|
||||
else
|
||||
while Curs.Node /= 0 loop
|
||||
Node := Curs.Node;
|
||||
Delete (C, Curs);
|
||||
Curs := Next (Container, (Node => Node));
|
||||
end loop;
|
||||
|
||||
return C;
|
||||
end if;
|
||||
end First_To_Previous;
|
||||
|
||||
-----------
|
||||
-- Floor --
|
||||
-----------
|
||||
@ -644,6 +586,333 @@ is
|
||||
end;
|
||||
end Floor;
|
||||
|
||||
------------------
|
||||
-- Formal_Model --
|
||||
------------------
|
||||
|
||||
package body Formal_Model is
|
||||
|
||||
-------------------------
|
||||
-- E_Bigger_Than_Range --
|
||||
-------------------------
|
||||
|
||||
function E_Bigger_Than_Range
|
||||
(Container : E.Sequence;
|
||||
Fst : Positive_Count_Type;
|
||||
Lst : Count_Type;
|
||||
Item : Element_Type) return Boolean
|
||||
is
|
||||
begin
|
||||
for I in Fst .. Lst loop
|
||||
if not (E.Get (Container, I) < Item) then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
return True;
|
||||
end E_Bigger_Than_Range;
|
||||
|
||||
-------------------------
|
||||
-- E_Elements_Included --
|
||||
-------------------------
|
||||
|
||||
function E_Elements_Included
|
||||
(Left : E.Sequence;
|
||||
Right : E.Sequence) return Boolean
|
||||
is
|
||||
begin
|
||||
for I in 1 .. E.Length (Left) loop
|
||||
if not E.Contains (Right, 1, E.Length (Right), E.Get (Left, I))
|
||||
then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
|
||||
return True;
|
||||
end E_Elements_Included;
|
||||
|
||||
function E_Elements_Included
|
||||
(Left : E.Sequence;
|
||||
Model : M.Set;
|
||||
Right : E.Sequence) return Boolean
|
||||
is
|
||||
begin
|
||||
for I in 1 .. E.Length (Left) loop
|
||||
declare
|
||||
Item : constant Element_Type := E.Get (Left, I);
|
||||
begin
|
||||
if M.Contains (Model, Item) then
|
||||
if not E.Contains (Right, 1, E.Length (Right), Item) then
|
||||
return False;
|
||||
end if;
|
||||
end if;
|
||||
end;
|
||||
end loop;
|
||||
|
||||
return True;
|
||||
end E_Elements_Included;
|
||||
|
||||
function E_Elements_Included
|
||||
(Container : E.Sequence;
|
||||
Model : M.Set;
|
||||
Left : E.Sequence;
|
||||
Right : E.Sequence) return Boolean
|
||||
is
|
||||
begin
|
||||
for I in 1 .. E.Length (Container) loop
|
||||
declare
|
||||
Item : constant Element_Type := E.Get (Container, I);
|
||||
begin
|
||||
if M.Contains (Model, Item) then
|
||||
if not E.Contains (Left, 1, E.Length (Left), Item) then
|
||||
return False;
|
||||
end if;
|
||||
else
|
||||
if not E.Contains (Right, 1, E.Length (Right), Item) then
|
||||
return False;
|
||||
end if;
|
||||
end if;
|
||||
end;
|
||||
end loop;
|
||||
|
||||
return True;
|
||||
end E_Elements_Included;
|
||||
|
||||
---------------
|
||||
-- E_Is_Find --
|
||||
---------------
|
||||
|
||||
function E_Is_Find
|
||||
(Container : E.Sequence;
|
||||
Item : Element_Type;
|
||||
Position : Count_Type) return Boolean
|
||||
is
|
||||
begin
|
||||
for I in 1 .. Position - 1 loop
|
||||
if Item < E.Get (Container, I) then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
|
||||
if Position < E.Length (Container) then
|
||||
for I in Position + 1 .. E.Length (Container) loop
|
||||
if E.Get (Container, I) < Item then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
end if;
|
||||
return True;
|
||||
end E_Is_Find;
|
||||
|
||||
--------------------------
|
||||
-- E_Smaller_Than_Range --
|
||||
--------------------------
|
||||
|
||||
function E_Smaller_Than_Range
|
||||
(Container : E.Sequence;
|
||||
Fst : Positive_Count_Type;
|
||||
Lst : Count_Type;
|
||||
Item : Element_Type) return Boolean
|
||||
is
|
||||
begin
|
||||
for I in Fst .. Lst loop
|
||||
if not (Item < E.Get (Container, I)) then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
return True;
|
||||
end E_Smaller_Than_Range;
|
||||
|
||||
----------
|
||||
-- Find --
|
||||
----------
|
||||
|
||||
function Find
|
||||
(Container : E.Sequence;
|
||||
Item : Element_Type) return Count_Type
|
||||
is
|
||||
begin
|
||||
for I in 1 .. E.Length (Container) loop
|
||||
if Equivalent_Elements (Item, E.Get (Container, I)) then
|
||||
return I;
|
||||
end if;
|
||||
end loop;
|
||||
return 0;
|
||||
end Find;
|
||||
|
||||
--------------
|
||||
-- Elements --
|
||||
--------------
|
||||
|
||||
function Elements (Container : Set) return E.Sequence is
|
||||
Position : Count_Type := Container.First;
|
||||
R : E.Sequence;
|
||||
|
||||
begin
|
||||
-- Can't use First, Next or Element here, since they depend on models
|
||||
-- for their postconditions.
|
||||
|
||||
while Position /= 0 loop
|
||||
R := E.Add (R, Container.Nodes (Position).Element);
|
||||
Position := Tree_Operations.Next (Container, Position);
|
||||
end loop;
|
||||
|
||||
return R;
|
||||
end Elements;
|
||||
|
||||
----------------------------
|
||||
-- Lift_Abstraction_Level --
|
||||
----------------------------
|
||||
|
||||
procedure Lift_Abstraction_Level (Container : Set) is null;
|
||||
|
||||
-----------------------
|
||||
-- Mapping_Preserved --
|
||||
-----------------------
|
||||
|
||||
function Mapping_Preserved
|
||||
(E_Left : E.Sequence;
|
||||
E_Right : E.Sequence;
|
||||
P_Left : P.Map;
|
||||
P_Right : P.Map) return Boolean
|
||||
is
|
||||
begin
|
||||
for C of P_Left loop
|
||||
if not P.Has_Key (P_Right, C)
|
||||
or else P.Get (P_Left, C) > E.Length (E_Left)
|
||||
or else P.Get (P_Right, C) > E.Length (E_Right)
|
||||
or else E.Get (E_Left, P.Get (P_Left, C)) /=
|
||||
E.Get (E_Right, P.Get (P_Right, C))
|
||||
then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
|
||||
return True;
|
||||
end Mapping_Preserved;
|
||||
|
||||
------------------------------
|
||||
-- Mapping_Preserved_Except --
|
||||
------------------------------
|
||||
|
||||
function Mapping_Preserved_Except
|
||||
(E_Left : E.Sequence;
|
||||
E_Right : E.Sequence;
|
||||
P_Left : P.Map;
|
||||
P_Right : P.Map;
|
||||
Position : Cursor) return Boolean
|
||||
is
|
||||
begin
|
||||
for C of P_Left loop
|
||||
if C /= Position
|
||||
and (not P.Has_Key (P_Right, C)
|
||||
or else P.Get (P_Left, C) > E.Length (E_Left)
|
||||
or else P.Get (P_Right, C) > E.Length (E_Right)
|
||||
or else E.Get (E_Left, P.Get (P_Left, C)) /=
|
||||
E.Get (E_Right, P.Get (P_Right, C)))
|
||||
then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
|
||||
return True;
|
||||
end Mapping_Preserved_Except;
|
||||
|
||||
-------------------------
|
||||
-- P_Positions_Shifted --
|
||||
-------------------------
|
||||
|
||||
function P_Positions_Shifted
|
||||
(Small : P.Map;
|
||||
Big : P.Map;
|
||||
Cut : Positive_Count_Type;
|
||||
Count : Count_Type := 1) return Boolean
|
||||
is
|
||||
begin
|
||||
for Cu of Small loop
|
||||
if not P.Has_Key (Big, Cu) then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
|
||||
for Cu of Big loop
|
||||
declare
|
||||
Pos : constant Positive_Count_Type := P.Get (Big, Cu);
|
||||
|
||||
begin
|
||||
if Pos < Cut then
|
||||
if not P.Has_Key (Small, Cu)
|
||||
or else Pos /= P.Get (Small, Cu)
|
||||
then
|
||||
return False;
|
||||
end if;
|
||||
|
||||
elsif Pos >= Cut + Count then
|
||||
if not P.Has_Key (Small, Cu)
|
||||
or else Pos /= P.Get (Small, Cu) + Count
|
||||
then
|
||||
return False;
|
||||
end if;
|
||||
|
||||
else
|
||||
if P.Has_Key (Small, Cu) then
|
||||
return False;
|
||||
end if;
|
||||
end if;
|
||||
end;
|
||||
end loop;
|
||||
|
||||
return True;
|
||||
end P_Positions_Shifted;
|
||||
|
||||
-----------
|
||||
-- Model --
|
||||
-----------
|
||||
|
||||
function Model (Container : Set) return M.Set is
|
||||
Position : Count_Type := Container.First;
|
||||
R : M.Set;
|
||||
|
||||
begin
|
||||
-- Can't use First, Next or Element here, since they depend on models
|
||||
-- for their postconditions.
|
||||
|
||||
while Position /= 0 loop
|
||||
R :=
|
||||
M.Add
|
||||
(Container => R,
|
||||
Item => Container.Nodes (Position).Element);
|
||||
|
||||
Position := Tree_Operations.Next (Container, Position);
|
||||
end loop;
|
||||
|
||||
return R;
|
||||
end Model;
|
||||
|
||||
---------------
|
||||
-- Positions --
|
||||
---------------
|
||||
|
||||
function Positions (Container : Set) return P.Map is
|
||||
I : Count_Type := 1;
|
||||
Position : Count_Type := Container.First;
|
||||
R : P.Map;
|
||||
|
||||
begin
|
||||
-- Can't use First, Next or Element here, since they depend on models
|
||||
-- for their postconditions.
|
||||
|
||||
while Position /= 0 loop
|
||||
R := P.Add (R, (Node => Position), I);
|
||||
pragma Assert (P.Length (R) = I);
|
||||
Position := Tree_Operations.Next (Container, Position);
|
||||
I := I + 1;
|
||||
end loop;
|
||||
|
||||
return R;
|
||||
end Positions;
|
||||
|
||||
end Formal_Model;
|
||||
|
||||
----------
|
||||
-- Free --
|
||||
----------
|
||||
@ -807,6 +1076,116 @@ is
|
||||
return (if Node = 0 then No_Element else (Node => Node));
|
||||
end Floor;
|
||||
|
||||
------------------
|
||||
-- Formal_Model --
|
||||
------------------
|
||||
|
||||
package body Formal_Model is
|
||||
|
||||
-------------------------
|
||||
-- E_Bigger_Than_Range --
|
||||
-------------------------
|
||||
|
||||
function E_Bigger_Than_Range
|
||||
(Container : E.Sequence;
|
||||
Fst : Positive_Count_Type;
|
||||
Lst : Count_Type;
|
||||
Key : Key_Type) return Boolean
|
||||
is
|
||||
begin
|
||||
for I in Fst .. Lst loop
|
||||
if not (Generic_Keys.Key (E.Get (Container, I)) < Key) then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
return True;
|
||||
end E_Bigger_Than_Range;
|
||||
|
||||
---------------
|
||||
-- E_Is_Find --
|
||||
---------------
|
||||
|
||||
function E_Is_Find
|
||||
(Container : E.Sequence;
|
||||
Key : Key_Type;
|
||||
Position : Count_Type) return Boolean
|
||||
is
|
||||
begin
|
||||
for I in 1 .. Position - 1 loop
|
||||
if Key < Generic_Keys.Key (E.Get (Container, I)) then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
|
||||
if Position < E.Length (Container) then
|
||||
for I in Position + 1 .. E.Length (Container) loop
|
||||
if Generic_Keys.Key (E.Get (Container, I)) < Key then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
end if;
|
||||
return True;
|
||||
end E_Is_Find;
|
||||
|
||||
--------------------------
|
||||
-- E_Smaller_Than_Range --
|
||||
--------------------------
|
||||
|
||||
function E_Smaller_Than_Range
|
||||
(Container : E.Sequence;
|
||||
Fst : Positive_Count_Type;
|
||||
Lst : Count_Type;
|
||||
Key : Key_Type) return Boolean
|
||||
is
|
||||
begin
|
||||
for I in Fst .. Lst loop
|
||||
if not (Key < Generic_Keys.Key (E.Get (Container, I))) then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
return True;
|
||||
end E_Smaller_Than_Range;
|
||||
|
||||
----------
|
||||
-- Find --
|
||||
----------
|
||||
|
||||
function Find
|
||||
(Container : E.Sequence;
|
||||
Key : Key_Type) return Count_Type
|
||||
is
|
||||
begin
|
||||
for I in 1 .. E.Length (Container) loop
|
||||
if Equivalent_Keys
|
||||
(Key, Generic_Keys.Key (E.Get (Container, I)))
|
||||
then
|
||||
return I;
|
||||
end if;
|
||||
end loop;
|
||||
return 0;
|
||||
end Find;
|
||||
|
||||
-----------------------
|
||||
-- M_Included_Except --
|
||||
-----------------------
|
||||
|
||||
function M_Included_Except
|
||||
(Left : M.Set;
|
||||
Right : M.Set;
|
||||
Key : Key_Type) return Boolean
|
||||
is
|
||||
begin
|
||||
for E of Left loop
|
||||
if not Contains (Right, E)
|
||||
and not Equivalent_Keys (Generic_Keys.Key (E), Key)
|
||||
then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
return True;
|
||||
end M_Included_Except;
|
||||
end Formal_Model;
|
||||
|
||||
-------------------------
|
||||
-- Is_Greater_Key_Node --
|
||||
-------------------------
|
||||
@ -1441,35 +1820,6 @@ is
|
||||
Node.Right := Right;
|
||||
end Set_Right;
|
||||
|
||||
------------------
|
||||
-- Strict_Equal --
|
||||
------------------
|
||||
|
||||
function Strict_Equal (Left, Right : Set) return Boolean is
|
||||
LNode : Count_Type := First (Left).Node;
|
||||
RNode : Count_Type := First (Right).Node;
|
||||
|
||||
begin
|
||||
if Length (Left) /= Length (Right) then
|
||||
return False;
|
||||
end if;
|
||||
|
||||
while LNode = RNode loop
|
||||
if LNode = 0 then
|
||||
return True;
|
||||
end if;
|
||||
|
||||
if Left.Nodes (LNode).Element /= Right.Nodes (RNode).Element then
|
||||
exit;
|
||||
end if;
|
||||
|
||||
LNode := Next (Left, LNode);
|
||||
RNode := Next (Right, RNode);
|
||||
end loop;
|
||||
|
||||
return False;
|
||||
end Strict_Equal;
|
||||
|
||||
--------------------------
|
||||
-- Symmetric_Difference --
|
||||
--------------------------
|
||||
|
1632
gcc/ada/a-cforse.ads
1632
gcc/ada/a-cforse.ads
File diff suppressed because it is too large
Load Diff
@ -636,6 +636,45 @@ is
|
||||
|
||||
package body Generic_Sorting with SPARK_Mode => Off is
|
||||
|
||||
------------------
|
||||
-- Formal_Model --
|
||||
------------------
|
||||
|
||||
package body Formal_Model is
|
||||
|
||||
-----------------------
|
||||
-- M_Elements_Sorted --
|
||||
-----------------------
|
||||
|
||||
function M_Elements_Sorted (Container : M.Sequence) return Boolean is
|
||||
begin
|
||||
if M.Length (Container) = 0 then
|
||||
return True;
|
||||
end if;
|
||||
|
||||
declare
|
||||
E1 : Element_Type := Element (Container, Index_Type'First);
|
||||
|
||||
begin
|
||||
for I in Index_Type'First + 1 .. M.Last (Container) loop
|
||||
declare
|
||||
E2 : constant Element_Type := Element (Container, I);
|
||||
|
||||
begin
|
||||
if E2 < E1 then
|
||||
return False;
|
||||
end if;
|
||||
|
||||
E1 := E2;
|
||||
end;
|
||||
end loop;
|
||||
end;
|
||||
|
||||
return True;
|
||||
end M_Elements_Sorted;
|
||||
|
||||
end Formal_Model;
|
||||
|
||||
---------------
|
||||
-- Is_Sorted --
|
||||
---------------
|
||||
@ -655,37 +694,6 @@ is
|
||||
return True;
|
||||
end Is_Sorted;
|
||||
|
||||
-----------------------
|
||||
-- M_Elements_Sorted --
|
||||
-----------------------
|
||||
|
||||
function M_Elements_Sorted (Container : M.Sequence) return Boolean is
|
||||
begin
|
||||
if M.Length (Container) = 0 then
|
||||
return True;
|
||||
end if;
|
||||
|
||||
declare
|
||||
E1 : Element_Type := Element (Container, Index_Type'First);
|
||||
|
||||
begin
|
||||
for I in Index_Type'First + 1 .. M.Last (Container) loop
|
||||
declare
|
||||
E2 : constant Element_Type := Element (Container, I);
|
||||
|
||||
begin
|
||||
if E2 < E1 then
|
||||
return False;
|
||||
end if;
|
||||
|
||||
E1 := E2;
|
||||
end;
|
||||
end loop;
|
||||
end;
|
||||
|
||||
return True;
|
||||
end M_Elements_Sorted;
|
||||
|
||||
----------
|
||||
-- Sort --
|
||||
----------
|
||||
|
@ -717,7 +717,7 @@ is
|
||||
Global => null,
|
||||
Contract_Cases =>
|
||||
|
||||
-- If Item is not is not contained in Container after Index, Find_Index
|
||||
-- If Item is not contained in Container after Index, Find_Index
|
||||
-- returns No_Index.
|
||||
|
||||
(Index > Last_Index (Container)
|
||||
@ -754,7 +754,7 @@ is
|
||||
Global => null,
|
||||
Contract_Cases =>
|
||||
|
||||
-- If Item is not is not contained in Container before Index,
|
||||
-- If Item is not contained in Container before Index,
|
||||
-- Reverse_Find_Index returns No_Index.
|
||||
|
||||
(not M.Contains
|
||||
@ -815,16 +815,22 @@ is
|
||||
generic
|
||||
with function "<" (Left, Right : Element_Type) return Boolean is <>;
|
||||
package Generic_Sorting with SPARK_Mode is
|
||||
function M_Elements_Sorted (Container : M.Sequence) return Boolean with
|
||||
Ghost,
|
||||
Global => null,
|
||||
Post =>
|
||||
M_Elements_Sorted'Result =
|
||||
(for all I in Index_Type'First .. M.Last (Container) =>
|
||||
(for all J in I .. M.Last (Container) =>
|
||||
Element (Container, I) = Element (Container, J)
|
||||
or Element (Container, I) < Element (Container, J)));
|
||||
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
|
||||
|
||||
package Formal_Model with Ghost is
|
||||
|
||||
function M_Elements_Sorted (Container : M.Sequence) return Boolean
|
||||
with
|
||||
Global => null,
|
||||
Post =>
|
||||
M_Elements_Sorted'Result =
|
||||
(for all I in Index_Type'First .. M.Last (Container) =>
|
||||
(for all J in I .. M.Last (Container) =>
|
||||
Element (Container, I) = Element (Container, J)
|
||||
or Element (Container, I) < Element (Container, J)));
|
||||
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
|
||||
|
||||
end Formal_Model;
|
||||
use Formal_Model;
|
||||
|
||||
function Is_Sorted (Container : Vector) return Boolean with
|
||||
Global => null,
|
||||
|
@ -35,7 +35,9 @@ private with Ada.Containers.Functional_Base;
|
||||
generic
|
||||
type Key_Type (<>) is private;
|
||||
type Element_Type (<>) is private;
|
||||
with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
|
||||
with function Equivalent_Keys
|
||||
(Left : Key_Type;
|
||||
Right : Key_Type) return Boolean is "=";
|
||||
Enable_Handling_Of_Equivalence : Boolean := True;
|
||||
-- This constant should only be set to False when no particular handling
|
||||
-- of equivalence over keys is needed, that is, Equivalent_Keys defines a
|
||||
@ -53,8 +55,8 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
|
||||
-- "For in" quantification over maps should not be used.
|
||||
-- "For of" quantification over maps iterates over keys.
|
||||
-- Note that, for proof, "for of" quantification is understood modulo
|
||||
-- equivalence (quantification includes keys equivalent to keys of the
|
||||
-- map).
|
||||
-- equivalence (the range of quantification comprises all the keys that are
|
||||
-- equivalent to any key of the map).
|
||||
|
||||
-----------------------
|
||||
-- Basic operations --
|
||||
@ -89,8 +91,8 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
|
||||
|
||||
Get'Result = W_Get (Container, Witness (Container, Key))
|
||||
and (for all K of Container =>
|
||||
(if Equivalent_Keys (K, Key) then
|
||||
Witness (Container, Key) = Witness (Container, K))));
|
||||
(Equivalent_Keys (K, Key) =
|
||||
(Witness (Container, Key) = Witness (Container, K)))));
|
||||
|
||||
function Length (Container : Map) return Count_Type with
|
||||
Global => null;
|
||||
|
@ -113,6 +113,17 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
|
||||
function Is_Empty (Container : Set) return Boolean is
|
||||
(Length (Container.Content) = 0);
|
||||
|
||||
------------------
|
||||
-- Is_Singleton --
|
||||
------------------
|
||||
|
||||
function Is_Singleton
|
||||
(Container : Set;
|
||||
New_Item : Element_Type) return Boolean
|
||||
is
|
||||
(Length (Container.Content) = 1
|
||||
and New_Item = Get (Container.Content, 1));
|
||||
|
||||
------------
|
||||
-- Length --
|
||||
------------
|
||||
@ -120,6 +131,25 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
|
||||
function Length (Container : Set) return Count_Type is
|
||||
(Length (Container.Content));
|
||||
|
||||
-----------------
|
||||
-- Not_In_Both --
|
||||
-----------------
|
||||
|
||||
function Not_In_Both
|
||||
(Container : Set;
|
||||
Left : Set;
|
||||
Right : Set) return Boolean
|
||||
is
|
||||
(for all Item of Container =>
|
||||
not Contains (Right, Item) or not Contains (Left, Item));
|
||||
|
||||
----------------
|
||||
-- No_Overlap --
|
||||
----------------
|
||||
|
||||
function No_Overlap (Left : Set; Right : Set) return Boolean is
|
||||
(Num_Overlaps (Left.Content, Right.Content) = 0);
|
||||
|
||||
------------------
|
||||
-- Num_Overlaps --
|
||||
------------------
|
||||
|
@ -36,7 +36,7 @@ generic
|
||||
type Element_Type (<>) is private;
|
||||
with function Equivalent_Elements
|
||||
(Left : Element_Type;
|
||||
Right : Element_Type) return Boolean;
|
||||
Right : Element_Type) return Boolean is "=";
|
||||
Enable_Handling_Of_Equivalence : Boolean := True;
|
||||
-- This constant should only be set to False when no particular handling
|
||||
-- of equivalence over elements is needed, that is, Equivalent_Elements
|
||||
@ -45,7 +45,7 @@ generic
|
||||
package Ada.Containers.Functional_Sets with SPARK_Mode is
|
||||
|
||||
type Set is private with
|
||||
Default_Initial_Condition => Is_Empty (Set) and Length (Set) = 0,
|
||||
Default_Initial_Condition => Is_Empty (Set),
|
||||
Iterable => (First => Iter_First,
|
||||
Next => Iter_Next,
|
||||
Has_Element => Iter_Has_Element,
|
||||
@ -54,8 +54,8 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
|
||||
-- "For in" quantification over sets should not be used.
|
||||
-- "For of" quantification over sets iterates over elements.
|
||||
-- Note that, for proof, "for of" quantification is understood modulo
|
||||
-- equivalence (quantification includes elements equivalent to elements of
|
||||
-- the map).
|
||||
-- equivalence (the range of quantification comprises all the elements that
|
||||
-- are equivalent to any element of the set).
|
||||
|
||||
-----------------------
|
||||
-- Basic operations --
|
||||
@ -89,23 +89,23 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
|
||||
-- Set inclusion
|
||||
|
||||
Global => null,
|
||||
Post => "<="'Result = (for all Item of Left => Contains (Right, Item));
|
||||
Post => "<="'Result = (for all Item of Left => Contains (Right, Item))
|
||||
and (if "<="'Result then Length (Left) <= Length (Right));
|
||||
|
||||
function "=" (Left : Set; Right : Set) return Boolean with
|
||||
-- Extensional equality over sets
|
||||
|
||||
Global => null,
|
||||
Post =>
|
||||
"="'Result =
|
||||
(for all Item of Left => Contains (Right, Item))
|
||||
and (for all Item of Right => Contains (Left, Item));
|
||||
Post => "="'Result = (Left <= Right and Right <= Left);
|
||||
|
||||
pragma Warnings (Off, "unused variable ""Item""");
|
||||
function Is_Empty (Container : Set) return Boolean with
|
||||
-- A set is empty if it contains no element
|
||||
|
||||
Global => null,
|
||||
Post => Is_Empty'Result = (for all Item of Container => False);
|
||||
Post =>
|
||||
Is_Empty'Result = (for all Item of Container => False)
|
||||
and Is_Empty'Result = (Length (Container) = 0);
|
||||
pragma Warnings (On, "unused variable ""Item""");
|
||||
|
||||
function Included_Except
|
||||
@ -149,15 +149,45 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
|
||||
(for all Item of Container =>
|
||||
Contains (Left, Item) or Contains (Right, Item));
|
||||
|
||||
function Is_Singleton
|
||||
(Container : Set;
|
||||
New_Item : Element_Type) return Boolean
|
||||
with
|
||||
-- Return True Container only contains New_Item
|
||||
|
||||
Global => null,
|
||||
Post =>
|
||||
Is_Singleton'Result =
|
||||
(for all Item of Container => Equivalent_Elements (Item, New_Item));
|
||||
|
||||
function Not_In_Both
|
||||
(Container : Set;
|
||||
Left : Set;
|
||||
Right : Set) return Boolean
|
||||
-- Return True if there are no elements in Container that are in Left and
|
||||
-- Right.
|
||||
|
||||
with
|
||||
Global => null,
|
||||
Post =>
|
||||
Not_In_Both'Result =
|
||||
(for all Item of Container =>
|
||||
not Contains (Left, Item) or not Contains (Right, Item));
|
||||
|
||||
function No_Overlap (Left : Set; Right : Set) return Boolean with
|
||||
-- Return True if there are no equivalent elements in Left and Right
|
||||
|
||||
Global => null,
|
||||
Post =>
|
||||
No_Overlap'Result =
|
||||
(for all Item of Left => not Contains (Right, Item));
|
||||
|
||||
function Num_Overlaps (Left : Set; Right : Set) return Count_Type with
|
||||
-- Number of elements that are both in Left and Right
|
||||
|
||||
Global => null,
|
||||
Post =>
|
||||
Num_Overlaps'Result <= Length (Left)
|
||||
and Num_Overlaps'Result <= Length (Right)
|
||||
and (if Num_Overlaps'Result = 0 then
|
||||
(for all Item of Left => not Contains (Right, Item)));
|
||||
Num_Overlaps'Result = Length (Intersection (Left, Right));
|
||||
|
||||
----------------------------
|
||||
-- Construction Functions --
|
||||
@ -195,8 +225,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
|
||||
|
||||
Global => null,
|
||||
Post =>
|
||||
Length (Intersection'Result) = Num_Overlaps (Left, Right)
|
||||
and Intersection'Result <= Left
|
||||
Intersection'Result <= Left
|
||||
and Intersection'Result <= Right
|
||||
and Includes_Intersection (Intersection'Result, Left, Right);
|
||||
|
||||
@ -250,9 +279,13 @@ private
|
||||
|
||||
subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
|
||||
|
||||
function "="
|
||||
(Left : Element_Type;
|
||||
Right : Element_Type) return Boolean renames Equivalent_Elements;
|
||||
|
||||
package Containers is new Ada.Containers.Functional_Base
|
||||
(Element_Type => Element_Type,
|
||||
Index_Type => Positive_Count_Type);
|
||||
(Element_Type => Element_Type,
|
||||
Index_Type => Positive_Count_Type);
|
||||
|
||||
type Set is record
|
||||
Content : Containers.Container;
|
||||
|
@ -35,7 +35,6 @@ with Csets; use Csets;
|
||||
with Debug; use Debug;
|
||||
with Einfo; use Einfo;
|
||||
with Erroutc; use Erroutc;
|
||||
with Fname; use Fname;
|
||||
with Gnatvsn; use Gnatvsn;
|
||||
with Lib; use Lib;
|
||||
with Opt; use Opt;
|
||||
@ -2708,9 +2707,7 @@ package body Errout is
|
||||
-- Types in other language defined units are displayed as
|
||||
-- "package-name.type-name"
|
||||
|
||||
elsif
|
||||
Is_Predefined_File_Name (Unit_File_Name (Get_Source_Unit (Ent)))
|
||||
then
|
||||
elsif Is_Predefined_Unit (Get_Source_Unit (Ent)) then
|
||||
Get_Unqualified_Decoded_Name_String
|
||||
(Unit_Name (Get_Source_Unit (Ent)));
|
||||
Name_Len := Name_Len - 2;
|
||||
@ -2748,8 +2745,7 @@ package body Errout is
|
||||
|
||||
if Sloc (Error_Msg_Node_1) > Standard_Location
|
||||
and then
|
||||
not Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Error_Msg_Node_1)))
|
||||
not Is_Predefined_Unit (Get_Source_Unit (Error_Msg_Node_1))
|
||||
then
|
||||
Get_Name_String (Unit_File_Name (Get_Source_Unit (Error_Msg_Node_1)));
|
||||
Set_Msg_Str (" defined");
|
||||
|
@ -37,7 +37,6 @@ with Exp_Ch7; use Exp_Ch7;
|
||||
with Exp_Ch9; use Exp_Ch9;
|
||||
with Exp_Disp; use Exp_Disp;
|
||||
with Exp_Tss; use Exp_Tss;
|
||||
with Fname; use Fname;
|
||||
with Freeze; use Freeze;
|
||||
with Itypes; use Itypes;
|
||||
with Lib; use Lib;
|
||||
@ -4532,8 +4531,7 @@ package body Exp_Aggr is
|
||||
and then
|
||||
Is_Preelaborated (Spec_Entity (P)))
|
||||
or else
|
||||
Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (P)))
|
||||
Is_Predefined_Unit (Get_Source_Unit (P))
|
||||
then
|
||||
null;
|
||||
|
||||
|
@ -39,7 +39,6 @@ with Exp_Pakd; use Exp_Pakd;
|
||||
with Exp_Strm; use Exp_Strm;
|
||||
with Exp_Tss; use Exp_Tss;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Fname; use Fname;
|
||||
with Freeze; use Freeze;
|
||||
with Gnatvsn; use Gnatvsn;
|
||||
with Itypes; use Itypes;
|
||||
@ -7749,7 +7748,7 @@ package body Exp_Attr is
|
||||
-- instead. That is why we include the test Is_Available when dealing
|
||||
-- with these cases.
|
||||
|
||||
if not Is_Predefined_File_Name (Unit_File_Name (Current_Sem_Unit)) then
|
||||
if not Is_Predefined_Unit (Current_Sem_Unit) then
|
||||
-- Storage_Array as defined in package System.Storage_Elements
|
||||
|
||||
if Is_RTE (Base_Typ, RE_Storage_Array) then
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1996-2015, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1996-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- --
|
||||
@ -26,7 +26,6 @@
|
||||
with Atree; use Atree;
|
||||
with Einfo; use Einfo;
|
||||
with Errout; use Errout;
|
||||
with Fname; use Fname;
|
||||
with Lib; use Lib;
|
||||
with Namet; use Namet;
|
||||
with Nlists; use Nlists;
|
||||
@ -274,9 +273,7 @@ package body Exp_Code is
|
||||
-- referenced entity is in a runtime routine.
|
||||
|
||||
if Is_Entity_Name (N)
|
||||
and then
|
||||
Is_Predefined_File_Name (Unit_File_Name
|
||||
(Get_Source_Unit (Entity (N))))
|
||||
and then Is_Predefined_Unit (Get_Source_Unit (Entity (N)))
|
||||
then
|
||||
return;
|
||||
|
||||
|
@ -1116,9 +1116,15 @@ package body Exp_Util is
|
||||
|
||||
-- If the entity is an overridden primitive and we are not in
|
||||
-- GNATprove mode, we must build a wrapper for the current
|
||||
-- inherited operation.
|
||||
-- inherited operation. If the reference is the prefix of an
|
||||
-- attribute such as 'Result (or others ???) there is no need
|
||||
-- for a wrapper: the condition is just rewritten in terms of
|
||||
-- the inherited subprogram.
|
||||
|
||||
if Is_Subprogram (New_E) and then not GNATprove_Mode then
|
||||
if Is_Subprogram (New_E)
|
||||
and then Nkind (Parent (N)) /= N_Attribute_Reference
|
||||
and then not GNATprove_Mode
|
||||
then
|
||||
Needs_Wrapper := True;
|
||||
end if;
|
||||
end if;
|
||||
|
@ -6,7 +6,7 @@
|
||||
* *
|
||||
* C Header File *
|
||||
* *
|
||||
* Copyright (C) 1992-2016, Free Software Foundation, Inc. *
|
||||
* Copyright (C) 1992-2017, Free Software Foundation, Inc. *
|
||||
* *
|
||||
* GNAT is free software; you can redistribute it and/or modify it under *
|
||||
* terms of the GNU General Public License as published by the Free Soft- *
|
||||
@ -219,6 +219,7 @@ extern void Check_Elaboration_Code_Allowed (Node_Id);
|
||||
extern void Check_Implicit_Dynamic_Code_Allowed (Node_Id);
|
||||
|
||||
/* sem_aggr: */
|
||||
|
||||
#define Is_Others_Aggregate sem_aggr__is_others_aggregate
|
||||
|
||||
extern Boolean Is_Others_Aggregate (Node_Id);
|
||||
@ -297,6 +298,12 @@ extern Boolean Signed_Zeros_On_Target;
|
||||
extern Boolean Stack_Check_Probes_On_Target;
|
||||
extern Boolean Stack_Check_Limits_On_Target;
|
||||
|
||||
/* warnsw: */
|
||||
|
||||
#define Warn_On_Questionable_Layout warnsw__warn_on_questionable_layout
|
||||
|
||||
extern Boolean Warn_On_Questionable_Layout;
|
||||
|
||||
#ifdef __cplusplus
|
||||
}
|
||||
#endif
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNAT is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
@ -99,21 +99,14 @@ package body Fname is
|
||||
return False;
|
||||
end Has_Prefix;
|
||||
|
||||
---------------------------
|
||||
-- Is_Internal_File_Name --
|
||||
---------------------------
|
||||
-----------------------
|
||||
-- Is_GNAT_File_Name --
|
||||
-----------------------
|
||||
|
||||
function Is_Internal_File_Name
|
||||
(Fname : String;
|
||||
Renamings_Included : Boolean := True) return Boolean
|
||||
is
|
||||
function Is_GNAT_File_Name (Fname : String) return Boolean is
|
||||
begin
|
||||
if Is_Predefined_File_Name (Fname, Renamings_Included) then
|
||||
return True;
|
||||
end if;
|
||||
|
||||
-- Check for internal extensions first, so we don't think (e.g.)
|
||||
-- "gnat.adc" is internal.
|
||||
-- Check for internal extensions before checking prefixes, so we don't
|
||||
-- think (e.g.) "gnat.adc" is internal.
|
||||
|
||||
if not Has_Internal_Extension (Fname) then
|
||||
return False;
|
||||
@ -128,6 +121,29 @@ package body Fname is
|
||||
-- See the note in Is_Predefined_File_Name for the rationale
|
||||
|
||||
return Fname'Length = 8 and then Has_Prefix (Fname, "gnat");
|
||||
end Is_GNAT_File_Name;
|
||||
|
||||
function Is_GNAT_File_Name (Fname : File_Name_Type) return Boolean is
|
||||
Result : constant Boolean :=
|
||||
Is_GNAT_File_Name (Get_Name_String (Fname));
|
||||
begin
|
||||
return Result;
|
||||
end Is_GNAT_File_Name;
|
||||
|
||||
---------------------------
|
||||
-- Is_Internal_File_Name --
|
||||
---------------------------
|
||||
|
||||
function Is_Internal_File_Name
|
||||
(Fname : String;
|
||||
Renamings_Included : Boolean := True) return Boolean
|
||||
is
|
||||
begin
|
||||
if Is_Predefined_File_Name (Fname, Renamings_Included) then
|
||||
return True;
|
||||
end if;
|
||||
|
||||
return Is_GNAT_File_Name (Fname);
|
||||
end Is_Internal_File_Name;
|
||||
|
||||
function Is_Internal_File_Name
|
||||
@ -149,27 +165,13 @@ package body Fname is
|
||||
(Fname : String;
|
||||
Renamings_Included : Boolean := True) return Boolean
|
||||
is
|
||||
subtype Str8 is String (1 .. 8);
|
||||
|
||||
Renaming_Names : constant array (1 .. 8) of Str8 :=
|
||||
("calendar", -- Calendar
|
||||
"machcode", -- Machine_Code
|
||||
"unchconv", -- Unchecked_Conversion
|
||||
"unchdeal", -- Unchecked_Deallocation
|
||||
"directio", -- Direct_IO
|
||||
"ioexcept", -- IO_Exceptions
|
||||
"sequenio", -- Sequential_IO
|
||||
"text_io."); -- Text_IO
|
||||
|
||||
-- Note: the implementation is optimized to perform uniform comparisons
|
||||
-- on string slices whose length is known at compile time and is a small
|
||||
-- power of 2 (at most 8 characters); the remaining calls to Has_Prefix
|
||||
-- must be inlined to expose the compile-time known length. There must
|
||||
-- be no calls to the fallback string comparison routine (e.g. memcmp)
|
||||
-- left in the object code for the function; this can save up to 10% of
|
||||
-- the entire compilation time spent in the front end.
|
||||
|
||||
begin
|
||||
-- Definitely false if longer than 12 characters (8.3)
|
||||
|
||||
if Fname'Length > 12 then
|
||||
return False;
|
||||
end if;
|
||||
|
||||
if not Has_Internal_Extension (Fname) then
|
||||
return False;
|
||||
end if;
|
||||
@ -186,12 +188,6 @@ package body Fname is
|
||||
end;
|
||||
end if;
|
||||
|
||||
-- Definitely false if longer than 12 characters (8.3)
|
||||
|
||||
if Fname'Length > 12 then
|
||||
return False;
|
||||
end if;
|
||||
|
||||
-- We include the "." in the prefixes below, so we don't match (e.g.)
|
||||
-- adamant.ads. So the first line matches "ada.ads", "ada.adb", and
|
||||
-- "ada.ali". But that's not necessary if they have 8 characters.
|
||||
@ -205,16 +201,10 @@ package body Fname is
|
||||
|
||||
-- If instructed and the name has 8+ characters, check for renamings
|
||||
|
||||
if Renamings_Included and then Fname'Length >= 8 then
|
||||
declare
|
||||
S : String renames Fname (Fname'First .. Fname'First + 7);
|
||||
begin
|
||||
for J in Renaming_Names'Range loop
|
||||
if S = Renaming_Names (J) then
|
||||
return True;
|
||||
end if;
|
||||
end loop;
|
||||
end;
|
||||
if Renamings_Included
|
||||
and then Is_Predefined_Renaming_File_Name (Fname)
|
||||
then
|
||||
return True;
|
||||
end if;
|
||||
|
||||
return False;
|
||||
@ -231,6 +221,50 @@ package body Fname is
|
||||
return Result;
|
||||
end Is_Predefined_File_Name;
|
||||
|
||||
--------------------------------------
|
||||
-- Is_Predefined_Renaming_File_Name --
|
||||
--------------------------------------
|
||||
|
||||
function Is_Predefined_Renaming_File_Name
|
||||
(Fname : String) return Boolean
|
||||
is
|
||||
subtype Str8 is String (1 .. 8);
|
||||
|
||||
Renaming_Names : constant array (1 .. 8) of Str8 :=
|
||||
("calendar", -- Calendar
|
||||
"machcode", -- Machine_Code
|
||||
"unchconv", -- Unchecked_Conversion
|
||||
"unchdeal", -- Unchecked_Deallocation
|
||||
"directio", -- Direct_IO
|
||||
"ioexcept", -- IO_Exceptions
|
||||
"sequenio", -- Sequential_IO
|
||||
"text_io."); -- Text_IO
|
||||
begin
|
||||
-- Definitely false if longer than 12 characters (8.3)
|
||||
|
||||
if Fname'Length in 8 .. 12 then
|
||||
declare
|
||||
S : String renames Fname (Fname'First .. Fname'First + 7);
|
||||
begin
|
||||
for J in Renaming_Names'Range loop
|
||||
if S = Renaming_Names (J) then
|
||||
return True;
|
||||
end if;
|
||||
end loop;
|
||||
end;
|
||||
end if;
|
||||
|
||||
return False;
|
||||
end Is_Predefined_Renaming_File_Name;
|
||||
|
||||
function Is_Predefined_Renaming_File_Name
|
||||
(Fname : File_Name_Type) return Boolean is
|
||||
Result : constant Boolean :=
|
||||
Is_Predefined_Renaming_File_Name (Get_Name_String (Fname));
|
||||
begin
|
||||
return Result;
|
||||
end Is_Predefined_Renaming_File_Name;
|
||||
|
||||
---------------
|
||||
-- Tree_Read --
|
||||
---------------
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- S p e c --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNAT is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
@ -79,6 +79,14 @@ package Fname is
|
||||
-- Renamings_Included is True, then Text_IO will return True, otherwise
|
||||
-- only children of Ada, Interfaces and System return True.
|
||||
|
||||
function Is_Predefined_Renaming_File_Name
|
||||
(Fname : String) return Boolean;
|
||||
function Is_Predefined_Renaming_File_Name
|
||||
(Fname : File_Name_Type) return Boolean;
|
||||
-- True if Fname is the file name for a predefined renaming (the same file
|
||||
-- names that are included if Renamings_Included => True is passed to
|
||||
-- Is_Predefined_File_Name).
|
||||
|
||||
function Is_Internal_File_Name
|
||||
(Fname : String;
|
||||
Renamings_Included : Boolean := True) return Boolean;
|
||||
@ -88,6 +96,10 @@ package Fname is
|
||||
-- Same as Is_Predefined_File_Name, except units in the GNAT hierarchy are
|
||||
-- included.
|
||||
|
||||
function Is_GNAT_File_Name (Fname : String) return Boolean;
|
||||
function Is_GNAT_File_Name (Fname : File_Name_Type) return Boolean;
|
||||
-- True for units in the GNAT hierarchy
|
||||
|
||||
procedure Tree_Read;
|
||||
-- Dummy procedure (reads dummy table values from tree file)
|
||||
|
||||
|
@ -37,7 +37,6 @@ with Exp_Disp; use Exp_Disp;
|
||||
with Exp_Pakd; use Exp_Pakd;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Exp_Tss; use Exp_Tss;
|
||||
with Fname; use Fname;
|
||||
with Ghost; use Ghost;
|
||||
with Layout; use Layout;
|
||||
with Lib; use Lib;
|
||||
@ -8197,7 +8196,7 @@ package body Freeze is
|
||||
if Is_Pure (E)
|
||||
and then Is_Subprogram (E)
|
||||
and then not Has_Pragma_Pure_Function (E)
|
||||
and then not Is_Internal_File_Name (Unit_File_Name (Current_Sem_Unit))
|
||||
and then not Is_Internal_Unit (Current_Sem_Unit)
|
||||
then
|
||||
Check_Function_With_Address_Parameter (E);
|
||||
end if;
|
||||
|
@ -177,7 +177,7 @@ package body GNAT.Command_Line is
|
||||
-- these.
|
||||
|
||||
procedure Sort_Sections
|
||||
(Line : GNAT.OS_Lib.Argument_List_Access;
|
||||
(Line : not null GNAT.OS_Lib.Argument_List_Access;
|
||||
Sections : GNAT.OS_Lib.Argument_List_Access;
|
||||
Params : GNAT.OS_Lib.Argument_List_Access);
|
||||
-- Reorder the command line switches so that the switches belonging to a
|
||||
@ -2792,7 +2792,7 @@ package body GNAT.Command_Line is
|
||||
-------------------
|
||||
|
||||
procedure Sort_Sections
|
||||
(Line : GNAT.OS_Lib.Argument_List_Access;
|
||||
(Line : not null GNAT.OS_Lib.Argument_List_Access;
|
||||
Sections : GNAT.OS_Lib.Argument_List_Access;
|
||||
Params : GNAT.OS_Lib.Argument_List_Access)
|
||||
is
|
||||
@ -2805,10 +2805,6 @@ package body GNAT.Command_Line is
|
||||
Index : Natural;
|
||||
|
||||
begin
|
||||
if Line = null then
|
||||
return;
|
||||
end if;
|
||||
|
||||
-- First construct a list of all sections
|
||||
|
||||
for E in Line'Range loop
|
||||
|
@ -217,8 +217,9 @@ static bool constructor_address_p (tree);
|
||||
static bool allocatable_size_p (tree, bool);
|
||||
static bool initial_value_needs_conversion (tree, tree);
|
||||
static int compare_field_bitpos (const PTR, const PTR);
|
||||
static bool components_to_record (tree, Node_Id, tree, int, bool, bool, bool,
|
||||
bool, bool, bool, bool, bool, tree, tree *);
|
||||
static bool components_to_record (Node_Id, Entity_Id, tree, tree, int, bool,
|
||||
bool, bool, bool, bool, bool, bool, tree,
|
||||
tree *);
|
||||
static Uint annotate_value (tree);
|
||||
static void annotate_rep (Entity_Id, tree);
|
||||
static tree build_position_list (tree, bool, tree, tree, unsigned int, tree);
|
||||
@ -3328,11 +3329,10 @@ gnat_to_gnu_entity (Entity_Id gnat_entity, tree gnu_expr, bool definition)
|
||||
}
|
||||
|
||||
/* Add the fields into the record type and finish it up. */
|
||||
components_to_record (gnu_type, Component_List (record_definition),
|
||||
gnu_field_list, packed, definition, false,
|
||||
all_rep, is_unchecked_union,
|
||||
artificial_p, debug_info_p,
|
||||
false, OK_To_Reorder_Components (gnat_entity),
|
||||
components_to_record (Component_List (record_definition), gnat_entity,
|
||||
gnu_field_list, gnu_type, packed, definition,
|
||||
false, all_rep, is_unchecked_union, artificial_p,
|
||||
debug_info_p, false,
|
||||
all_rep ? NULL_TREE : bitsize_zero_node, NULL);
|
||||
|
||||
/* Fill in locations of fields. */
|
||||
@ -7463,6 +7463,71 @@ compare_field_bitpos (const PTR rt1, const PTR rt2)
|
||||
return ret ? ret : (int) (DECL_UID (field1) - DECL_UID (field2));
|
||||
}
|
||||
|
||||
/* Reverse function from gnat_to_gnu_field: return the GNAT field present in
|
||||
either GNAT_COMPONENT_LIST or the discriminants of GNAT_RECORD_TYPE, and
|
||||
corresponding to the GNU tree GNU_FIELD. */
|
||||
|
||||
static Entity_Id
|
||||
gnu_field_to_gnat (tree gnu_field, Node_Id gnat_component_list,
|
||||
Entity_Id gnat_record_type)
|
||||
{
|
||||
Entity_Id gnat_component_decl, gnat_field;
|
||||
|
||||
if (Present (Component_Items (gnat_component_list)))
|
||||
for (gnat_component_decl
|
||||
= First_Non_Pragma (Component_Items (gnat_component_list));
|
||||
Present (gnat_component_decl);
|
||||
gnat_component_decl = Next_Non_Pragma (gnat_component_decl))
|
||||
{
|
||||
gnat_field = Defining_Entity (gnat_component_decl);
|
||||
if (gnat_to_gnu_field_decl (gnat_field) == gnu_field)
|
||||
return gnat_field;
|
||||
}
|
||||
|
||||
if (Has_Discriminants (gnat_record_type))
|
||||
for (gnat_field = First_Stored_Discriminant (gnat_record_type);
|
||||
Present (gnat_field);
|
||||
gnat_field = Next_Stored_Discriminant (gnat_field))
|
||||
if (gnat_to_gnu_field_decl (gnat_field) == gnu_field)
|
||||
return gnat_field;
|
||||
|
||||
return Empty;
|
||||
}
|
||||
|
||||
/* Issue a warning for the problematic placement of GNU_FIELD present in
|
||||
either GNAT_COMPONENT_LIST or the discriminants of GNAT_RECORD_TYPE.
|
||||
IN_VARIANT is true if GNAT_COMPONENT_LIST is the list of a variant.
|
||||
DO_REORDER is true if fields of GNAT_RECORD_TYPE are being reordered. */
|
||||
|
||||
static void
|
||||
warn_on_field_placement (tree gnu_field, Node_Id gnat_component_list,
|
||||
Entity_Id gnat_record_type, bool in_variant,
|
||||
bool do_reorder)
|
||||
{
|
||||
const char *msg1
|
||||
= in_variant
|
||||
? "?variant layout may cause performance issues"
|
||||
: "?record layout may cause performance issues";
|
||||
const char *msg2
|
||||
= field_has_self_size (gnu_field)
|
||||
? "?component & whose length depends on a discriminant"
|
||||
: field_has_variable_size (gnu_field)
|
||||
? "?component & whose length is not fixed"
|
||||
: "?component & whose length is not multiple of a byte";
|
||||
const char *msg3
|
||||
= do_reorder
|
||||
? "?comes too early and was moved down"
|
||||
: "?comes too early and ought to be moved down";
|
||||
Entity_Id gnat_field
|
||||
= gnu_field_to_gnat (gnu_field, gnat_component_list, gnat_record_type);
|
||||
|
||||
gcc_assert (Present (gnat_field));
|
||||
|
||||
post_error (msg1, gnat_field);
|
||||
post_error_ne (msg2, gnat_field, gnat_field);
|
||||
post_error (msg3, gnat_field);
|
||||
}
|
||||
|
||||
/* Structure holding information for a given variant. */
|
||||
typedef struct vinfo
|
||||
{
|
||||
@ -7483,14 +7548,15 @@ typedef struct vinfo
|
||||
|
||||
} vinfo_t;
|
||||
|
||||
/* Translate and chain the GNAT_COMPONENT_LIST to the GNU_FIELD_LIST, set the
|
||||
result as the field list of GNU_RECORD_TYPE and finish it up. Return true
|
||||
if GNU_RECORD_TYPE has a rep clause which affects the layout (see below).
|
||||
When called from gnat_to_gnu_entity during the processing of a record type
|
||||
definition, the GCC node for the parent, if any, will be the single field
|
||||
of GNU_RECORD_TYPE and the GCC nodes for the discriminants will be on the
|
||||
GNU_FIELD_LIST. The other calls to this function are recursive calls for
|
||||
the component list of a variant and, in this case, GNU_FIELD_LIST is empty.
|
||||
/* Translate and chain GNAT_COMPONENT_LIST present in GNAT_RECORD_TYPE to
|
||||
GNU_FIELD_LIST, set the result as the field list of GNU_RECORD_TYPE and
|
||||
finish it up. Return true if GNU_RECORD_TYPE has a rep clause that affects
|
||||
the layout (see below). When called from gnat_to_gnu_entity during the
|
||||
processing of a record definition, the GCC node for the parent, if any,
|
||||
will be the single field of GNU_RECORD_TYPE and the GCC nodes for the
|
||||
discriminants will be on GNU_FIELD_LIST. The other call to this function
|
||||
is a recursive call for the component list of a variant and, in this case,
|
||||
GNU_FIELD_LIST is empty.
|
||||
|
||||
PACKED is 1 if this is for a packed record or -1 if this is for a record
|
||||
with Component_Alignment of Storage_Unit.
|
||||
@ -7514,8 +7580,6 @@ typedef struct vinfo
|
||||
MAYBE_UNUSED is true if this type may be unused in the end; this doesn't
|
||||
mean that its contents may be unused as well, only the container itself.
|
||||
|
||||
REORDER is true if we are permitted to reorder components of this type.
|
||||
|
||||
FIRST_FREE_POS, if nonzero, is the first (lowest) free field position in
|
||||
the outer record type down to this variant level. It is nonzero only if
|
||||
all the fields down to this level have a rep clause and ALL_REP is false.
|
||||
@ -7525,12 +7589,12 @@ typedef struct vinfo
|
||||
be done with such fields and the return value will be false. */
|
||||
|
||||
static bool
|
||||
components_to_record (tree gnu_record_type, Node_Id gnat_component_list,
|
||||
tree gnu_field_list, int packed, bool definition,
|
||||
bool cancel_alignment, bool all_rep,
|
||||
bool unchecked_union, bool artificial,
|
||||
bool debug_info, bool maybe_unused, bool reorder,
|
||||
tree first_free_pos, tree *p_gnu_rep_list)
|
||||
components_to_record (Node_Id gnat_component_list, Entity_Id gnat_record_type,
|
||||
tree gnu_field_list, tree gnu_record_type, int packed,
|
||||
bool definition, bool cancel_alignment, bool all_rep,
|
||||
bool unchecked_union, bool artificial, bool debug_info,
|
||||
bool maybe_unused, tree first_free_pos,
|
||||
tree *p_gnu_rep_list)
|
||||
{
|
||||
const bool needs_xv_encodings
|
||||
= debug_info && gnat_encodings != DWARF_GNAT_ENCODINGS_MINIMAL;
|
||||
@ -7539,24 +7603,21 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list,
|
||||
bool layout_with_rep = false;
|
||||
bool has_self_field = false;
|
||||
bool has_aliased_after_self_field = false;
|
||||
Node_Id component_decl, variant_part;
|
||||
Entity_Id gnat_component_decl, gnat_variant_part;
|
||||
tree gnu_field, gnu_next, gnu_last;
|
||||
tree gnu_variant_part = NULL_TREE;
|
||||
tree gnu_rep_list = NULL_TREE;
|
||||
tree gnu_var_list = NULL_TREE;
|
||||
tree gnu_self_list = NULL_TREE;
|
||||
tree gnu_zero_list = NULL_TREE;
|
||||
|
||||
/* For each component referenced in a component declaration create a GCC
|
||||
field and add it to the list, skipping pragmas in the GNAT list. */
|
||||
gnu_last = tree_last (gnu_field_list);
|
||||
if (Present (Component_Items (gnat_component_list)))
|
||||
for (component_decl
|
||||
for (gnat_component_decl
|
||||
= First_Non_Pragma (Component_Items (gnat_component_list));
|
||||
Present (component_decl);
|
||||
component_decl = Next_Non_Pragma (component_decl))
|
||||
Present (gnat_component_decl);
|
||||
gnat_component_decl = Next_Non_Pragma (gnat_component_decl))
|
||||
{
|
||||
Entity_Id gnat_field = Defining_Entity (component_decl);
|
||||
Entity_Id gnat_field = Defining_Entity (gnat_component_decl);
|
||||
Name_Id gnat_name = Chars (gnat_field);
|
||||
|
||||
/* If present, the _Parent field must have been created as the single
|
||||
@ -7603,7 +7664,7 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list,
|
||||
}
|
||||
|
||||
/* At the end of the component list there may be a variant part. */
|
||||
variant_part = Variant_Part (gnat_component_list);
|
||||
gnat_variant_part = Variant_Part (gnat_component_list);
|
||||
|
||||
/* We create a QUAL_UNION_TYPE for the variant part since the variants are
|
||||
mutually exclusive and should go in the same memory. To do this we need
|
||||
@ -7612,9 +7673,9 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list,
|
||||
lists for the variants and put them all into the QUAL_UNION_TYPE.
|
||||
If this is an Unchecked_Union, we make a UNION_TYPE instead or
|
||||
use GNU_RECORD_TYPE if there are no fields so far. */
|
||||
if (Present (variant_part))
|
||||
if (Present (gnat_variant_part))
|
||||
{
|
||||
Node_Id gnat_discr = Name (variant_part), variant;
|
||||
Node_Id gnat_discr = Name (gnat_variant_part), variant;
|
||||
tree gnu_discr = gnat_to_gnu (gnat_discr);
|
||||
tree gnu_name = TYPE_IDENTIFIER (gnu_record_type);
|
||||
tree gnu_var_name
|
||||
@ -7676,7 +7737,7 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list,
|
||||
the container types and computing the associated properties. However
|
||||
we cannot finish up the container types during this pass because we
|
||||
don't know where the variant part will be placed until the end. */
|
||||
for (variant = First_Non_Pragma (Variants (variant_part));
|
||||
for (variant = First_Non_Pragma (Variants (gnat_variant_part));
|
||||
Present (variant);
|
||||
variant = Next_Non_Pragma (variant))
|
||||
{
|
||||
@ -7712,12 +7773,11 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list,
|
||||
/* Add the fields into the record type for the variant. Note that
|
||||
we aren't sure to really use it at this point, see below. */
|
||||
has_rep
|
||||
= components_to_record (gnu_variant_type, Component_List (variant),
|
||||
NULL_TREE, packed, definition,
|
||||
!all_rep_and_size, all_rep,
|
||||
unchecked_union,
|
||||
true, needs_xv_encodings, true, reorder,
|
||||
this_first_free_pos,
|
||||
= components_to_record (Component_List (variant), gnat_record_type,
|
||||
NULL_TREE, gnu_variant_type, packed,
|
||||
definition, !all_rep_and_size, all_rep,
|
||||
unchecked_union, true, needs_xv_encodings,
|
||||
true, this_first_free_pos,
|
||||
all_rep || this_first_free_pos
|
||||
? NULL : &gnu_rep_list);
|
||||
|
||||
@ -7873,19 +7933,44 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list,
|
||||
}
|
||||
}
|
||||
|
||||
/* Scan GNU_FIELD_LIST and see if any fields have rep clauses and, if we are
|
||||
permitted to reorder components, self-referential sizes or variable sizes.
|
||||
If they do, pull them out and put them onto the appropriate list. We have
|
||||
to do this in a separate pass since we want to handle the discriminants
|
||||
but can't play with them until we've used them in debugging data above.
|
||||
/* Scan GNU_FIELD_LIST and see if any fields have rep clauses. If they do,
|
||||
pull them out and put them onto the appropriate list. We have to do it
|
||||
in a separate pass since we want to handle the discriminants but can't
|
||||
play with them until we've used them in debugging data above.
|
||||
|
||||
Similarly, pull out the fields with zero size and no rep clause, as they
|
||||
would otherwise modify the layout and thus very likely run afoul of the
|
||||
Ada semantics, which are different from those of C here.
|
||||
|
||||
Finally, if there is an aliased field placed in the list after fields
|
||||
with self-referential size, pull out the latter in the same way.
|
||||
|
||||
Optionally, if the reordering mechanism is enabled, pull out the fields
|
||||
with self-referential size, variable size and fixed size not a multiple
|
||||
of a byte, so that they don't cause the regular fields to be either at
|
||||
self-referential/variable offset or misaligned. Note, in the latter
|
||||
case, that this can only happen in packed record types so the alignment
|
||||
is effectively capped to the byte for the whole record.
|
||||
|
||||
Optionally, if the layout warning is enabled, keep track of the above 4
|
||||
different kinds of fields and issue a warning if some of them would be
|
||||
(or are being) reordered by the reordering mechanism.
|
||||
|
||||
??? If we reorder them, debugging information will be wrong but there is
|
||||
nothing that can be done about this at the moment. */
|
||||
gnu_last = NULL_TREE;
|
||||
const bool do_reorder = OK_To_Reorder_Components (gnat_record_type);
|
||||
const bool w_reorder
|
||||
= Warn_On_Questionable_Layout
|
||||
&& (Convention (gnat_record_type) == Convention_Ada);
|
||||
const bool in_variant = (p_gnu_rep_list != NULL);
|
||||
tree gnu_zero_list = NULL_TREE;
|
||||
tree gnu_self_list = NULL_TREE;
|
||||
tree gnu_var_list = NULL_TREE;
|
||||
tree gnu_bitp_list = NULL_TREE;
|
||||
tree gnu_tmp_bitp_list = NULL_TREE;
|
||||
unsigned int tmp_bitp_size = 0;
|
||||
unsigned int last_reorder_field_type = -1;
|
||||
unsigned int tmp_last_reorder_field_type = -1;
|
||||
|
||||
#define MOVE_FROM_FIELD_LIST_TO(LIST) \
|
||||
do { \
|
||||
@ -7898,6 +7983,7 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list,
|
||||
(LIST) = gnu_field; \
|
||||
} while (0)
|
||||
|
||||
gnu_last = NULL_TREE;
|
||||
for (gnu_field = gnu_field_list; gnu_field; gnu_field = gnu_next)
|
||||
{
|
||||
gnu_next = DECL_CHAIN (gnu_field);
|
||||
@ -7908,19 +7994,6 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list,
|
||||
continue;
|
||||
}
|
||||
|
||||
if ((reorder || has_aliased_after_self_field)
|
||||
&& field_has_self_size (gnu_field))
|
||||
{
|
||||
MOVE_FROM_FIELD_LIST_TO (gnu_self_list);
|
||||
continue;
|
||||
}
|
||||
|
||||
if (reorder && field_has_variable_size (gnu_field))
|
||||
{
|
||||
MOVE_FROM_FIELD_LIST_TO (gnu_var_list);
|
||||
continue;
|
||||
}
|
||||
|
||||
if (DECL_SIZE (gnu_field) && integer_zerop (DECL_SIZE (gnu_field)))
|
||||
{
|
||||
DECL_FIELD_OFFSET (gnu_field) = size_zero_node;
|
||||
@ -7934,6 +8007,129 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list,
|
||||
continue;
|
||||
}
|
||||
|
||||
if (has_aliased_after_self_field && field_has_self_size (gnu_field))
|
||||
{
|
||||
MOVE_FROM_FIELD_LIST_TO (gnu_self_list);
|
||||
continue;
|
||||
}
|
||||
|
||||
/* We don't need further processing in default mode. */
|
||||
if (!w_reorder && !do_reorder)
|
||||
{
|
||||
gnu_last = gnu_field;
|
||||
continue;
|
||||
}
|
||||
|
||||
if (field_has_self_size (gnu_field))
|
||||
{
|
||||
if (w_reorder)
|
||||
{
|
||||
if (last_reorder_field_type < 4)
|
||||
warn_on_field_placement (gnu_field, gnat_component_list,
|
||||
gnat_record_type, in_variant,
|
||||
do_reorder);
|
||||
else
|
||||
last_reorder_field_type = 4;
|
||||
}
|
||||
|
||||
if (do_reorder)
|
||||
{
|
||||
MOVE_FROM_FIELD_LIST_TO (gnu_self_list);
|
||||
continue;
|
||||
}
|
||||
}
|
||||
|
||||
else if (field_has_variable_size (gnu_field))
|
||||
{
|
||||
if (w_reorder)
|
||||
{
|
||||
if (last_reorder_field_type < 3)
|
||||
warn_on_field_placement (gnu_field, gnat_component_list,
|
||||
gnat_record_type, in_variant,
|
||||
do_reorder);
|
||||
else
|
||||
last_reorder_field_type = 3;
|
||||
}
|
||||
|
||||
if (do_reorder)
|
||||
{
|
||||
MOVE_FROM_FIELD_LIST_TO (gnu_var_list);
|
||||
continue;
|
||||
}
|
||||
}
|
||||
|
||||
else
|
||||
{
|
||||
/* If the field has no size, then it cannot be bit-packed. */
|
||||
const unsigned int bitp_size
|
||||
= DECL_SIZE (gnu_field)
|
||||
? TREE_INT_CST_LOW (DECL_SIZE (gnu_field)) % BITS_PER_UNIT
|
||||
: 0;
|
||||
|
||||
/* If the field is bit-packed, we move it to a temporary list that
|
||||
contains the contiguously preceding bit-packed fields, because
|
||||
we want to be able to put them back if the misalignment happens
|
||||
to cancel itself after several bit-packed fields. */
|
||||
if (bitp_size != 0)
|
||||
{
|
||||
tmp_bitp_size = (tmp_bitp_size + bitp_size) % BITS_PER_UNIT;
|
||||
|
||||
if (last_reorder_field_type != 2)
|
||||
{
|
||||
tmp_last_reorder_field_type = last_reorder_field_type;
|
||||
last_reorder_field_type = 2;
|
||||
}
|
||||
|
||||
if (do_reorder)
|
||||
{
|
||||
MOVE_FROM_FIELD_LIST_TO (gnu_tmp_bitp_list);
|
||||
continue;
|
||||
}
|
||||
}
|
||||
|
||||
/* No more bit-packed fields, move the existing ones to the end or
|
||||
put them back at their original location. */
|
||||
else if (last_reorder_field_type == 2 || gnu_tmp_bitp_list)
|
||||
{
|
||||
last_reorder_field_type = 1;
|
||||
|
||||
if (tmp_bitp_size != 0)
|
||||
{
|
||||
if (w_reorder && tmp_last_reorder_field_type < 2)
|
||||
warn_on_field_placement (gnu_tmp_bitp_list
|
||||
? gnu_tmp_bitp_list : gnu_last,
|
||||
gnat_component_list,
|
||||
gnat_record_type, in_variant,
|
||||
do_reorder);
|
||||
|
||||
if (do_reorder)
|
||||
gnu_bitp_list = chainon (gnu_tmp_bitp_list, gnu_bitp_list);
|
||||
|
||||
gnu_tmp_bitp_list = NULL_TREE;
|
||||
tmp_bitp_size = 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
/* Rechain the temporary list in front of GNU_FIELD. */
|
||||
tree gnu_bitp_field = gnu_field;
|
||||
while (gnu_tmp_bitp_list)
|
||||
{
|
||||
tree gnu_bitp_next = DECL_CHAIN (gnu_tmp_bitp_list);
|
||||
DECL_CHAIN (gnu_tmp_bitp_list) = gnu_bitp_field;
|
||||
if (gnu_last)
|
||||
DECL_CHAIN (gnu_last) = gnu_tmp_bitp_list;
|
||||
else
|
||||
gnu_field_list = gnu_tmp_bitp_list;
|
||||
gnu_bitp_field = gnu_tmp_bitp_list;
|
||||
gnu_tmp_bitp_list = gnu_bitp_next;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
else
|
||||
last_reorder_field_type = 1;
|
||||
}
|
||||
|
||||
gnu_last = gnu_field;
|
||||
}
|
||||
|
||||
@ -7943,15 +8139,30 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list,
|
||||
|
||||
/* If permitted, we reorder the fields as follows:
|
||||
|
||||
1) all fixed length fields,
|
||||
2) all fields whose length doesn't depend on discriminants,
|
||||
3) all fields whose length depends on discriminants,
|
||||
4) the variant part,
|
||||
1) all (groups of) fields whose length is fixed and multiple of a byte,
|
||||
2) the remaining fields whose length is fixed and not multiple of a byte,
|
||||
3) the remaining fields whose length doesn't depend on discriminants,
|
||||
4) all fields whose length depends on discriminants,
|
||||
5) the variant part,
|
||||
|
||||
within the record and within each variant recursively. */
|
||||
if (reorder)
|
||||
gnu_field_list
|
||||
= chainon (gnu_field_list, chainon (gnu_var_list, gnu_self_list));
|
||||
if (w_reorder
|
||||
&& last_reorder_field_type == 2
|
||||
&& tmp_last_reorder_field_type < 2)
|
||||
warn_on_field_placement (gnu_tmp_bitp_list
|
||||
? gnu_tmp_bitp_list : gnu_field_list,
|
||||
gnat_component_list, gnat_record_type,
|
||||
in_variant, do_reorder);
|
||||
if (do_reorder)
|
||||
{
|
||||
if (gnu_tmp_bitp_list)
|
||||
gnu_bitp_list = chainon (gnu_tmp_bitp_list, gnu_bitp_list);
|
||||
|
||||
gnu_field_list
|
||||
= chainon (gnu_field_list,
|
||||
chainon (gnu_bitp_list,
|
||||
chainon (gnu_var_list, gnu_self_list)));
|
||||
}
|
||||
|
||||
/* Otherwise, if there is an aliased field placed after a field whose length
|
||||
depends on discriminants, we put all the fields of the latter sort, last.
|
||||
|
@ -500,26 +500,29 @@ procedure Gnat1drv is
|
||||
-- Detect that the runtime library support for floating-point numbers
|
||||
-- may not be compatible with SPARK analysis of IEEE-754 floats.
|
||||
|
||||
if Denorm_On_Target = False then
|
||||
Write_Line
|
||||
("warning: Run-time library may be configured incorrectly");
|
||||
Write_Line
|
||||
("warning: "
|
||||
& "(SPARK analysis requires support for float subnormals)");
|
||||
declare
|
||||
procedure SPARK_Library_Warning (Kind : String);
|
||||
-- Issue a warning in GNATprove mode if the run-time library does
|
||||
-- not fully support IEEE-754 floating-point semantics.
|
||||
|
||||
elsif Machine_Rounds_On_Target = False then
|
||||
Write_Line
|
||||
("warning: Run-time library may be configured incorrectly");
|
||||
Write_Line
|
||||
("warning: "
|
||||
& "(SPARK analysis requires support for float rounding)");
|
||||
procedure SPARK_Library_Warning (Kind : String) is
|
||||
begin
|
||||
Write_Line
|
||||
("warning: run-time library may be configured incorrectly");
|
||||
Write_Line
|
||||
("warning: (SPARK analysis requires support for " & Kind
|
||||
& ')');
|
||||
end SPARK_Library_Warning;
|
||||
|
||||
elsif Signed_Zeros_On_Target = False then
|
||||
Write_Line
|
||||
("warning: Run-time library may be configured incorrectly");
|
||||
Write_Line
|
||||
("warning: (SPARK analysis requires support for signed zeros)");
|
||||
end if;
|
||||
begin
|
||||
if Denorm_On_Target = False then
|
||||
SPARK_Library_Warning ("float subnormals");
|
||||
elsif Machine_Rounds_On_Target = False then
|
||||
SPARK_Library_Warning ("float rounding");
|
||||
elsif Signed_Zeros_On_Target = False then
|
||||
SPARK_Library_Warning ("signed zeros");
|
||||
end if;
|
||||
end;
|
||||
end if;
|
||||
|
||||
-- Set Configurable_Run_Time mode if system.ads flag set or if the
|
||||
|
@ -410,8 +410,7 @@ package body Inline is
|
||||
|
||||
if not Comes_From_Source (N)
|
||||
and then In_Extended_Main_Source_Unit (N)
|
||||
and then
|
||||
Is_Predefined_File_Name (Unit_File_Name (Get_Source_Unit (E)))
|
||||
and then Is_Predefined_Unit (Get_Source_Unit (E))
|
||||
then
|
||||
Set_Needs_Debug_Info (E, False);
|
||||
end if;
|
||||
@ -1556,7 +1555,7 @@ package body Inline is
|
||||
-- subprograms may contain nested subprograms and become ineligible
|
||||
-- for inlining.
|
||||
|
||||
if Is_Predefined_File_Name (Unit_File_Name (Get_Source_Unit (Subp)))
|
||||
if Is_Predefined_Unit (Get_Source_Unit (Subp))
|
||||
and then not In_Extended_Main_Source_Unit (Subp)
|
||||
then
|
||||
null;
|
||||
@ -1602,7 +1601,7 @@ package body Inline is
|
||||
-- compatibility but it will be removed when we enforce the
|
||||
-- strictness of the new rules.
|
||||
|
||||
if Is_Predefined_File_Name (Unit_File_Name (Get_Source_Unit (Subp)))
|
||||
if Is_Predefined_Unit (Get_Source_Unit (Subp))
|
||||
and then not In_Extended_Main_Source_Unit (Subp)
|
||||
then
|
||||
null;
|
||||
@ -1617,9 +1616,7 @@ package body Inline is
|
||||
declare
|
||||
Gen_P : constant Entity_Id := Generic_Parent (Parent (Subp));
|
||||
begin
|
||||
if Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Gen_P)))
|
||||
then
|
||||
if Is_Predefined_Unit (Get_Source_Unit (Gen_P)) then
|
||||
Set_Is_Inlined (Subp, False);
|
||||
Error_Msg_NE (Msg & "p?", N, Subp);
|
||||
return;
|
||||
@ -2283,8 +2280,7 @@ package body Inline is
|
||||
is
|
||||
Loc : constant Source_Ptr := Sloc (N);
|
||||
Is_Predef : constant Boolean :=
|
||||
Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Subp)));
|
||||
Is_Predefined_Unit (Get_Source_Unit (Subp));
|
||||
Orig_Bod : constant Node_Id :=
|
||||
Body_To_Inline (Unit_Declaration_Node (Subp));
|
||||
|
||||
@ -3565,8 +3561,7 @@ package body Inline is
|
||||
end if;
|
||||
|
||||
return Present (Conv)
|
||||
and then Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Conv)))
|
||||
and then Is_Predefined_Unit (Get_Source_Unit (Conv))
|
||||
and then Is_Intrinsic_Subprogram (Conv);
|
||||
end Is_Unchecked_Conversion;
|
||||
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2009, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNAT is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
@ -78,9 +78,7 @@ begin
|
||||
|
||||
for R in Sorted_Units'Range loop
|
||||
if File_Names_Only then
|
||||
if not Is_Internal_File_Name
|
||||
(File_Name (Source_Index (Sorted_Units (R))))
|
||||
then
|
||||
if not Is_Internal_Unit (Sorted_Units (R)) then
|
||||
Write_Name (Full_File_Name (Source_Index (Sorted_Units (R))));
|
||||
Write_Eol;
|
||||
end if;
|
||||
|
@ -145,7 +145,15 @@ package body Lib.Load is
|
||||
Cunit : Node_Id;
|
||||
Du_Name : Node_Or_Entity_Id;
|
||||
End_Lab : Node_Id;
|
||||
Save_CS : constant Boolean := Get_Comes_From_Source_Default;
|
||||
Fname : constant File_Name_Type :=
|
||||
Get_File_Name (Spec_Name, Subunit => False);
|
||||
Pre_Name : constant Boolean :=
|
||||
Is_Predefined_File_Name (Fname, Renamings_Included => False);
|
||||
Ren_Name : constant Boolean :=
|
||||
Is_Predefined_Renaming_File_Name (Fname);
|
||||
GNAT_Name : constant Boolean :=
|
||||
Is_GNAT_File_Name (Fname);
|
||||
Save_CS : constant Boolean := Get_Comes_From_Source_Default;
|
||||
|
||||
begin
|
||||
-- The created dummy package unit does not come from source
|
||||
@ -205,29 +213,35 @@ package body Lib.Load is
|
||||
Units.Increment_Last;
|
||||
Unum := Units.Last;
|
||||
|
||||
Units.Table (Unum) := (
|
||||
Cunit => Cunit,
|
||||
Cunit_Entity => Cunit_Entity,
|
||||
Dependency_Num => 0,
|
||||
Dynamic_Elab => False,
|
||||
Error_Location => Sloc (With_Node),
|
||||
Expected_Unit => Spec_Name,
|
||||
Fatal_Error => Error_Detected,
|
||||
Generate_Code => False,
|
||||
Has_RACW => False,
|
||||
Filler => False,
|
||||
Ident_String => Empty,
|
||||
Loading => False,
|
||||
Main_Priority => Default_Main_Priority,
|
||||
Main_CPU => Default_Main_CPU,
|
||||
Munit_Index => 0,
|
||||
No_Elab_Code_All => False,
|
||||
Serial_Number => 0,
|
||||
Source_Index => No_Source_File,
|
||||
Unit_File_Name => Get_File_Name (Spec_Name, Subunit => False),
|
||||
Unit_Name => Spec_Name,
|
||||
Version => 0,
|
||||
OA_Setting => 'O');
|
||||
Units.Table (Unum) :=
|
||||
(Cunit => Cunit,
|
||||
Cunit_Entity => Cunit_Entity,
|
||||
Dependency_Num => 0,
|
||||
Dynamic_Elab => False,
|
||||
Error_Location => Sloc (With_Node),
|
||||
Expected_Unit => Spec_Name,
|
||||
Fatal_Error => Error_Detected,
|
||||
Generate_Code => False,
|
||||
Has_RACW => False,
|
||||
Filler => False,
|
||||
Ident_String => Empty,
|
||||
|
||||
Is_Predefined_Renaming => Ren_Name,
|
||||
Is_Predefined_Unit => Pre_Name or Ren_Name,
|
||||
Is_Internal_Unit => Pre_Name or Ren_Name or GNAT_Name,
|
||||
Filler2 => False,
|
||||
|
||||
Loading => False,
|
||||
Main_Priority => Default_Main_Priority,
|
||||
Main_CPU => Default_Main_CPU,
|
||||
Munit_Index => 0,
|
||||
No_Elab_Code_All => False,
|
||||
Serial_Number => 0,
|
||||
Source_Index => No_Source_File,
|
||||
Unit_File_Name => Fname,
|
||||
Unit_Name => Spec_Name,
|
||||
Version => 0,
|
||||
OA_Setting => 'O');
|
||||
|
||||
Set_Comes_From_Source_Default (Save_CS);
|
||||
Set_Error_Posted (Cunit_Entity);
|
||||
@ -285,7 +299,13 @@ package body Lib.Load is
|
||||
----------------------
|
||||
|
||||
procedure Load_Main_Source is
|
||||
Fname : File_Name_Type;
|
||||
Fname : constant File_Name_Type := Next_Main_Source;
|
||||
Pre_Name : constant Boolean :=
|
||||
Is_Predefined_File_Name (Fname, Renamings_Included => False);
|
||||
Ren_Name : constant Boolean :=
|
||||
Is_Predefined_Renaming_File_Name (Fname);
|
||||
GNAT_Name : constant Boolean :=
|
||||
Is_GNAT_File_Name (Fname);
|
||||
Version : Word := 0;
|
||||
|
||||
begin
|
||||
@ -299,7 +319,6 @@ package body Lib.Load is
|
||||
-- Cunit_Entity fields also get filled in later by the parser.
|
||||
|
||||
Units.Increment_Last;
|
||||
Fname := Next_Main_Source;
|
||||
|
||||
Units.Table (Main_Unit).Unit_File_Name := Fname;
|
||||
|
||||
@ -311,29 +330,35 @@ package body Lib.Load is
|
||||
Version := Source_Checksum (Main_Source_File);
|
||||
end if;
|
||||
|
||||
Units.Table (Main_Unit) := (
|
||||
Cunit => Empty,
|
||||
Cunit_Entity => Empty,
|
||||
Dependency_Num => 0,
|
||||
Dynamic_Elab => False,
|
||||
Error_Location => No_Location,
|
||||
Expected_Unit => No_Unit_Name,
|
||||
Fatal_Error => None,
|
||||
Generate_Code => False,
|
||||
Has_RACW => False,
|
||||
Filler => False,
|
||||
Ident_String => Empty,
|
||||
Loading => True,
|
||||
Main_Priority => Default_Main_Priority,
|
||||
Main_CPU => Default_Main_CPU,
|
||||
Munit_Index => 0,
|
||||
No_Elab_Code_All => False,
|
||||
Serial_Number => 0,
|
||||
Source_Index => Main_Source_File,
|
||||
Unit_File_Name => Fname,
|
||||
Unit_Name => No_Unit_Name,
|
||||
Version => Version,
|
||||
OA_Setting => 'O');
|
||||
Units.Table (Main_Unit) :=
|
||||
(Cunit => Empty,
|
||||
Cunit_Entity => Empty,
|
||||
Dependency_Num => 0,
|
||||
Dynamic_Elab => False,
|
||||
Error_Location => No_Location,
|
||||
Expected_Unit => No_Unit_Name,
|
||||
Fatal_Error => None,
|
||||
Generate_Code => False,
|
||||
Has_RACW => False,
|
||||
Filler => False,
|
||||
Ident_String => Empty,
|
||||
|
||||
Is_Predefined_Renaming => Ren_Name,
|
||||
Is_Predefined_Unit => Pre_Name or Ren_Name,
|
||||
Is_Internal_Unit => Pre_Name or Ren_Name or GNAT_Name,
|
||||
Filler2 => False,
|
||||
|
||||
Loading => True,
|
||||
Main_Priority => Default_Main_Priority,
|
||||
Main_CPU => Default_Main_CPU,
|
||||
Munit_Index => 0,
|
||||
No_Elab_Code_All => False,
|
||||
Serial_Number => 0,
|
||||
Source_Index => Main_Source_File,
|
||||
Unit_File_Name => Fname,
|
||||
Unit_Name => No_Unit_Name,
|
||||
Version => Version,
|
||||
OA_Setting => 'O');
|
||||
end if;
|
||||
end Load_Main_Source;
|
||||
|
||||
@ -356,6 +381,9 @@ package body Lib.Load is
|
||||
Unum : Unit_Number_Type;
|
||||
Unump : Unit_Number_Type;
|
||||
Fname : File_Name_Type;
|
||||
Pre_Name : Boolean;
|
||||
Ren_Name : Boolean;
|
||||
GNAT_Name : Boolean;
|
||||
Src_Ind : Source_File_Index;
|
||||
Save_PMES : constant Boolean := Parsing_Main_Extended_Source;
|
||||
|
||||
@ -467,7 +495,11 @@ package body Lib.Load is
|
||||
Uname_Actual := Load_Name;
|
||||
end if;
|
||||
|
||||
Fname := Get_File_Name (Uname_Actual, Subunit);
|
||||
Fname := Get_File_Name (Uname_Actual, Subunit);
|
||||
Pre_Name :=
|
||||
Is_Predefined_File_Name (Fname, Renamings_Included => False);
|
||||
Ren_Name := Is_Predefined_Renaming_File_Name (Fname);
|
||||
GNAT_Name := Is_GNAT_File_Name (Fname);
|
||||
|
||||
if Debug_Flag_L then
|
||||
Write_Eol;
|
||||
@ -676,29 +708,35 @@ package body Lib.Load is
|
||||
-- File was found
|
||||
|
||||
if Src_Ind /= No_Source_File then
|
||||
Units.Table (Unum) := (
|
||||
Cunit => Empty,
|
||||
Cunit_Entity => Empty,
|
||||
Dependency_Num => 0,
|
||||
Dynamic_Elab => False,
|
||||
Error_Location => Sloc (Error_Node),
|
||||
Expected_Unit => Uname_Actual,
|
||||
Fatal_Error => None,
|
||||
Generate_Code => False,
|
||||
Has_RACW => False,
|
||||
Filler => False,
|
||||
Ident_String => Empty,
|
||||
Loading => True,
|
||||
Main_Priority => Default_Main_Priority,
|
||||
Main_CPU => Default_Main_CPU,
|
||||
Munit_Index => 0,
|
||||
No_Elab_Code_All => False,
|
||||
Serial_Number => 0,
|
||||
Source_Index => Src_Ind,
|
||||
Unit_File_Name => Fname,
|
||||
Unit_Name => Uname_Actual,
|
||||
Version => Source_Checksum (Src_Ind),
|
||||
OA_Setting => 'O');
|
||||
Units.Table (Unum) :=
|
||||
(Cunit => Empty,
|
||||
Cunit_Entity => Empty,
|
||||
Dependency_Num => 0,
|
||||
Dynamic_Elab => False,
|
||||
Error_Location => Sloc (Error_Node),
|
||||
Expected_Unit => Uname_Actual,
|
||||
Fatal_Error => None,
|
||||
Generate_Code => False,
|
||||
Has_RACW => False,
|
||||
Filler => False,
|
||||
Ident_String => Empty,
|
||||
|
||||
Is_Predefined_Renaming => Ren_Name,
|
||||
Is_Predefined_Unit => Pre_Name or Ren_Name,
|
||||
Is_Internal_Unit => Pre_Name or Ren_Name or GNAT_Name,
|
||||
Filler2 => False,
|
||||
|
||||
Loading => True,
|
||||
Main_Priority => Default_Main_Priority,
|
||||
Main_CPU => Default_Main_CPU,
|
||||
Munit_Index => 0,
|
||||
No_Elab_Code_All => False,
|
||||
Serial_Number => 0,
|
||||
Source_Index => Src_Ind,
|
||||
Unit_File_Name => Fname,
|
||||
Unit_Name => Uname_Actual,
|
||||
Version => Source_Checksum (Src_Ind),
|
||||
OA_Setting => 'O');
|
||||
|
||||
-- Parse the new unit
|
||||
|
||||
@ -880,7 +918,7 @@ package body Lib.Load is
|
||||
-- code will have to be generated for it.
|
||||
|
||||
procedure Make_Instance_Unit (N : Node_Id; In_Main : Boolean) is
|
||||
Sind : constant Source_File_Index := Source_Index (Main_Unit);
|
||||
Sind : constant Source_File_Index := Source_Index (Main_Unit);
|
||||
|
||||
begin
|
||||
Units.Increment_Last;
|
||||
|
@ -74,28 +74,32 @@ package body Lib.Writ is
|
||||
begin
|
||||
Units.Increment_Last;
|
||||
Units.Table (Units.Last) :=
|
||||
(Unit_File_Name => File_Name (S),
|
||||
Unit_Name => No_Unit_Name,
|
||||
Expected_Unit => No_Unit_Name,
|
||||
Source_Index => S,
|
||||
Cunit => Empty,
|
||||
Cunit_Entity => Empty,
|
||||
Dependency_Num => 0,
|
||||
Dynamic_Elab => False,
|
||||
Fatal_Error => None,
|
||||
Generate_Code => False,
|
||||
Has_RACW => False,
|
||||
Filler => False,
|
||||
Ident_String => Empty,
|
||||
Loading => False,
|
||||
Main_Priority => -1,
|
||||
Main_CPU => -1,
|
||||
Munit_Index => 0,
|
||||
No_Elab_Code_All => False,
|
||||
Serial_Number => 0,
|
||||
Version => 0,
|
||||
Error_Location => No_Location,
|
||||
OA_Setting => 'O');
|
||||
(Unit_File_Name => File_Name (S),
|
||||
Unit_Name => No_Unit_Name,
|
||||
Expected_Unit => No_Unit_Name,
|
||||
Source_Index => S,
|
||||
Cunit => Empty,
|
||||
Cunit_Entity => Empty,
|
||||
Dependency_Num => 0,
|
||||
Dynamic_Elab => False,
|
||||
Fatal_Error => None,
|
||||
Generate_Code => False,
|
||||
Has_RACW => False,
|
||||
Filler => False,
|
||||
Ident_String => Empty,
|
||||
Is_Predefined_Renaming => False,
|
||||
Is_Internal_Unit => False,
|
||||
Is_Predefined_Unit => False,
|
||||
Filler2 => False,
|
||||
Loading => False,
|
||||
Main_Priority => -1,
|
||||
Main_CPU => -1,
|
||||
Munit_Index => 0,
|
||||
No_Elab_Code_All => False,
|
||||
Serial_Number => 0,
|
||||
Version => 0,
|
||||
Error_Location => No_Location,
|
||||
OA_Setting => 'O');
|
||||
end Add_Preprocessing_Dependency;
|
||||
|
||||
------------------------------
|
||||
@ -130,29 +134,33 @@ package body Lib.Writ is
|
||||
System_Fname := File_Name (System_Source_File_Index);
|
||||
|
||||
Units.Increment_Last;
|
||||
Units.Table (Units.Last) := (
|
||||
Unit_File_Name => System_Fname,
|
||||
Unit_Name => System_Uname,
|
||||
Expected_Unit => System_Uname,
|
||||
Source_Index => System_Source_File_Index,
|
||||
Cunit => Empty,
|
||||
Cunit_Entity => Empty,
|
||||
Dependency_Num => 0,
|
||||
Dynamic_Elab => False,
|
||||
Fatal_Error => None,
|
||||
Generate_Code => False,
|
||||
Has_RACW => False,
|
||||
Filler => False,
|
||||
Ident_String => Empty,
|
||||
Loading => False,
|
||||
Main_Priority => -1,
|
||||
Main_CPU => -1,
|
||||
Munit_Index => 0,
|
||||
No_Elab_Code_All => False,
|
||||
Serial_Number => 0,
|
||||
Version => 0,
|
||||
Error_Location => No_Location,
|
||||
OA_Setting => 'O');
|
||||
Units.Table (Units.Last) :=
|
||||
(Unit_File_Name => System_Fname,
|
||||
Unit_Name => System_Uname,
|
||||
Expected_Unit => System_Uname,
|
||||
Source_Index => System_Source_File_Index,
|
||||
Cunit => Empty,
|
||||
Cunit_Entity => Empty,
|
||||
Dependency_Num => 0,
|
||||
Dynamic_Elab => False,
|
||||
Fatal_Error => None,
|
||||
Generate_Code => False,
|
||||
Has_RACW => False,
|
||||
Filler => False,
|
||||
Ident_String => Empty,
|
||||
Is_Predefined_Renaming => False,
|
||||
Is_Internal_Unit => True,
|
||||
Is_Predefined_Unit => True,
|
||||
Filler2 => False,
|
||||
Loading => False,
|
||||
Main_Priority => -1,
|
||||
Main_CPU => -1,
|
||||
Munit_Index => 0,
|
||||
No_Elab_Code_All => False,
|
||||
Serial_Number => 0,
|
||||
Version => 0,
|
||||
Error_Location => No_Location,
|
||||
OA_Setting => 'O');
|
||||
|
||||
-- Parse system.ads so that the checksum is set right. Style checks are
|
||||
-- not applied. The Ekind is set to ensure that this reference is always
|
||||
@ -533,7 +541,7 @@ package body Lib.Writ is
|
||||
Write_Info_Str (" GE");
|
||||
end if;
|
||||
|
||||
if not Is_Internal_File_Name (Unit_File_Name (Unit_Num), True) then
|
||||
if not Is_Internal_Unit (Unit_Num) then
|
||||
case Identifier_Casing (Source_Index (Unit_Num)) is
|
||||
when All_Lower_Case => Write_Info_Str (" IL");
|
||||
when All_Upper_Case => Write_Info_Str (" IU");
|
||||
@ -618,8 +626,7 @@ package body Lib.Writ is
|
||||
-- parameters (see Lib_Writ spec for an explanation).
|
||||
|
||||
if Is_Generic_Unit (Cunit_Entity (Main_Unit))
|
||||
and then
|
||||
Is_Predefined_File_Name (Unit_File_Name (Current_Sem_Unit))
|
||||
and then Is_Predefined_Unit (Current_Sem_Unit)
|
||||
and then Linker_Option_Lines.Table (J).Unit = Unit_Num
|
||||
then
|
||||
Set_Standard_Error;
|
||||
@ -858,7 +865,7 @@ package body Lib.Writ is
|
||||
if not ((Nkind (Unit (Cunit)) in N_Generic_Declaration
|
||||
or else
|
||||
Nkind (Unit (Cunit)) in N_Generic_Renaming_Declaration)
|
||||
and then Generic_May_Lack_ALI (Fname))
|
||||
and then Generic_May_Lack_ALI (Unum))
|
||||
|
||||
-- In SPARK mode, always generate the dependencies on ALI
|
||||
-- files, which are required to compute frame conditions
|
||||
@ -1160,9 +1167,7 @@ package body Lib.Writ is
|
||||
Write_Info_Str (" DB");
|
||||
end if;
|
||||
|
||||
if Tasking_Used
|
||||
and then not Is_Predefined_File_Name (Unit_File_Name (Main_Unit))
|
||||
then
|
||||
if Tasking_Used and then not Is_Predefined_Unit (Main_Unit) then
|
||||
if Locking_Policy /= ' ' then
|
||||
Write_Info_Str (" L");
|
||||
Write_Info_Char (Locking_Policy);
|
||||
|
@ -36,7 +36,6 @@ pragma Style_Checks (All_Checks);
|
||||
with Atree; use Atree;
|
||||
with Csets; use Csets;
|
||||
with Einfo; use Einfo;
|
||||
with Fname; use Fname;
|
||||
with Nlists; use Nlists;
|
||||
with Opt; use Opt;
|
||||
with Output; use Output;
|
||||
@ -127,6 +126,21 @@ package body Lib is
|
||||
return Units.Table (U).Has_RACW;
|
||||
end Has_RACW;
|
||||
|
||||
function Is_Predefined_Renaming (U : Unit_Number_Type) return Boolean is
|
||||
begin
|
||||
return Units.Table (U).Is_Predefined_Renaming;
|
||||
end Is_Predefined_Renaming;
|
||||
|
||||
function Is_Internal_Unit (U : Unit_Number_Type) return Boolean is
|
||||
begin
|
||||
return Units.Table (U).Is_Internal_Unit;
|
||||
end Is_Internal_Unit;
|
||||
|
||||
function Is_Predefined_Unit (U : Unit_Number_Type) return Boolean is
|
||||
begin
|
||||
return Units.Table (U).Is_Predefined_Unit;
|
||||
end Is_Predefined_Unit;
|
||||
|
||||
function Ident_String (U : Unit_Number_Type) return Node_Id is
|
||||
begin
|
||||
return Units.Table (U).Ident_String;
|
||||
@ -576,7 +590,7 @@ package body Lib is
|
||||
-- Generic_May_Lack_ALI --
|
||||
--------------------------
|
||||
|
||||
function Generic_May_Lack_ALI (Sfile : File_Name_Type) return Boolean is
|
||||
function Generic_May_Lack_ALI (Unum : Unit_Number_Type) return Boolean is
|
||||
begin
|
||||
-- We allow internal generic units to be used without having a
|
||||
-- corresponding ALI files to help bootstrapping with older compilers
|
||||
@ -585,9 +599,7 @@ package body Lib is
|
||||
-- is the elaboration boolean, and we are careful to elaborate all
|
||||
-- predefined units first anyway.
|
||||
|
||||
return Is_Internal_File_Name
|
||||
(Fname => Sfile,
|
||||
Renamings_Included => True);
|
||||
return Is_Internal_Unit (Unum);
|
||||
end Generic_May_Lack_ALI;
|
||||
|
||||
-----------------------------
|
||||
@ -904,12 +916,25 @@ package body Lib is
|
||||
|
||||
function In_Internal_Unit (S : Source_Ptr) return Boolean is
|
||||
Unit : constant Unit_Number_Type := Get_Source_Unit (S);
|
||||
File : constant File_Name_Type := Unit_File_Name (Unit);
|
||||
|
||||
begin
|
||||
return Is_Internal_File_Name (File);
|
||||
return Is_Internal_Unit (Unit);
|
||||
end In_Internal_Unit;
|
||||
|
||||
----------------------------
|
||||
-- In_Predefined_Renaming --
|
||||
----------------------------
|
||||
|
||||
function In_Predefined_Renaming (N : Node_Or_Entity_Id) return Boolean is
|
||||
begin
|
||||
return In_Predefined_Renaming (Sloc (N));
|
||||
end In_Predefined_Renaming;
|
||||
|
||||
function In_Predefined_Renaming (S : Source_Ptr) return Boolean is
|
||||
Unit : constant Unit_Number_Type := Get_Source_Unit (S);
|
||||
begin
|
||||
return Is_Predefined_Renaming (Unit);
|
||||
end In_Predefined_Renaming;
|
||||
|
||||
------------------------
|
||||
-- In_Predefined_Unit --
|
||||
------------------------
|
||||
@ -921,9 +946,8 @@ package body Lib is
|
||||
|
||||
function In_Predefined_Unit (S : Source_Ptr) return Boolean is
|
||||
Unit : constant Unit_Number_Type := Get_Source_Unit (S);
|
||||
File : constant File_Name_Type := Unit_File_Name (Unit);
|
||||
begin
|
||||
return Is_Predefined_File_Name (File);
|
||||
return Is_Predefined_Unit (Unit);
|
||||
end In_Predefined_Unit;
|
||||
|
||||
-----------------------
|
||||
|
@ -327,6 +327,19 @@ package Lib is
|
||||
-- N_String_Literal node from a valid pragma Ident that applies to
|
||||
-- this unit. If no Ident pragma applies to the unit, then Empty.
|
||||
|
||||
-- Is_Predefined_Renaming
|
||||
-- True if this unit is a predefined renaming, as in "Text_IO renames
|
||||
-- Ada.Text_IO").
|
||||
|
||||
-- Is_Internal_Unit
|
||||
-- Same as In_Predefined_Unit, except units in the GNAT hierarchy are
|
||||
-- included.
|
||||
|
||||
-- Is_Predefined_Unit
|
||||
-- True if this unit is predefined (i.e. part of the Ada, System, or
|
||||
-- Interface hierarchies, or Is_Predefined_Renaming). Note that units
|
||||
-- in the GNAT hierarchy are not considered predefined.
|
||||
|
||||
-- Loading
|
||||
-- A flag that is used to catch circular WITH dependencies. It is set
|
||||
-- True when an entry is initially created in the file table, and set
|
||||
@ -428,6 +441,9 @@ package Lib is
|
||||
function Generate_Code (U : Unit_Number_Type) return Boolean;
|
||||
function Ident_String (U : Unit_Number_Type) return Node_Id;
|
||||
function Has_RACW (U : Unit_Number_Type) return Boolean;
|
||||
function Is_Predefined_Renaming (U : Unit_Number_Type) return Boolean;
|
||||
function Is_Internal_Unit (U : Unit_Number_Type) return Boolean;
|
||||
function Is_Predefined_Unit (U : Unit_Number_Type) return Boolean;
|
||||
function Loading (U : Unit_Number_Type) return Boolean;
|
||||
function Main_CPU (U : Unit_Number_Type) return Int;
|
||||
function Main_Priority (U : Unit_Number_Type) return Int;
|
||||
@ -493,7 +509,7 @@ package Lib is
|
||||
-- Return the Nth stored compilation switch, or null if less than N
|
||||
-- switches have been stored. Used by ASIS and back ends written in Ada.
|
||||
|
||||
function Generic_May_Lack_ALI (Sfile : File_Name_Type) return Boolean;
|
||||
function Generic_May_Lack_ALI (Unum : Unit_Number_Type) return Boolean;
|
||||
-- Generic units must be separately compiled. Since we always use
|
||||
-- macro substitution for generics, the resulting object file is a dummy
|
||||
-- one with no code, but the ALI file has the normal form, and we need
|
||||
@ -597,13 +613,20 @@ package Lib is
|
||||
-- of the descendant packages of one of these three packages).
|
||||
|
||||
function In_Predefined_Unit (S : Source_Ptr) return Boolean;
|
||||
pragma Inline (In_Predefined_Unit);
|
||||
-- Same function as above but argument is a source pointer
|
||||
|
||||
function In_Internal_Unit (N : Node_Or_Entity_Id) return Boolean;
|
||||
function In_Internal_Unit (S : Source_Ptr) return Boolean;
|
||||
pragma Inline (In_Internal_Unit);
|
||||
-- Same as In_Predefined_Unit, except units in the GNAT hierarchy are
|
||||
-- included.
|
||||
|
||||
function In_Predefined_Renaming (N : Node_Or_Entity_Id) return Boolean;
|
||||
function In_Predefined_Renaming (S : Source_Ptr) return Boolean;
|
||||
pragma Inline (In_Predefined_Renaming);
|
||||
-- Returns True if N or S is in a predefined renaming unit
|
||||
|
||||
function In_Same_Code_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean;
|
||||
pragma Inline (In_Same_Code_Unit);
|
||||
-- Determines if the two nodes or entities N1 and N2 are in the same
|
||||
@ -776,6 +799,9 @@ private
|
||||
pragma Inline (Set_Fatal_Error);
|
||||
pragma Inline (Set_Generate_Code);
|
||||
pragma Inline (Set_Has_RACW);
|
||||
pragma Inline (Is_Predefined_Renaming);
|
||||
pragma Inline (Is_Internal_Unit);
|
||||
pragma Inline (Is_Predefined_Unit);
|
||||
pragma Inline (Set_Loading);
|
||||
pragma Inline (Set_Main_CPU);
|
||||
pragma Inline (Set_Main_Priority);
|
||||
@ -811,6 +837,11 @@ private
|
||||
Filler : Boolean;
|
||||
Loading : Boolean;
|
||||
OA_Setting : Character;
|
||||
|
||||
Is_Predefined_Renaming : Boolean;
|
||||
Is_Internal_Unit : Boolean;
|
||||
Is_Predefined_Unit : Boolean;
|
||||
Filler2 : Boolean;
|
||||
end record;
|
||||
|
||||
-- The following representation clause ensures that the above record
|
||||
@ -840,9 +871,14 @@ private
|
||||
Filler at 61 range 0 .. 7;
|
||||
OA_Setting at 62 range 0 .. 7;
|
||||
Loading at 63 range 0 .. 7;
|
||||
|
||||
Is_Predefined_Renaming at 64 range 0 .. 7;
|
||||
Is_Internal_Unit at 65 range 0 .. 7;
|
||||
Is_Predefined_Unit at 66 range 0 .. 7;
|
||||
Filler2 at 67 range 0 .. 7;
|
||||
end record;
|
||||
|
||||
for Unit_Record'Size use 64 * 8;
|
||||
for Unit_Record'Size use 68 * 8;
|
||||
-- This ensures that we did not leave out any fields
|
||||
|
||||
package Units is new Table.Table (
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNAT is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
@ -1526,8 +1526,8 @@ begin
|
||||
|
||||
for Ucount in Pos loop
|
||||
Set_Opt_Config_Switches
|
||||
(Is_Internal_File_Name (File_Name (Current_Source_File)),
|
||||
Current_Source_Unit = Main_Unit);
|
||||
(Is_Internal_Unit (Current_Source_Unit),
|
||||
Main_Unit => Current_Source_Unit = Main_Unit);
|
||||
|
||||
-- Initialize scope table and other parser control variables
|
||||
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNAT is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
@ -1763,7 +1763,7 @@ package body Restrict is
|
||||
-- Otherwise suppress message if internal file
|
||||
|
||||
else
|
||||
return Is_Internal_File_Name (Unit_File_Name (Get_Source_Unit (N)));
|
||||
return In_Internal_Unit (N);
|
||||
end if;
|
||||
end Suppress_Restriction_Message;
|
||||
|
||||
|
@ -469,9 +469,7 @@ package body Rtsfind is
|
||||
-- unit for inlining purposes, the body must be illegal in this
|
||||
-- mode, and there is no point in continuing.
|
||||
|
||||
if Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Sloc (Current_Error_Node))))
|
||||
then
|
||||
if In_Predefined_Unit (Current_Error_Node) then
|
||||
Error_Msg_N
|
||||
("construct not allowed in no run time mode!",
|
||||
Current_Error_Node);
|
||||
@ -1626,7 +1624,7 @@ package body Rtsfind is
|
||||
E : constant Entity_Id :=
|
||||
Defining_Entity (Unit (Cunit (Unum)));
|
||||
begin
|
||||
pragma Assert (Is_Predefined_File_Name (Unit_File_Name (Unum)));
|
||||
pragma Assert (Is_Predefined_Unit (Unum));
|
||||
|
||||
-- Loop through entries in RTU table looking for matching entry
|
||||
|
||||
|
@ -29,7 +29,6 @@ with Debug_A; use Debug_A;
|
||||
with Elists; use Elists;
|
||||
with Exp_SPARK; use Exp_SPARK;
|
||||
with Expander; use Expander;
|
||||
with Fname; use Fname;
|
||||
with Ghost; use Ghost;
|
||||
with Lib; use Lib;
|
||||
with Lib.Load; use Lib.Load;
|
||||
@ -1425,8 +1424,8 @@ package body Sem is
|
||||
-- Sequential_IO) as this would prevent pragma Extend_System from being
|
||||
-- taken into account, for example when Text_IO is renaming DEC.Text_IO.
|
||||
|
||||
if Is_Predefined_File_Name
|
||||
(Unit_File_Name (Current_Sem_Unit), Renamings_Included => False)
|
||||
if Is_Predefined_Unit (Current_Sem_Unit)
|
||||
and then not Is_Predefined_Renaming (Current_Sem_Unit)
|
||||
then
|
||||
GNAT_Mode := True;
|
||||
end if;
|
||||
@ -1474,7 +1473,7 @@ package body Sem is
|
||||
|
||||
Save_Opt_Config_Switches (Save_Config_Switches);
|
||||
Set_Opt_Config_Switches
|
||||
(Is_Internal_File_Name (Unit_File_Name (Current_Sem_Unit)),
|
||||
(Is_Internal_Unit (Current_Sem_Unit),
|
||||
Is_Main_Unit_Or_Main_Unit_Spec);
|
||||
|
||||
-- Save current non-partition-wide restrictions
|
||||
|
@ -29,7 +29,6 @@ with Einfo; use Einfo;
|
||||
with Elists; use Elists;
|
||||
with Errout; use Errout;
|
||||
with Exp_Disp; use Exp_Disp;
|
||||
with Fname; use Fname;
|
||||
with Lib; use Lib;
|
||||
with Namet; use Namet;
|
||||
with Nlists; use Nlists;
|
||||
@ -263,8 +262,8 @@ package body Sem_Cat is
|
||||
-- so it is convenient not to generate them (since it causes
|
||||
-- annoying interference with debugging).
|
||||
|
||||
if Is_Internal_File_Name (Unit_File_Name (Current_Sem_Unit))
|
||||
and then not Is_Internal_File_Name (Unit_File_Name (Main_Unit))
|
||||
if Is_Internal_Unit (Current_Sem_Unit)
|
||||
and then not Is_Internal_Unit (Main_Unit)
|
||||
then
|
||||
return;
|
||||
|
||||
@ -949,8 +948,7 @@ package body Sem_Cat is
|
||||
|
||||
if Is_Private_Type (T)
|
||||
and then not Has_Pragma_Preelab_Init (T)
|
||||
and then not Is_Internal_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (N)))
|
||||
and then not In_Internal_Unit (N)
|
||||
then
|
||||
Error_Msg_N
|
||||
("private ancestor type not allowed in preelaborated unit", A);
|
||||
@ -1098,8 +1096,7 @@ package body Sem_Cat is
|
||||
if In_Preelaborated_Unit
|
||||
and then not Debug_Flag_PP
|
||||
and then Comes_From_Source (E)
|
||||
and then not
|
||||
Is_Internal_File_Name (Unit_File_Name (Get_Source_Unit (E)))
|
||||
and then not In_Internal_Unit (E)
|
||||
and then (not Inside_A_Generic
|
||||
or else Present (Enclosing_Generic_Body (E)))
|
||||
and then not Is_Protected_Type (Etype (E))
|
||||
@ -2202,7 +2199,7 @@ package body Sem_Cat is
|
||||
E := Entity (N);
|
||||
Val := Constant_Value (E);
|
||||
|
||||
if Is_Internal_File_Name (Unit_File_Name (Get_Source_Unit (N)))
|
||||
if In_Internal_Unit (N)
|
||||
and then
|
||||
Enclosing_Comp_Unit_Node (N) /= Enclosing_Comp_Unit_Node (E)
|
||||
and then (Is_Preelaborated (Scope (E))
|
||||
|
@ -648,9 +648,7 @@ package body Sem_Ch10 is
|
||||
Circularity : Boolean := True;
|
||||
|
||||
begin
|
||||
if Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Unit (N))))
|
||||
then
|
||||
if In_Predefined_Unit (N) then
|
||||
Circularity := False;
|
||||
|
||||
else
|
||||
@ -919,13 +917,9 @@ package body Sem_Ch10 is
|
||||
|
||||
-- Register predefined units in Rtsfind
|
||||
|
||||
declare
|
||||
Unum : constant Unit_Number_Type := Get_Source_Unit (Sloc (N));
|
||||
begin
|
||||
if Is_Predefined_File_Name (Unit_File_Name (Unum)) then
|
||||
Set_RTU_Loaded (Unit_Node);
|
||||
end if;
|
||||
end;
|
||||
if In_Predefined_Unit (N) then
|
||||
Set_RTU_Loaded (Unit_Node);
|
||||
end if;
|
||||
|
||||
-- Treat compilation unit pragmas that appear after the library unit
|
||||
|
||||
@ -1230,7 +1224,7 @@ package body Sem_Ch10 is
|
||||
|
||||
-- No checks needed for predefined files
|
||||
|
||||
or else Is_Predefined_File_Name (Unit_File_Name (Unum))
|
||||
or else Is_Predefined_Unit (Unum)
|
||||
|
||||
-- No checks required if no separate spec
|
||||
|
||||
@ -2524,18 +2518,10 @@ package body Sem_Ch10 is
|
||||
-- himself, but that's a marginal case, and fixing it is hard ???
|
||||
|
||||
if Restriction_Check_Required (No_Obsolescent_Features) then
|
||||
declare
|
||||
F : constant File_Name_Type :=
|
||||
Unit_File_Name (Get_Source_Unit (U));
|
||||
begin
|
||||
if Is_Predefined_File_Name (F, Renamings_Included => True)
|
||||
and then not
|
||||
Is_Predefined_File_Name (F, Renamings_Included => False)
|
||||
then
|
||||
Check_Restriction (No_Obsolescent_Features, N);
|
||||
Restriction_Violation := True;
|
||||
end if;
|
||||
end;
|
||||
if In_Predefined_Renaming (U) then
|
||||
Check_Restriction (No_Obsolescent_Features, N);
|
||||
Restriction_Violation := True;
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Check No_Implementation_Units violation
|
||||
@ -2566,7 +2552,7 @@ package body Sem_Ch10 is
|
||||
-- clauses into regular with clauses.
|
||||
|
||||
if Sloc (U) /= No_Location then
|
||||
if Is_Predefined_File_Name (Unit_File_Name (Get_Source_Unit (U)))
|
||||
if In_Predefined_Unit (U)
|
||||
|
||||
-- In ASIS mode the rtsfind mechanism plays no role, and
|
||||
-- we need to maintain the original tree structure, so
|
||||
@ -2598,7 +2584,7 @@ package body Sem_Ch10 is
|
||||
|
||||
Semantics (Library_Unit (N));
|
||||
|
||||
Intunit := Is_Internal_File_Name (Unit_File_Name (Current_Sem_Unit));
|
||||
Intunit := Is_Internal_Unit (Current_Sem_Unit);
|
||||
|
||||
if Sloc (U) /= No_Location then
|
||||
|
||||
@ -3537,7 +3523,7 @@ package body Sem_Ch10 is
|
||||
-- Exclude license check if withed unit is an internal unit.
|
||||
-- This situation arises e.g. with the GPL version of GNAT.
|
||||
|
||||
if Is_Internal_File_Name (Unit_File_Name (Withu)) then
|
||||
if Is_Internal_Unit (Withu) then
|
||||
null;
|
||||
|
||||
-- Otherwise check various cases
|
||||
@ -5276,7 +5262,7 @@ package body Sem_Ch10 is
|
||||
-- skipped for dummy units (for missing packages).
|
||||
|
||||
if Sloc (Uname) /= No_Location
|
||||
and then (not Is_Internal_File_Name (Unit_File_Name (Current_Sem_Unit))
|
||||
and then (not Is_Internal_Unit (Current_Sem_Unit)
|
||||
or else Current_Sem_Unit = Main_Unit)
|
||||
then
|
||||
Check_Restricted_Unit
|
||||
|
@ -4109,8 +4109,7 @@ package body Sem_Ch12 is
|
||||
-- predefined subprograms marked Inline_Always, to minimize
|
||||
-- the use of the run-time library.
|
||||
|
||||
elsif Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Gen_Decl)))
|
||||
elsif In_Predefined_Unit (Gen_Decl)
|
||||
and then Configurable_Run_Time_Mode
|
||||
and then Nkind (Parent (N)) /= N_Compilation_Unit
|
||||
then
|
||||
@ -11210,8 +11209,7 @@ package body Sem_Ch12 is
|
||||
-- interested in finding possible runtime errors.
|
||||
|
||||
if not CodePeer_Mode
|
||||
and then Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Gen_Decl)))
|
||||
and then In_Predefined_Unit (Gen_Decl)
|
||||
then
|
||||
Analyze (Act_Body, Suppress => All_Checks);
|
||||
else
|
||||
@ -15473,10 +15471,7 @@ package body Sem_Ch12 is
|
||||
-- to predefined units. Nothing needs to be done for non-internal units.
|
||||
-- These are always analyzed in the current mode.
|
||||
|
||||
if Is_Internal_File_Name
|
||||
(Fname => Unit_File_Name (Get_Source_Unit (Gen_Unit)),
|
||||
Renamings_Included => True)
|
||||
then
|
||||
if In_Internal_Unit (Gen_Unit) then
|
||||
Set_Opt_Config_Switches (True, Current_Sem_Unit = Main_Unit);
|
||||
|
||||
-- In Ada2012 we may want to enable assertions in an instance of a
|
||||
|
@ -38,7 +38,6 @@ with Exp_Disp; use Exp_Disp;
|
||||
with Exp_Dist; use Exp_Dist;
|
||||
with Exp_Tss; use Exp_Tss;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Fname; use Fname;
|
||||
with Freeze; use Freeze;
|
||||
with Ghost; use Ghost;
|
||||
with Itypes; use Itypes;
|
||||
@ -3266,7 +3265,7 @@ package body Sem_Ch3 is
|
||||
|
||||
if Chars (Scope (Def_Id)) = Name_System
|
||||
and then Chars (Def_Id) = Name_Address
|
||||
and then Is_Predefined_File_Name (Unit_File_Name (Get_Source_Unit (N)))
|
||||
and then In_Predefined_Unit (N)
|
||||
then
|
||||
Set_Is_Descendant_Of_Address (Def_Id);
|
||||
Set_Is_Descendant_Of_Address (Base_Type (Def_Id));
|
||||
|
@ -30,7 +30,6 @@ with Einfo; use Einfo;
|
||||
with Elists; use Elists;
|
||||
with Errout; use Errout;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Fname; use Fname;
|
||||
with Itypes; use Itypes;
|
||||
with Lib; use Lib;
|
||||
with Lib.Xref; use Lib.Xref;
|
||||
@ -3483,9 +3482,7 @@ package body Sem_Ch4 is
|
||||
and then
|
||||
(Etype (Actual) /= Universal_Integer
|
||||
or else not Is_Descendant_Of_Address (Etype (Formal))
|
||||
or else
|
||||
Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (N))))
|
||||
or else In_Predefined_Unit (N))
|
||||
then
|
||||
Next_Actual (Actual);
|
||||
Next_Formal (Formal);
|
||||
@ -7351,8 +7348,7 @@ package body Sem_Ch4 is
|
||||
-- variants of System, and it must be removed as well.
|
||||
|
||||
elsif Ada_Version >= Ada_2005
|
||||
or else Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (It.Nam)))
|
||||
or else In_Predefined_Unit (It.Nam)
|
||||
then
|
||||
Remove_Interp (I);
|
||||
exit;
|
||||
|
@ -39,7 +39,6 @@ with Exp_Dbug; use Exp_Dbug;
|
||||
with Exp_Disp; use Exp_Disp;
|
||||
with Exp_Tss; use Exp_Tss;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Fname; use Fname;
|
||||
with Freeze; use Freeze;
|
||||
with Ghost; use Ghost;
|
||||
with Inline; use Inline;
|
||||
@ -3308,8 +3307,7 @@ package body Sem_Ch6 is
|
||||
|
||||
elsif Style_Check
|
||||
and then Can_Override_Operator (Spec_Id)
|
||||
and then not Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Spec_Id)))
|
||||
and then not In_Predefined_Unit (Spec_Id)
|
||||
then
|
||||
pragma Assert (Unit_Declaration_Node (Body_Id) = N);
|
||||
Style.Missing_Overriding (N, Body_Id);
|
||||
@ -6156,9 +6154,7 @@ package body Sem_Ch6 is
|
||||
and then Chars (Overridden_Subp) = Name_Adjust
|
||||
and then Is_Limited_Type (Etype (First_Formal (Subp)))
|
||||
and then Present (Alias (Overridden_Subp))
|
||||
and then
|
||||
Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Alias (Overridden_Subp))))
|
||||
and then In_Predefined_Unit (Alias (Overridden_Subp))
|
||||
then
|
||||
Get_Name_String
|
||||
(Unit_File_Name (Get_Source_Unit (Alias (Overridden_Subp))));
|
||||
@ -6243,9 +6239,7 @@ package body Sem_Ch6 is
|
||||
elsif not Error_Posted (Subp)
|
||||
and then Style_Check
|
||||
and then Can_Override_Operator (Subp)
|
||||
and then
|
||||
not Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Subp)))
|
||||
and then not In_Predefined_Unit (Subp)
|
||||
then
|
||||
-- If style checks are enabled, indicate that the indicator is
|
||||
-- missing. However, at the point of declaration, the type of
|
||||
|
@ -31,7 +31,6 @@ with Errout; use Errout;
|
||||
with Exp_Disp; use Exp_Disp;
|
||||
with Exp_Tss; use Exp_Tss;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Fname; use Fname;
|
||||
with Freeze; use Freeze;
|
||||
with Ghost; use Ghost;
|
||||
with Impunit; use Impunit;
|
||||
@ -3644,7 +3643,7 @@ package body Sem_Ch8 is
|
||||
-- except that packages whose file name starts a-n are OK (these are
|
||||
-- children of Ada.Numerics, which are never loaded by Rtsfind).
|
||||
|
||||
if Is_Predefined_File_Name (Unit_File_Name (Current_Sem_Unit))
|
||||
if Is_Predefined_Unit (Current_Sem_Unit)
|
||||
and then Get_Name_String
|
||||
(Unit_File_Name (Current_Sem_Unit)) (1 .. 3) /= "a-n"
|
||||
and then Nkind (Unit (Cunit (Current_Sem_Unit))) =
|
||||
@ -4968,7 +4967,7 @@ package body Sem_Ch8 is
|
||||
|
||||
-- Case of from internal file
|
||||
|
||||
if Is_Internal_File_Name (Fname) then
|
||||
if In_Internal_Unit (E) then
|
||||
|
||||
-- Private part entities in internal files are never considered
|
||||
-- to be known to the writer of normal application code.
|
||||
@ -5551,17 +5550,14 @@ package body Sem_Ch8 is
|
||||
Nvis_Messages;
|
||||
goto Done;
|
||||
|
||||
elsif Is_Predefined_File_Name (Unit_File_Name (Current_Sem_Unit))
|
||||
then
|
||||
elsif Is_Predefined_Unit (Current_Sem_Unit) then
|
||||
-- A use-clause in the body of a system file creates conflict
|
||||
-- with some entity in a user scope, while rtsfind is active.
|
||||
-- Keep only the entity coming from another predefined unit.
|
||||
|
||||
E2 := E;
|
||||
while Present (E2) loop
|
||||
if Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Sloc (E2))))
|
||||
then
|
||||
if In_Predefined_Unit (E2) then
|
||||
E := E2;
|
||||
goto Found;
|
||||
end if;
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNAT is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
@ -32,7 +32,6 @@ with Einfo; use Einfo;
|
||||
with Errout; use Errout;
|
||||
with Exp_Ch9; use Exp_Ch9;
|
||||
with Elists; use Elists;
|
||||
with Fname; use Fname;
|
||||
with Freeze; use Freeze;
|
||||
with Layout; use Layout;
|
||||
with Lib; use Lib;
|
||||
@ -2024,7 +2023,7 @@ package body Sem_Ch9 is
|
||||
-- implemented.
|
||||
|
||||
if In_Private_Part (Current_Scope)
|
||||
and then Is_Internal_File_Name (Unit_File_Name (Current_Sem_Unit))
|
||||
and then Is_Internal_Unit (Current_Sem_Unit)
|
||||
then
|
||||
Set_Has_Protected (T, False);
|
||||
else
|
||||
|
@ -32,7 +32,6 @@ with Errout; use Errout;
|
||||
with Exp_Tss; use Exp_Tss;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Expander; use Expander;
|
||||
with Fname; use Fname;
|
||||
with Lib; use Lib;
|
||||
with Lib.Load; use Lib.Load;
|
||||
with Namet; use Namet;
|
||||
@ -910,8 +909,7 @@ package body Sem_Elab is
|
||||
|
||||
-- Check cases of internal units
|
||||
|
||||
Callee_Unit_Internal :=
|
||||
Is_Internal_File_Name (Unit_File_Name (Get_Source_Unit (E_Scope)));
|
||||
Callee_Unit_Internal := In_Internal_Unit (E_Scope);
|
||||
|
||||
-- Do not give a warning if the with'ed unit is internal and this is
|
||||
-- the generic instantiation case (this saves a lot of hassle dealing
|
||||
@ -924,8 +922,7 @@ package body Sem_Elab is
|
||||
if C_Scope = Standard_Standard then
|
||||
Caller_Unit_Internal := False;
|
||||
else
|
||||
Caller_Unit_Internal :=
|
||||
Is_Internal_File_Name (Unit_File_Name (Get_Source_Unit (C_Scope)));
|
||||
Caller_Unit_Internal := In_Internal_Unit (C_Scope);
|
||||
end if;
|
||||
|
||||
-- Do not give a warning if the with'ed unit is internal and the caller
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNAT is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
@ -28,7 +28,6 @@
|
||||
with Atree; use Atree;
|
||||
with Einfo; use Einfo;
|
||||
with Errout; use Errout;
|
||||
with Fname; use Fname;
|
||||
with Lib; use Lib;
|
||||
with Namet; use Namet;
|
||||
with Opt; use Opt;
|
||||
@ -339,8 +338,7 @@ package body Sem_Intr is
|
||||
|
||||
elsif not Comes_From_Source (E)
|
||||
or else not Comes_From_Source (N)
|
||||
or else Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (N)))
|
||||
or else In_Predefined_Unit (N)
|
||||
then
|
||||
null;
|
||||
|
||||
|
@ -35,7 +35,6 @@ with Exp_Ch6; use Exp_Ch6;
|
||||
with Exp_Ch7; use Exp_Ch7;
|
||||
with Exp_Tss; use Exp_Tss;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Fname; use Fname;
|
||||
with Freeze; use Freeze;
|
||||
with Ghost; use Ghost;
|
||||
with Inline; use Inline;
|
||||
@ -1895,9 +1894,7 @@ package body Sem_Res is
|
||||
function Comes_From_Predefined_Lib_Unit (Nod : Node_Id) return Boolean is
|
||||
begin
|
||||
return
|
||||
Sloc (Nod) = Standard_Location
|
||||
or else Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Sloc (Nod))));
|
||||
Sloc (Nod) = Standard_Location or else In_Predefined_Unit (Nod);
|
||||
end Comes_From_Predefined_Lib_Unit;
|
||||
|
||||
--------------------
|
||||
|
@ -13482,9 +13482,7 @@ package body Sem_Util is
|
||||
begin
|
||||
if Present (Init)
|
||||
and then Comes_From_Source (Init)
|
||||
and then not
|
||||
Is_Predefined_File_Name
|
||||
(File_Name (Get_Source_File_Index (Sloc (Init))))
|
||||
and then not In_Predefined_Unit (Init)
|
||||
then
|
||||
return True;
|
||||
|
||||
@ -13771,8 +13769,7 @@ package body Sem_Util is
|
||||
return
|
||||
Nam_In (Chars (Iter_Typ), Name_Forward_Iterator,
|
||||
Name_Reversible_Iterator)
|
||||
and then Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Root_Type (Iter_Typ))));
|
||||
and then In_Predefined_Unit (Root_Type (Iter_Typ));
|
||||
end Denotes_Iterator;
|
||||
|
||||
-- Local variables
|
||||
@ -15069,8 +15066,7 @@ package body Sem_Util is
|
||||
begin
|
||||
if Is_Class_Wide_Type (Typ)
|
||||
and then Chars (Root_Type (Typ)) = Name_Reversible_Iterator
|
||||
and then Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Root_Type (Typ))))
|
||||
and then In_Predefined_Unit (Root_Type (Typ))
|
||||
then
|
||||
return True;
|
||||
|
||||
@ -15084,9 +15080,7 @@ package body Sem_Util is
|
||||
while Present (Iface_Elmt) loop
|
||||
Iface := Node (Iface_Elmt);
|
||||
if Chars (Iface) = Name_Reversible_Iterator
|
||||
and then
|
||||
Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Iface)))
|
||||
and then In_Predefined_Unit (Iface)
|
||||
then
|
||||
return True;
|
||||
end if;
|
||||
@ -15597,8 +15591,7 @@ package body Sem_Util is
|
||||
return
|
||||
Chars (Par) = Name_Unchecked_Conversion
|
||||
and then Is_Intrinsic_Subprogram (Par)
|
||||
and then Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Par)));
|
||||
and then In_Predefined_Unit (Par);
|
||||
else
|
||||
return
|
||||
Present (Alias (Id))
|
||||
@ -20982,10 +20975,7 @@ package body Sem_Util is
|
||||
then
|
||||
return;
|
||||
|
||||
elsif In_Inlined_Body
|
||||
and then Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Sloc (T))))
|
||||
then
|
||||
elsif In_Inlined_Body and then In_Predefined_Unit (T) then
|
||||
Set_Needs_Debug_Info (T, False);
|
||||
end if;
|
||||
|
||||
|
@ -28,7 +28,6 @@ with Debug; use Debug;
|
||||
with Einfo; use Einfo;
|
||||
with Errout; use Errout;
|
||||
with Exp_Code; use Exp_Code;
|
||||
with Fname; use Fname;
|
||||
with Lib; use Lib;
|
||||
with Lib.Xref; use Lib.Xref;
|
||||
with Namet; use Namet;
|
||||
@ -1612,10 +1611,7 @@ package body Sem_Warn is
|
||||
-- (these would be junk warnings for an applications program,
|
||||
-- since they refer to problems in internal units).
|
||||
|
||||
if GNAT_Mode
|
||||
or else not Is_Internal_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (E1)))
|
||||
then
|
||||
if GNAT_Mode or else not In_Internal_Unit (E1) then
|
||||
-- We do not immediately flag the error. This is because we
|
||||
-- have not expanded generic bodies yet, and they may have
|
||||
-- the missing reference. So instead we park the entity on a
|
||||
@ -2383,7 +2379,7 @@ package body Sem_Warn is
|
||||
-- clearly undesirable.
|
||||
|
||||
elsif Configurable_Run_Time_Mode
|
||||
and then Is_Predefined_File_Name (Unit_File_Name (Unit))
|
||||
and then Is_Predefined_Unit (Unit)
|
||||
then
|
||||
return;
|
||||
end if;
|
||||
@ -2414,9 +2410,7 @@ package body Sem_Warn is
|
||||
-- (these would be junk warnings for an application program,
|
||||
-- since they refer to problems in internal units).
|
||||
|
||||
if GNAT_Mode
|
||||
or else not Is_Internal_File_Name (Unit_File_Name (Unit))
|
||||
then
|
||||
if GNAT_Mode or else not Is_Internal_Unit (Unit) then
|
||||
-- Here we definitely have a non-referenced unit. If it
|
||||
-- is the special call for a spec unit, then just set the
|
||||
-- flag to be read later.
|
||||
@ -3302,8 +3296,7 @@ package body Sem_Warn is
|
||||
-- Do not consider internal files to allow for various assertions and
|
||||
-- safeguards within our runtime.
|
||||
|
||||
and then not Is_Internal_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Op)))
|
||||
and then not In_Internal_Unit (Op)
|
||||
then
|
||||
Test_Comparison
|
||||
(Op => Op,
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNAT is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
@ -29,7 +29,6 @@ with Casing; use Casing;
|
||||
with Csets; use Csets;
|
||||
with Debug; use Debug;
|
||||
with Einfo; use Einfo;
|
||||
with Fname; use Fname;
|
||||
with Lib; use Lib;
|
||||
with Namet; use Namet;
|
||||
with Nlists; use Nlists;
|
||||
@ -4806,9 +4805,7 @@ package body Sprint is
|
||||
Ent : constant Entity_Id := Entity (N);
|
||||
begin
|
||||
if not In_Extended_Main_Source_Unit (Ent)
|
||||
and then
|
||||
Is_Predefined_File_Name
|
||||
(Unit_File_Name (Get_Source_Unit (Ent)))
|
||||
and then In_Predefined_Unit (Ent)
|
||||
then
|
||||
-- Run-time routine name, output name with a preceding dollar
|
||||
-- making sure that we do not get a line split between them.
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1999-2016, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1999-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- --
|
||||
@ -75,6 +75,7 @@ package body Warnsw is
|
||||
Warn_On_Overlap := Setting;
|
||||
Warn_On_Overridden_Size := Setting;
|
||||
Warn_On_Parameter_Order := Setting;
|
||||
Warn_On_Questionable_Layout := Setting;
|
||||
Warn_On_Questionable_Missing_Parens := Setting;
|
||||
Warn_On_Record_Holes := Setting;
|
||||
Warn_On_Redundant_Constructs := Setting;
|
||||
@ -166,6 +167,8 @@ package body Warnsw is
|
||||
W.Warn_On_Overridden_Size;
|
||||
Warn_On_Parameter_Order :=
|
||||
W.Warn_On_Parameter_Order;
|
||||
Warn_On_Questionable_Layout :=
|
||||
W.Warn_On_Questionable_Layout;
|
||||
Warn_On_Questionable_Missing_Parens :=
|
||||
W.Warn_On_Questionable_Missing_Parens;
|
||||
Warn_On_Record_Holes :=
|
||||
@ -270,6 +273,8 @@ package body Warnsw is
|
||||
Warn_On_Overridden_Size;
|
||||
W.Warn_On_Parameter_Order :=
|
||||
Warn_On_Parameter_Order;
|
||||
W.Warn_On_Questionable_Layout :=
|
||||
Warn_On_Questionable_Layout;
|
||||
W.Warn_On_Questionable_Missing_Parens :=
|
||||
Warn_On_Questionable_Missing_Parens;
|
||||
W.Warn_On_Record_Holes :=
|
||||
@ -394,6 +399,12 @@ package body Warnsw is
|
||||
when 'P' =>
|
||||
Warn_On_Parameter_Order := False;
|
||||
|
||||
when 'q' =>
|
||||
Warn_On_Questionable_Layout := True;
|
||||
|
||||
when 'Q' =>
|
||||
Warn_On_Questionable_Layout := False;
|
||||
|
||||
when 'r' =>
|
||||
Warn_On_Object_Renames_Function := True;
|
||||
|
||||
|
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- S p e c --
|
||||
-- --
|
||||
-- Copyright (C) 1999-2016, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1999-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- --
|
||||
@ -42,16 +42,21 @@ package Warnsw is
|
||||
-- Warn when tagged type public primitives are defined after its private
|
||||
-- extensions.
|
||||
|
||||
Warn_On_Record_Holes : Boolean := False;
|
||||
-- Warn when explicit record component clauses leave uncovered holes (gaps)
|
||||
-- in a record layout. Off by default, set by -gnatw.h (but not -gnatwa).
|
||||
|
||||
Warn_On_Overridden_Size : Boolean := False;
|
||||
-- Warn when explicit record component clause or array component_size
|
||||
-- clause specifies a size that overrides a size for the type which was
|
||||
-- set with an explicit size clause. Off by default, modified by use of
|
||||
-- -gnatw.s/.S (but not -gnatwa).
|
||||
|
||||
Warn_On_Questionable_Layout : Boolean := False;
|
||||
-- Warn when default layout of a record type is questionable for run-time
|
||||
-- efficiency reasons and would be improved by reordering the components.
|
||||
-- Off by default, modified by use of -gnatw.q/.Q (but not -gnatwa).
|
||||
|
||||
Warn_On_Record_Holes : Boolean := False;
|
||||
-- Warn when explicit record component clauses leave uncovered holes (gaps)
|
||||
-- in a record layout. Off by default, set by -gnatw.h (but not -gnatwa).
|
||||
|
||||
Warn_On_Size_Alignment : Boolean := True;
|
||||
-- Warn when explicit Size and Alignment clauses are given for a type, and
|
||||
-- the size is not a multiple of the alignment. Off by default, modified
|
||||
@ -104,6 +109,7 @@ package Warnsw is
|
||||
Warn_On_Overlap : Boolean;
|
||||
Warn_On_Overridden_Size : Boolean;
|
||||
Warn_On_Parameter_Order : Boolean;
|
||||
Warn_On_Questionable_Layout : Boolean;
|
||||
Warn_On_Questionable_Missing_Parens : Boolean;
|
||||
Warn_On_Record_Holes : Boolean;
|
||||
Warn_On_Redundant_Constructs : Boolean;
|
||||
|
Loading…
x
Reference in New Issue
Block a user