OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[multiple changes] 

2016-04-18  Yannick Moy  <moy@adacore.com>

	* sem_util.adb, sem_util.ads (Has_Full_Default_Initialization): used
	outside of GNATprove, hence it should not be removed.

2016-04-18  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Refinement_Clause):
	The refinement of an external abstract state can now mention
	non-external constituents.
	(Check_External_Property): Update all SPARK RM references.

2016-04-18  Bob Duff  <duff@adacore.com>

	* exp_intr.adb: Remove some duplicated code.

2016-04-18  Yannick Moy  <moy@adacore.com>

	* a-nudira.adb, a-nudira.ads, a-nuflra.adb, a-nuflra.ads: Mark
	package spec and body out of SPARK.

2016-04-18  Johannes Kanig  <kanig@adacore.com>

	* spark_xrefs.ads: Minor comment update.

2016-04-18  Johannes Kanig  <kanig@adacore.com>

	* gnat1drv.adb (Gnat1drv): Force loading of System
	unit for SPARK.

2016-04-18  Bob Duff  <duff@adacore.com>

	* a-cuprqu.adb: Correction to previous change. If a new node
	is inserted at the front of the queue (because it is higher
	priority than the previous front node), we need to update
	Header.Next_Unequal -- not just in the case where the queue was
	previously empty.

From-SVN: r235122
This commit is contained in:
Arnaud Charlet 2016-04-18 12:41:18 +02:00
parent 142870f570
commit 1f55088db5
12 changed files with 220 additions and 118 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
gcc/ada/ChangeLog
View File

@ -1,3 +1,41 @@
2016-04-18 Yannick Moy <moy@adacore.com>
* sem_util.adb, sem_util.ads (Has_Full_Default_Initialization): used
outside of GNATprove, hence it should not be removed.
2016-04-18 Hristian Kirtchev <kirtchev@adacore.com>
* sem_prag.adb (Analyze_Refinement_Clause):
The refinement of an external abstract state can now mention
non-external constituents.
(Check_External_Property): Update all SPARK RM references.
2016-04-18 Bob Duff <duff@adacore.com>
* exp_intr.adb: Remove some duplicated code.
2016-04-18 Yannick Moy <moy@adacore.com>
* a-nudira.adb, a-nudira.ads, a-nuflra.adb, a-nuflra.ads: Mark
package spec and body out of SPARK.
2016-04-18 Johannes Kanig <kanig@adacore.com>
* spark_xrefs.ads: Minor comment update.
2016-04-18 Johannes Kanig <kanig@adacore.com>
* gnat1drv.adb (Gnat1drv): Force loading of System
unit for SPARK.
2016-04-18 Bob Duff <duff@adacore.com>
* a-cuprqu.adb: Correction to previous change. If a new node
is inserted at the front of the queue (because it is higher
priority than the previous front node), we need to update
Header.Next_Unequal -- not just in the case where the queue was
previously empty.
2016-04-18 Bob Duff <duff@adacore.com>
* a-cuprqu.ads: Change the representation of List_Type from a

9
gcc/ada/a-cuprqu.adb
View File

@ -187,10 +187,17 @@ package body Ada.Containers.Unbounded_Priority_Queues is
Prev.Next.Prev := Node;
Prev.Next := Node;
if List.Length = 0 then
if Prev = H then
-- Make sure Next_Unequal of the Header always points to the first
-- "real" node. Here, we've inserted a new first "real" node, so
-- must update.
List.Header.Next_Unequal := Node;
end if;
pragma Assert (List.Header.Next_Unequal = List.Header.Next);
List.Length := List.Length + 1;
if List.Length > List.Max_Length then

4
gcc/ada/a-nudira.adb
View File

@ -29,7 +29,9 @@
-- --
------------------------------------------------------------------------------
package body Ada.Numerics.Discrete_Random is
package body Ada.Numerics.Discrete_Random with
SPARK_Mode => Off
is
package SRN renames System.Random_Numbers;
use SRN;

4
gcc/ada/a-nudira.ads
View File

@ -41,7 +41,9 @@ with System.Random_Numbers;
generic
type Result_Subtype is (<>);
package Ada.Numerics.Discrete_Random is
package Ada.Numerics.Discrete_Random with
SPARK_Mode => Off
is
-- Basic facilities

6
gcc/ada/a-nuflra.adb
View File

@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
-- Copyright (C) 1992-2015, 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,9 @@
-- --
------------------------------------------------------------------------------
package body Ada.Numerics.Float_Random is
package body Ada.Numerics.Float_Random with
SPARK_Mode => Off
is
package SRN renames System.Random_Numbers;
use SRN;

6
gcc/ada/a-nuflra.ads
View File

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
@ -38,7 +38,9 @@
with System.Random_Numbers;
package Ada.Numerics.Float_Random is
package Ada.Numerics.Float_Random with
SPARK_Mode => Off
is
-- Basic facilities

66
gcc/ada/exp_intr.adb
View File

