+2017-09-25 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_res.adb (Replace_Actual_Discriminants): Replace a discriminant
+ for GNATprove.
+ (Resolve_Entry): Clean up predicate
+
+2017-09-25 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_prag.adb (Analyze_Constituent): Raise Unrecoverable_Error rather
+ than Program_Error because U_E is more in line with respect to the
+ intended behavior.
+
+2017-09-25 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch13.adb (Resolve_Aspect_Expressions): The expression for aspect
+ Storage_Size does not freeze, and thus can include references to
+ deferred constants.
+
+2017-09-25 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * exp_spark.adb (Expand_SPARK_Potential_Renaming): Do not process a
+ reference when it appears within a pragma of no significance to SPARK.
+ (In_Insignificant_Pragma): New routine.
+ * sem_prag.ads: Add new table Pragma_Significant_In_SPARK.
+
+2017-09-25 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch12.adb (Analyze_Associations, case N_Formal_Package): If the
+ actual is a renaming, indicate that it is the renamed package that must
+ be frozen before the instantiation.
+
+2017-09-25 Yannick Moy <moy@adacore.com>
+
+ * doc/gnat_ugn/gnat_and_program_execution.rst: Fix typo in description
+ of dimensionality system in GNAT UG.
+ * gnat_ugn.texi: Regenerate.
+
+2017-09-25 Yannick Moy <moy@adacore.com>
+
+ * gnat1drv.adb: Call Check_Safe_Pointers from the frontend in
+ GNATprove_Mode when switch -gnatdF used.
+
+2017-09-25 Piotr Trojanek <trojanek@adacore.com>
+
+ * adabkend.adb (Call_Back_End): Reset Current_Error_Node when starting
+ the backend.
+
2017-09-25 Javier Miranda <miranda@adacore.com>
* exp_imgv.adb (Expand_Image_Attribute): Disable the optimized
-- --
-- B o d y --
-- --
--- Copyright (C) 2001-2016, AdaCore --
+-- Copyright (C) 2001-2017, AdaCore --
-- --
-- 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- --
-- This is the version of the Back_End package for back ends written in Ada
+with Atree; use Atree;
with Debug;
with Lib;
with Opt; use Opt;
Write_Eol;
end if;
+ -- Frontend leaves the Current_Error_Node at a location that is
+ -- meaningless and confusing when emitting bugboxes from the backed. By
+ -- resetting it here we default to "No source file position information
+ -- available" message on backend crashes.
+
+ Current_Error_Node := Empty;
+
Driver (Lib.Cunit (Types.Main_Unit));
end Call_Back_End;
.. code-block:: ada
Distance := 5.0;
- Distance := 5.0 * kg:
+ Distance := 5.0 * kg;
are rejected with the following diagnoses:
.. index:: Dimension Vector (for a dimensioned subtype)
.. index:: Dimension aspect
.. index:: Dimension_System aspect
-
+
The ``Dimension`` aspect of a dimensioned subtype ``S`` defines a mapping
from the base type's Unit_Names to integer (or, more generally, rational)
values. This mapping is the *dimension vector* (also referred to as the
end;
Here ``DV(Acc)`` = ``DV(Acceleration)`` =
-``(Meter=>1, Kilogram=>0, Second => -2, Ampere=>0, Kelvin=>0, Mole=>0, Candela => 0)``.
-Symbolically, we can express this as ``Meter / Second**2``.
+``(Meter=>1, Kilogram=>0, Second=>-2, Ampere=>0, Kelvin=>0, Mole=>0, Candela=>0)``.
+Symbolically, we can express this as ``Meter / Second**2``.
The dimension vector of an arithmetic expression is synthesized from the
dimension vectors of its components, with compile-time dimensionality checks
* :samp:`DV({op expr})`, where *op* is a unary operator, is :samp:`DV({expr})`
* :samp:`DV({expr1 op expr2})` where *op* is "+" or "-" is :samp:`DV({expr1})`
- provided that :samp:`DV({expr1})` = :samp:`DV({expr2})`.
+ provided that :samp:`DV({expr1})` = :samp:`DV({expr2})`.
If this condition is not met then the construct is illegal.
* :samp:`DV({expr1} * {expr2})` is :samp:`DV({expr1})` + :samp:`DV({expr2})`,
acc-10.0 > 0.0
and is thus illegal. Analogously a conditional expression
-requires the same dimension vector for each branch.
+requires the same dimension vector for each branch.
The dimension vector of a type conversion :samp:`T({expr})` is defined
as follows, based on the nature of ``T``:
Thus, if *expr* is of a dimensioned subtype of ``T``, the conversion may
be regarded as a "view conversion" that preserves dimensionality.
- This rule makes it possible to write generic code that can be instantiated
+ This rule makes it possible to write generic code that can be instantiated
with compatible dimensioned subtypes. The generic unit will contain
conversions that will consequently be present in instantiations, but
conversions to the base type will preserve dimensionality and make it
The dimension vector for a type qualification :samp:`T'({expr})` is the same
as for the type conversion :samp:`T({expr})`.
-An assignment statement
+An assignment statement
.. code-block:: ada
-
+
Source := Target;
requires ``DV(Source)`` = ``DV(Target)``, and analogously for parameter
Expr : constant Node_Id := Relocate_Node (First (Exprs));
Pref : constant Node_Id := Prefix (N);
- function Is_User_Defined_Enumeration_Type
- (Typ : Entity_Id) return Boolean;
- -- Return True if Typ is a user-defined enumeration type
-
procedure Expand_User_Defined_Enumeration_Image;
-- Expand attribute 'Image in user-defined enumeration types, avoiding
-- string copy.
+ function Is_User_Defined_Enumeration_Type
+ (Typ : Entity_Id) return Boolean;
+ -- Return True if Typ is a user-defined enumeration type
+
-------------------------------------------
-- Expand_User_Defined_Enumeration_Image --
-------------------------------------------
Object_Definition =>
New_Occurrence_Of (Standard_Natural, Loc),
Constant_Present => True,
- Expression =>
+ Expression =>
Convert_To (Standard_Natural,
Make_Attribute_Reference (Loc,
Attribute_Name => Name_Pos,
Object_Definition =>
New_Occurrence_Of (Standard_Natural, Loc),
Constant_Present => True,
- Expression =>
+ Expression =>
Convert_To (Standard_Natural,
Make_Indexed_Component (Loc,
Prefix =>
Object_Definition =>
New_Occurrence_Of (Standard_Natural, Loc),
Constant_Present => True,
- Expression =>
+ Expression =>
Convert_To (Standard_Natural,
Make_Indexed_Component (Loc,
Prefix =>
Insert_Actions (N, Ins_List, Suppress => All_Checks);
Rewrite (N,
- Unchecked_Convert_To (S1_Id,
- New_Occurrence_Of (P4_Id, Loc)));
+ Unchecked_Convert_To (S1_Id, New_Occurrence_Of (P4_Id, Loc)));
+
Analyze_And_Resolve (N, Standard_String);
end Expand_User_Defined_Enumeration_Image;
with Rtsfind; use Rtsfind;
with Sem; use Sem;
with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
-------------------------------------
procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
+ function In_Insignificant_Pragma (Nod : Node_Id) return Boolean;
+ -- Determine whether arbitrary node Nod appears within a significant
+ -- pragma for SPARK.
+
+ -----------------------------
+ -- In_Insignificant_Pragma --
+ -----------------------------
+
+ function In_Insignificant_Pragma (Nod : Node_Id) return Boolean is
+ Par : Node_Id;
+
+ begin
+ -- Climb the parent chain looking for an enclosing pragma
+
+ Par := Nod;
+ while Present (Par) loop
+ if Nkind (Par) = N_Pragma then
+ return not Pragma_Significant_In_SPARK (Get_Pragma_Id (Par));
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Par) then
+ exit;
+ end if;
+
+ Par := Parent (Par);
+ end loop;
+
+ return False;
+ end In_Insignificant_Pragma;
+
+ -- Local variables
+
Loc : constant Source_Ptr := Sloc (N);
Obj_Id : constant Entity_Id := Entity (N);
Typ : constant Entity_Id := Etype (N);
Ren : Node_Id;
+ -- Start of processing for Expand_SPARK_Potential_Renaming
+
begin
-- Replace a reference to a renaming with the actual renamed object
if Present (Ren) then
+ -- Do not process a reference when it appears within a pragma of
+ -- no significance to SPARK. It is assumed that the replacement
+ -- will violate the semantics of the pragma and cause a spurious
+ -- error.
+
+ if In_Insignificant_Pragma (N) then
+ return;
+
-- Instantiations and inlining of subprograms employ "prologues"
-- which map actual to formal parameters by means of renamings.
-- Replace a reference to a formal by the corresponding actual
-- parameter.
- if Nkind (Ren) in N_Entity then
+ elsif Nkind (Ren) in N_Entity then
Rewrite (N, New_Occurrence_Of (Ren, Loc));
-- Otherwise the renamed object denotes a name
-- --
------------------------------------------------------------------------------
-with Atree; use Atree;
-with Back_End; use Back_End;
+with Atree; use Atree;
+with Back_End; use Back_End;
with Checks;
with Comperr;
-with Csets; use Csets;
-with Debug; use Debug;
+with Csets; use Csets;
+with Debug; use Debug;
with Elists;
-with Errout; use Errout;
+with Errout; use Errout;
with Exp_CG;
with Fmap;
-with Fname; use Fname;
-with Fname.UF; use Fname.UF;
+with Fname; use Fname;
+with Fname.UF; use Fname.UF;
with Frontend;
-with Ghost; use Ghost;
-with Gnatvsn; use Gnatvsn;
+with Ghost; use Ghost;
+with Gnatvsn; use Gnatvsn;
with Inline;
-with Lib; use Lib;
-with Lib.Writ; use Lib.Writ;
+with Lib; use Lib;
+with Lib.Writ; use Lib.Writ;
with Lib.Xref;
-with Namet; use Namet;
+with Namet; use Namet;
with Nlists;
-with Opt; use Opt;
-with Osint; use Osint;
-with Osint.C; use Osint.C;
-with Output; use Output;
+with Opt; use Opt;
+with Osint; use Osint;
+with Osint.C; use Osint.C;
+with Output; use Output;
with Par_SCO;
with Prepcomp;
-with Repinfo; use Repinfo;
+with Repinfo; use Repinfo;
with Restrict;
-with Rident; use Rident;
+with Rident; use Rident;
with Rtsfind;
with SCOs;
with Sem;
with Sem_SPARK; use Sem_SPARK;
with Sem_Type;
with Set_Targ;
-with Sinfo; use Sinfo;
-with Sinput.L; use Sinput.L;
-with Snames; use Snames;
-with Sprint; use Sprint;
+with Sinfo; use Sinfo;
+with Sinput.L; use Sinput.L;
+with Snames; use Snames;
+with Sprint; use Sprint;
with Stringt;
-with Stylesw; use Stylesw;
-with Targparm; use Targparm;
+with Stylesw; use Stylesw;
+with Targparm; use Targparm;
with Tbuild;
with Tree_Gen;
-with Treepr; use Treepr;
+with Treepr; use Treepr;
with Ttypes;
-with Types; use Types;
-with Uintp; use Uintp;
-with Uname; use Uname;
+with Types; use Types;
+with Uintp; use Uintp;
+with Uname; use Uname;
with Urealp;
with Usage;
-with Validsw; use Validsw;
+with Validsw; use Validsw;
with System.Assertions;
with System.OS_Lib;
@copying
@quotation
-GNAT User's Guide for Native Platforms , Sep 13, 2017
+GNAT User's Guide for Native Platforms , Sep 25, 2017
AdaCore
@example
Distance := 5.0;
-Distance := 5.0 * kg:
+Distance := 5.0 * kg;
@end example
@end quotation
@end quotation
Here @code{DV(Acc)} = @code{DV(Acceleration)} =
-@code{(Meter=>1, Kilogram=>0, Second => -2, Ampere=>0, Kelvin=>0, Mole=>0, Candela => 0)}.
+@code{(Meter=>1, Kilogram=>0, Second=>-2, Ampere=>0, Kelvin=>0, Mole=>0, Candela=>0)}.
Symbolically, we can express this as @code{Meter / Second**2}.
The dimension vector of an arithmetic expression is synthesized from the
-- Note well: If this function or related code is modified, it should be
-- tested by hand, because automated testing doesn't exercise it.
+ -------------------------
+ -- Get_Ceiling_Support --
+ -------------------------
+
function Get_Ceiling_Support return Boolean is
Ceiling_Support : Boolean := False;
begin
----------------------------------
function Compute_Base_Monotonic_Clock return Duration is
- TS_Bef0, TS_Mon0, TS_Aft0 : aliased timespec;
- TS_Bef, TS_Mon, TS_Aft : aliased timespec;
- Bef, Mon, Aft : Duration;
- Res_B, Res_M, Res_A : Interfaces.C.int;
+ Aft : Duration;
+ Bef : Duration;
+ Mon : Duration;
+ Res_A : Interfaces.C.int;
+ Res_B : Interfaces.C.int;
+ Res_M : Interfaces.C.int;
+ TS_Aft : aliased timespec;
+ TS_Aft0 : aliased timespec;
+ TS_Bef : aliased timespec;
+ TS_Bef0 : aliased timespec;
+ TS_Mon : aliased timespec;
+ TS_Mon0 : aliased timespec;
+
begin
- Res_B := clock_gettime
- (clock_id => OSC.CLOCK_REALTIME, tp => TS_Bef0'Unchecked_Access);
+ Res_B :=
+ clock_gettime
+ (clock_id => OSC.CLOCK_REALTIME,
+ tp => TS_Bef0'Unchecked_Access);
pragma Assert (Res_B = 0);
- Res_M := clock_gettime
- (clock_id => OSC.CLOCK_RT_Ada, tp => TS_Mon0'Unchecked_Access);
+
+ Res_M :=
+ clock_gettime
+ (clock_id => OSC.CLOCK_RT_Ada,
+ tp => TS_Mon0'Unchecked_Access);
pragma Assert (Res_M = 0);
- Res_A := clock_gettime
- (clock_id => OSC.CLOCK_REALTIME, tp => TS_Aft0'Unchecked_Access);
+
+ Res_A :=
+ clock_gettime
+ (clock_id => OSC.CLOCK_REALTIME,
+ tp => TS_Aft0'Unchecked_Access);
pragma Assert (Res_A = 0);
for I in 1 .. 10 loop
+
-- Guard against a leap second that will cause CLOCK_REALTIME to jump
-- backwards. In the extrenmely unlikely event we call clock_gettime
-- before and after the jump the epoch, the result will be off
-- Also try to calculate the most accurate epoch by taking the
-- minimum difference of 10 tries.
- Res_B := clock_gettime
- (clock_id => OSC.CLOCK_REALTIME, tp => TS_Bef'Unchecked_Access);
+ Res_B :=
+ clock_gettime
+ (clock_id => OSC.CLOCK_REALTIME,
+ tp => TS_Bef'Unchecked_Access);
pragma Assert (Res_B = 0);
- Res_M := clock_gettime
- (clock_id => OSC.CLOCK_RT_Ada, tp => TS_Mon'Unchecked_Access);
+
+ Res_M :=
+ clock_gettime
+ (clock_id => OSC.CLOCK_RT_Ada,
+ tp => TS_Mon'Unchecked_Access);
pragma Assert (Res_M = 0);
- Res_A := clock_gettime
- (clock_id => OSC.CLOCK_REALTIME, tp => TS_Aft'Unchecked_Access);
+
+ Res_A :=
+ clock_gettime
+ (clock_id => OSC.CLOCK_REALTIME,
+ tp => TS_Aft'Unchecked_Access);
pragma Assert (Res_A = 0);
- if (TS_Bef0.tv_sec /= TS_Aft0.tv_sec and then
- TS_Bef.tv_sec = TS_Aft.tv_sec)
- -- The calls to clock_gettime before the loop were no good
- or else
- (TS_Bef0.tv_sec = TS_Aft0.tv_sec and then
- TS_Bef.tv_sec = TS_Aft.tv_sec and then
- (TS_Aft.tv_nsec - TS_Bef.tv_nsec <
- TS_Aft0.tv_nsec - TS_Bef0.tv_nsec))
- -- The most recent calls to clock_gettime were better
+ -- The calls to clock_gettime before the loop were no good
+
+ if (TS_Bef0.tv_sec /= TS_Aft0.tv_sec
+ and then TS_Bef.tv_sec = TS_Aft.tv_sec)
+
+ -- The most recent calls to clock_gettime were better
+
+ or else
+ (TS_Bef0.tv_sec = TS_Aft0.tv_sec
+ and then TS_Bef.tv_sec = TS_Aft.tv_sec
+ and then (TS_Aft.tv_nsec - TS_Bef.tv_nsec
+ < TS_Aft0.tv_nsec - TS_Bef0.tv_nsec))
then
TS_Bef0 := TS_Bef;
TS_Aft0 := TS_Aft;
Mon := To_Duration (TS_Mon0);
Aft := To_Duration (TS_Aft0);
- return Bef / 2 + Aft / 2 - Mon;
-- Distribute the division, to avoid potential type overflow someday
+
+ return Bef / 2 + Aft / 2 - Mon;
end Compute_Base_Monotonic_Clock;
--------------
if Needs_Freezing then
Check_Generic_Parent;
- Set_Has_Delayed_Freeze (Actual);
- Append_Elmt (Actual, Actuals_To_Freeze);
+
+ -- If the actual is a renaming of a proper
+ -- instance of the formal package, indicate
+ -- that it is the instance that must be frozen.
+
+ if Nkind (Parent (Actual)) =
+ N_Package_Renaming_Declaration
+ then
+ Set_Has_Delayed_Freeze
+ (Renamed_Entity (Actual));
+ Append_Elmt
+ (Renamed_Entity (Actual), Actuals_To_Freeze);
+ else
+ Set_Has_Delayed_Freeze (Actual);
+ Append_Elmt (Actual, Actuals_To_Freeze);
+ end if;
end if;
end if;
end Explicit_Freeze_Check;
Set_Must_Not_Freeze (Expr);
Preanalyze_Spec_Expression (Expr, E);
+ -- Ditto for Storage_Size. Any other aspects that carry
+ -- expressions that should not freeze ??? This is only
+ -- relevant to the misuse of deferred constants.
+
+ when Aspect_Storage_Size =>
+ Set_Must_Not_Freeze (Expr);
+ Preanalyze_Spec_Expression (Expr, Any_Integer);
+
when others =>
if Present (Expr) then
case Aspect_Argument (A_Id) is
Analyze (N);
raise Pragma_Exit;
- -- No other possibilities
+ -- No other possibilities
when others =>
raise Program_Error;
-- Stop the compilation, as this leads to a multitude
-- of misleading cascaded errors.
- raise Program_Error;
+ raise Unrecoverable_Error;
end if;
-- The constituent is a valid state or object
Pragma_Warnings => True,
others => False);
+ -- The following table lists all pragmas which are significant in SPARK and
+ -- as a result get translated into verification conditions. The table is an
+ -- amalgamation of the pragmas listed in SPARK RM 16.1 and internally added
+ -- entries.
+
+ Pragma_Significant_In_SPARK : constant array (Pragma_Id) of Boolean :=
+ (Pragma_All_Calls_Remote => False,
+ Pragma_Asynchronous => False,
+ Pragma_Default_Storage_Pool => False,
+ Pragma_Discard_Names => False,
+ Pragma_Dispatching_Domain => False,
+ Pragma_Priority_Specific_Dispatching => False,
+ Pragma_Remote_Call_Interface => False,
+ Pragma_Remote_Types => False,
+ Pragma_Shared_Passive => False,
+ Pragma_Task_Dispatching_Policy => False,
+ Pragma_Warnings => False,
+ others => True);
+
-----------------
-- Subprograms --
-----------------
-- Start of processing for Replace_Actual_Discriminants
begin
- if not Expander_Active then
+ if Expander_Active then
+ null;
+
+ -- Allow the replacement of concurrent discriminants in GNATprove even
+ -- though this is a light expansion activity. Note that generic units
+ -- are not modified.
+
+ elsif GNATprove_Mode and not Inside_A_Generic then
+ null;
+
+ else
return;
end if;
Tsk := Prefix (Prefix (Name (N)));
end if;
- if No (Tsk) then
- return;
- else
+ if Present (Tsk) then
Replace_Discrs (Default);
end if;
end Replace_Actual_Discriminants;
Rewrite (Actval,
Make_Raise_Constraint_Error (Loc,
Reason => CE_Range_Check_Failed));
+
Set_Raises_Constraint_Error (Actval);
Set_Etype (Actval, Etype (F));
end if;
Assoc :=
Make_Parameter_Association (Loc,
Explicit_Actual_Parameter => Actval,
- Selector_Name => Make_Identifier (Loc, Chars (F)));
+ Selector_Name => Make_Identifier (Loc, Chars (F)));
-- Case of insertion is first named actual
- if No (Prev) or else
- Nkind (Parent (Prev)) /= N_Parameter_Association
+ if No (Prev)
+ or else Nkind (Parent (Prev)) /= N_Parameter_Association
then
Set_Next_Named_Actual (Assoc, First_Named_Actual (N));
Set_First_Named_Actual (N, Actval);
Index := First (Expressions (Entry_Name));
Resolve (Index, Entry_Index_Type (Nam));
- -- Generate a reference for the index entity when the index is not a
- -- literal.
+ -- Generate a reference for the index when it denotes an entity
- if Nkind (Index) in N_Has_Entity
- and then Nkind (Entity (Index)) in N_Entity
- then
- Generate_Reference (Entity (Index), Nam, ' ');
+ if Is_Entity_Name (Index) then
+ Generate_Reference (Entity (Index), Nam);
end if;
-- Up to this point the expression could have been the actual in a
projects / gcc.git / commitdiff