+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
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
-- --
------------------------------------------------------------------------------
-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;
generic
type Result_Subtype is (<>);
-package Ada.Numerics.Discrete_Random is
+package Ada.Numerics.Discrete_Random with
+ SPARK_Mode => Off
+is
-- Basic facilities
-- --
-- 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- --
-- --
------------------------------------------------------------------------------
-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;
-- --
-- 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 --
with System.Random_Numbers;
-package Ada.Numerics.Float_Random is
+package Ada.Numerics.Float_Random with
+ SPARK_Mode => Off
+is
-- Basic facilities
------------------------
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
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));
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
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
-- 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);
Analyze_Constituent (Constit);
end if;
- -- A refined external state is subject to special rules with respect
- -- to its properties and constituents.
+ -- 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
+ -- (SPARK RM 7.2.8(2)).
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.
-
- if External_Constit_Seen then
- Check_External_Property
- (Prop_Nam => Name_Async_Readers,
- Enabled => Async_Readers_Enabled (State_Id),
- Constit => AR_Constit);
-
- Check_External_Property
- (Prop_Nam => Name_Async_Writers,
- Enabled => Async_Writers_Enabled (State_Id),
- Constit => AW_Constit);
-
- Check_External_Property
- (Prop_Nam => Name_Effective_Reads,
- Enabled => Effective_Reads_Enabled (State_Id),
- Constit => ER_Constit);
-
- Check_External_Property
- (Prop_Nam => Name_Effective_Writes,
- 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;
+ Check_External_Property
+ (Prop_Nam => Name_Async_Readers,
+ Enabled => Async_Readers_Enabled (State_Id),
+ Constit => AR_Constit);
+
+ Check_External_Property
+ (Prop_Nam => Name_Async_Writers,
+ Enabled => Async_Writers_Enabled (State_Id),
+ Constit => AW_Constit);
+
+ Check_External_Property
+ (Prop_Nam => Name_Effective_Reads,
+ Enabled => Effective_Reads_Enabled (State_Id),
+ Constit => ER_Constit);
+
+ Check_External_Property
+ (Prop_Nam => Name_Effective_Writes,
+ Enabled => Effective_Writes_Enabled (State_Id),
+ Constit => EW_Constit);
-- When a refined state is not external, it should not have external
-- constituents (SPARK RM 7.2.8(1)).
---------------------------------------------
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);
+ 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
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 --
--------------------
-- 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.
-- 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.
----------------
projects / gcc.git / commitdiff