@ -852,11 +852,7 @@ package body Exp_Intr is
------------------------
procedure Expand_Source_Info (N : Node_Id; Nam : Name_Id) is
-- ???There is duplicated code here (see Add_Source_Info)
Loc : constant Source_Ptr := Sloc (N);
Ent : Entity_Id;
begin
-- Integer cases
@ -870,67 +866,7 @@ package body Exp_Intr is
else
Name_Len := 0;
case Nam is
when Name_File =>
Get_Decoded_Name_String
(Reference_Name (Get_Source_File_Index (Loc)));
when Name_Source_Location =>
Build_Location_String (Loc);
when Name_Enclosing_Entity =>
-- Skip enclosing blocks to reach enclosing unit
Ent := Current_Scope;
while Present (Ent) loop
exit when Ekind (Ent) /= E_Block
and then Ekind (Ent) /= E_Loop;
Ent := Scope (Ent);
end loop;
-- Ent now points to the relevant defining entity
Write_Entity_Name (Ent);
when Name_Compilation_ISO_Date =>
Name_Buffer (1 .. 10) := Opt.Compilation_Time (1 .. 10);
Name_Len := 10;
when Name_Compilation_Date =>
declare
subtype S13 is String (1 .. 3);
Months : constant array (1 .. 12) of S13 :=
("Jan", "Feb", "Mar", "Apr", "May", "Jun",
"Jul", "Aug", "Sep", "Oct", "Nov", "Dec");
M1 : constant Character := Opt.Compilation_Time (6);
M2 : constant Character := Opt.Compilation_Time (7);
MM : constant Natural range 1 .. 12 :=
(Character'Pos (M1) - Character'Pos ('0')) * 10 +
(Character'Pos (M2) - Character'Pos ('0'));
begin
-- Reformat ISO date into MMM DD YYYY (__DATE__) format
Name_Buffer (1 .. 3) := Months (MM);
Name_Buffer (4) := ' ';
Name_Buffer (5 .. 6) := Opt.Compilation_Time (9 .. 10);
Name_Buffer (7) := ' ';
Name_Buffer (8 .. 11) := Opt.Compilation_Time (1 .. 4);
Name_Len := 11;
end;
when Name_Compilation_Time =>
Name_Buffer (1 .. 8) := Opt.Compilation_Time (12 .. 19);
Name_Len := 8;
when others =>
raise Program_Error;
end case;
Add_Source_Info (Loc, Nam);
Rewrite (N,
Make_String_Literal (Loc,
Strval => String_From_Name_Buffer));

14
gcc/ada/gnat1drv.adb
View File

@ -1045,6 +1045,20 @@ begin
Original_Operating_Mode := Operating_Mode;
Frontend;
-- In GNATprove mode, force loading of System unit when tasking is
-- used, so that in particular System.Interrupt_Priority is available
-- to GNATprove for the generation of VCs for checking the respect of
-- Ceiling Protocol.
if GNATprove_Mode and Opt.Tasking_Used then
declare
Unused_E : constant Entity_Id :=
Rtsfind.RTE (Rtsfind.RE_Interrupt_Priority);
begin
null;
end;
end if;
-- Exit with errors if the main source could not be parsed
if Sinput.Main_Source_File = No_Source_File then

34
gcc/ada/sem_prag.adb
View File

@ -25514,7 +25514,7 @@ package body Sem_Prag is
Error_Msg_Name_1 := Prop_Nam;
-- The property is enabled in the related Abstract_State pragma
-- that defines the state (SPARK RM 7.2.8(3)).
-- that defines the state (SPARK RM 7.2.8(2)).
if Enabled then
if No (Constit) then
@ -25525,7 +25525,7 @@ package body Sem_Prag is
-- The property is missing in the declaration of the state, but
-- a constituent is introducing it in the state refinement
-- (SPARK RM 7.2.8(3)).
-- (SPARK RM 7.2.8(2)).
elsif Present (Constit) then
Error_Msg_Name_2 := Chars (Constit);
@ -25746,16 +25746,12 @@ package body Sem_Prag is
Analyze_Constituent (Constit);
end if;
-- A refined external state is subject to special rules with respect
-- to its properties and constituents.
if Is_External_State (State_Id) then
-- The set of properties that all external constituents yield must
-- match that of the refined state. There are two cases to detect:
-- the refined state lacks a property or has an extra property.
-- the refined state lacks a property or has an extra property
-- (SPARK RM 7.2.8(2)).
if External_Constit_Seen then
if Is_External_State (State_Id) then
Check_External_Property
(Prop_Nam => Name_Async_Readers,
Enabled => Async_Readers_Enabled (State_Id),
@ -25776,20 +25772,6 @@ package body Sem_Prag is
Enabled => Effective_Writes_Enabled (State_Id),
Constit => EW_Constit);
-- An external state may be refined to null (SPARK RM 7.2.8(2))
elsif Null_Seen then
null;
-- The external state has constituents, but none of them are
-- external (SPARK RM 7.2.8(2)).
else
SPARK_Msg_NE
("external state & requires at least one external "
& "constituent or null refinement", State, State_Id);
end if;
-- When a refined state is not external, it should not have external
-- constituents (SPARK RM 7.2.8(1)).
@ -26762,15 +26744,15 @@ package body Sem_Prag is
procedure Collect_Inherited_Class_Wide_Conditions (Subp : Entity_Id) is
Parent_Subp : constant Entity_Id := Overridden_Operation (Subp);
Prags : constant Node_Id := Contract (Parent_Subp);
In_Spec_Expr : Boolean;
Installed : Boolean;
Prag : Node_Id;
New_Prag : Node_Id;
Installed : Boolean;
In_Spec_Expr : Boolean;
begin
Installed := False;
-- Iterate over the contract of the overridden subprogram to find
-- Iterate over the contract of the overridden subprogram to find all
-- inherited class-wide pre- and postconditions.
if Present (Prags) then

