+2017-04-27 Steve Baird <baird@adacore.com>
+
+ * exp_ch9.adb (Expand_N_Asynchronous_Select): Initialize the Cancel
+ flag when it is declared in order to avoid confusing CodePeer about
+ the possibility of an uninitialized variable read.
+
+2017-04-27 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_dim.adb (Analyze_Dimension_Object_Declaration): There is
+ no dimensionality error if the subtype of the expression is
+ identical to the nominal subtype in the declaration, even though
+ the expression itself may have been constant-folded and lack a
+ dimension vector.
+ * sem_dim.ads: Add comments on setting of dimension vectors and
+ its interaction with node rewritings and side-effect removal.
+
+2017-04-27 Bob Duff <duff@adacore.com>
+
+ * debug.adb: Minor comment correction.
+ * sem_dim.ads: Minor reformatting and typo fixes.
+
+2017-04-27 Bob Duff <duff@adacore.com>
+
+ * g-table.adb, g-table.adsa, scos.h: From the C side, access First and
+ Last of the tables via function calls, rather than relying on layout
+ of data structures.
+
+2017-04-27 Ed Schonberg <schonberg@adacore.com>
+
+ * exp_util.adb: No wrapper in GNATprove mode.
+
+2017-04-27 Yannick Moy <moy@adacore.com>
+
+ * sem_res.adb (Resolve_Comparison_Op): Always
+ evaluate comparisons between values of universal types.
+
+2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_elab.adb (Check_Internal_Call_Continue): Do not generate
+ an elaboration counter nor a check when in GNATprove mode.
+ * sem_util.adb (Build_Elaboration_Entity): Do not create an
+ elaboration counter when in GNATprove mode.
+
2017-04-27 Ed Schonberg <schonberg@adacore.com>
* freeze.adb: copy-paste typo.
-- prefer specs with no bodies to specs with bodies, and between two
-- specs with bodies, prefers the one whose body is closer to being
-- able to be elaborated. This is a clear improvement, but we provide
- -- this debug flag in case of regressions. Note: -gnatdo is even older
- -- than -gnatdp.
+ -- this debug flag in case of regressions. Note: -do is even older
+ -- than -dp.
-- dp Use old elaboration order preference. The new preference rules
-- elaborate all units within a strongly connected component together,
Make_Object_Declaration (Loc,
Defining_Identifier => Cancel_Param,
Object_Definition =>
- New_Occurrence_Of (Standard_Boolean, Loc)));
+ New_Occurrence_Of (Standard_Boolean, Loc),
+ Expression =>
+ New_Occurrence_Of (Standard_False, Loc),
+ -- True would work equally well here. This initialization
+ -- should be dead, but only because of things (e.g.,
+ -- abortion deferral) that CodePeer doesn't know about.
+ -- We want to avoid CodePeer complaints about a possible read
+ -- of an uninitialized variable when this variable is read,
+ -- so we initialize it here.
+ Has_Init_Expression => True));
-- Remove and save the call to Call_Simple
if Present (New_E) then
Rewrite (N, New_Occurrence_Of (New_E, Sloc (N)));
- -- If the entity is an overridden primitive, we must build a
- -- wrapper for the current inherited operation.
+ -- If the entity is an overridden primitive and we are not
+ -- in proof mode, we must build a wrapper for the current
+ -- inherited operation.
- if Is_Subprogram (New_E) then
+ if Is_Subprogram (New_E)
+ and then not GNATprove_Mode
+ then
Needs_Wrapper := True;
end if;
end if;
-- --
-- B o d y --
-- --
--- Copyright (C) 1998-2014, AdaCore --
+-- Copyright (C) 1998-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- --
Last_Val := Last_Val - 1;
end Decrement_Last;
+ -----------
+ -- First --
+ -----------
+
+ function First return Table_Index_Type is
+ begin
+ return Table_Low_Bound;
+ end First;
+
--------------
-- For_Each --
--------------
-- --
-- S p e c --
-- --
--- Copyright (C) 1998-2015, AdaCore --
+-- Copyright (C) 1998-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- --
-- Free all allocated memory for the table. A call to Init is required
-- before any use of this table after calling Free.
- First : constant Table_Index_Type := Table_Low_Bound;
- -- Export First as synonym for Low_Bound (parallel with use of Last)
+ function First return Table_Index_Type;
+ pragma Inline (First);
+ -- Export First as synonym for Table_Low_Bound (parallel with use of Last)
procedure Set_Last (New_Val : Table_Index_Type);
pragma Inline (Set_Last);
* *
* C Header File *
* *
- * Copyright (C) 2014, Free Software Foundation, Inc. *
+ * Copyright (C) 2014-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- *
extern SCO_Unit_Table_Type scos__sco_unit_table__table;
#define SCO_Unit_Table scos__sco_unit_table__table
-extern Int scos__sco_unit_table__min;
-#define SCO_Unit_Table_Min scos__sco_unit_table__min
+extern Int scos__sco_unit_table__first(void);
+#define SCO_Unit_Table_First scos__sco_unit_table__first
-extern Int scos__sco_unit_table__last_val;
-#define SCO_Unit_Table_Last_Val scos__sco_unit_table__last_val
+extern Int scos__sco_unit_table__last(void);
+#define SCO_Unit_Table_Last scos__sco_unit_table__last
/* SCOs table: */
extern SCO_Table_Type scos__sco_table__table;
#define SCO_Table scos__sco_table__table
-extern Int scos__sco_table__min;
-#define SCO_Table_Min scos__sco_table__min
+extern Int scos__sco_table__first(void);
+#define SCO_Table_First scos__sco_table__first
-extern Int scos__sco_table__last_val;
-#define SCO_Table_Last_Val scos__sco_table__last_val
+extern Int scos__sco_table__last(void);
+#define SCO_Table_Last scos__sco_table__last
#ifdef __cplusplus
}
Set_Dimensions (Id, Dim_Of_Expr);
+ -- Expression may have been constant-folded. If nominal type
+ -- has dimensions, verify that expression has same type.
+
+ elsif Exists (Dim_Of_Etyp) and then Etype (Expr) = Etyp then
+ null;
+
-- For all other cases, issue an error message
else
-- --
-- S p e c --
-- --
--- Copyright (C) 2011-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 2011-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- --
-- Phase 2 is called only when the node allows a dimension (see body of
-- Sem_Dim to get the list of nodes that permit dimensions).
+-- In principle every node that is a component of a floating-point expression
+-- may have a dimension vector. However, the dimensionality checking is for
+-- the most part a bottom-up tree traversal, and the dimensions of operands
+-- become irrelevant once the dimensions of an operation have been computed.
+-- To minimize space use, the dimensions of operands are removed after the
+-- computation of the dimensions of the parent operation. This may complicate
+-- the analysis of nodes that have been constant-folded or otherwise rewritten
+-- when removing side effects. In such cases, the (sub)type of the expression
+-- is used to determine the applicable dimensions.
+
with Types; use Types;
package Sem_Dim is
-- Call is not at outer level
else
+ -- Do not generate elaboration checks in GNATprove mode because the
+ -- elaboration counter and the check are both forms of expansion.
+
+ if GNATprove_Mode then
+ null;
+
-- Deal with dynamic elaboration check
- if not Elaboration_Checks_Suppressed (E) then
+ elsif not Elaboration_Checks_Suppressed (E) then
Set_Elaboration_Entity_Required (E);
-- Case of no elaboration entity allocated yet
-- this Eval call may change N to True/False. Skip this evaluation
-- inside assertions, in order to keep assertions as written by users
-- for tools that rely on these, e.g. GNATprove for loop invariants.
-
- if In_Assertion_Expr = 0 then
+ -- Except evaluation is still performed even inside assertions for
+ -- comparisons between values of universal type, which are useless
+ -- for static analysis tools, and not supported even by GNATprove.
+
+ if In_Assertion_Expr = 0
+ or else (Is_Universal_Numeric_Type (Etype (L))
+ and then
+ Is_Universal_Numeric_Type (Etype (R)))
+ then
Eval_Relational_Op (N);
end if;
end Resolve_Comparison_Op;
elsif ASIS_Mode then
return;
- -- See if we need elaboration entity.
+ -- Do not generate an elaboration entity in GNATprove move because the
+ -- elaboration counter is a form of expansion.
+
+ elsif GNATprove_Mode then
+ return;
+
+ -- See if we need elaboration entity
-- We always need an elaboration entity when preserving control flow, as
-- we want to remain explicit about the unit's elaboration order.