104
gcc/ada/sem_util.adb
View File

@ -9046,6 +9046,110 @@ package body Sem_Util is
end if;
end Has_Enabled_Property;
-------------------------------------
-- Has_Full_Default_Initialization --
-------------------------------------
function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean is
Arg : Node_Id;
Comp : Entity_Id;
Prag : Node_Id;
begin
-- A private type and its full view is fully default initialized when it
-- is subject to pragma Default_Initial_Condition without an argument or
-- with a non-null argument. Since any type may act as the full view of
-- a private type, this check must be performed prior to the specialized
-- tests below.
if Has_Default_Init_Cond (Typ)
or else Has_Inherited_Default_Init_Cond (Typ)
then
Prag := Get_Pragma (Typ, Pragma_Default_Initial_Condition);
-- Pragma Default_Initial_Condition must be present if one of the
-- related entity flags is set.
pragma Assert (Present (Prag));
Arg := First (Pragma_Argument_Associations (Prag));
-- A non-null argument guarantees full default initialization
if Present (Arg) then
return Nkind (Arg) /= N_Null;
-- Otherwise the missing argument defaults the pragma to "True" which
-- is considered a non-null argument (see above).
else
return True;
end if;
end if;
-- A scalar type is fully default initialized if it is subject to aspect
-- Default_Value.
if Is_Scalar_Type (Typ) then
return Has_Default_Aspect (Typ);
-- An array type is fully default initialized if its element type is
-- scalar and the array type carries aspect Default_Component_Value or
-- the element type is fully default initialized.
elsif Is_Array_Type (Typ) then
return
Has_Default_Aspect (Typ)
or else Has_Full_Default_Initialization (Component_Type (Typ));
-- A protected type, record type or type extension is fully default
-- initialized if all its components either carry an initialization
-- expression or have a type that is fully default initialized. The
-- parent type of a type extension must be fully default initialized.
elsif Is_Record_Type (Typ) or else Is_Protected_Type (Typ) then
-- Inspect all entities defined in the scope of the type, looking for
-- uninitialized components.
Comp := First_Entity (Typ);
while Present (Comp) loop
if Ekind (Comp) = E_Component
and then Comes_From_Source (Comp)
and then No (Expression (Parent (Comp)))
and then not Has_Full_Default_Initialization (Etype (Comp))
then
return False;
end if;
Next_Entity (Comp);
end loop;
-- Ensure that the parent type of a type extension is fully default
-- initialized.
if Etype (Typ) /= Typ
and then not Has_Full_Default_Initialization (Etype (Typ))
then
return False;
end if;
-- If we get here, then all components and parent portion are fully
-- default initialized.
return True;
-- A task type is fully default initialized by default
elsif Is_Task_Type (Typ) then
return True;
-- Otherwise the type is not fully default initialized
else
return False;
end if;
end Has_Full_Default_Initialization;
--------------------
-- Has_Infinities --
--------------------

13
gcc/ada/sem_util.ads
View File

@ -1034,6 +1034,19 @@ package Sem_Util is
-- Determine whether subprogram Subp_Id has an effectively volatile formal
-- parameter or returns an effectively volatile value.
function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean;
-- Determine whether type Typ defines "full default initialization" as
-- specified by SPARK RM 3.1. To qualify as such, the type must be
-- * A scalar type with specified Default_Value
-- * An array-of-scalar type with specified Default_Component_Value
-- * An array type whose element type defines full default initialization
-- * A protected type, record type or type extension whose components
-- either include a default expression or have a type which defines
-- full default initialization. In the case of type extensions, the
-- parent type defines full default initialization.
-- * A task type
-- * A private type whose Default_Initial_Condition is non-null
function Has_Infinities (E : Entity_Id) return Boolean;
-- Determines if the range of the floating-point type E includes
-- infinities. Returns False if E is not a floating-point type.

2
gcc/ada/spark_xrefs.ads
View File

@ -200,7 +200,7 @@ package SPARK_Xrefs is
-- not relate to Generated Globals.
-- The processing (reading and writing) of this section happens in
-- package Flow_Computed_Globals (from the SPARK 2014 sources), for
-- package Flow_Generated_Globals (from the SPARK 2014 sources), for
-- further information please refer there.
----------------