+2017-04-25 Gary Dismukes <dismukes@adacore.com>
+
+ * sem_ch3.adb, exp_util.adb, sem_prag.adb, exp_ch4.adb: Minor
+ reformatting.
+
+2017-04-25 Yannick Moy <moy@adacore.com>
+
+ * a-ngelfu.adb, a-ngelfu.ads: Add SPARK_Mode On on spec, Off
+ on body.
+
2017-04-25 Ed Schonberg <schonberg@adacore.com>
* sem_disp.adb (Check_Dispatching_Context): Add guard to refine
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2016, 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- --
with Ada.Numerics.Aux;
-package body Ada.Numerics.Generic_Elementary_Functions is
+package body Ada.Numerics.Generic_Elementary_Functions with
+ SPARK_Mode => Off
+is
use type Ada.Numerics.Aux.Double;
-- --
-- S p e c --
-- --
--- Copyright (C) 2012-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2012-2016, 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 --
generic
type Float_Type is digits <>;
-package Ada.Numerics.Generic_Elementary_Functions is
+package Ada.Numerics.Generic_Elementary_Functions with
+ SPARK_Mode => On
+is
pragma Pure;
function Sqrt (X : Float_Type'Base) return Float_Type'Base with
if Is_Access_Type (Target_Type) then
- -- If this type conversion was internally generated by the frontend
+ -- If this type conversion was internally generated by the front end
-- to displace the pointer to the object to reference an interface
- -- type and the original node was an 'Unrestricted_Access reference
+ -- type and the original node was an Unrestricted_Access attribute,
-- then skip applying accessibility checks (because, according to the
-- GNAT Reference Manual, this attribute is similar to 'Access except
-- that all accessibility and aliased view checks are omitted).
if Is_Ignored (DIC_Prag) then
null;
- -- Otherwise the DIC expression must be checked at runtime. Generate:
+ -- Otherwise the DIC expression must be checked at run time.
+ -- Generate:
-- pragma Check (<Nam>, <DIC_Expr>);
-- When the type inheriting the class-wide invariant is a concurrent
-- type, use the corresponding record type because it contains all
- -- primitive operations of the concurren type and allows for proper
+ -- primitive operations of the concurrent type and allows for proper
-- substitution.
if Is_Concurrent_Type (T) then
null;
-- Otherwise the invariant is checked. Build a pragma Check to verify
- -- the expression at runtime.
+ -- the expression at run time.
else
Assoc := New_List (
-- force every derived type to potentially provide an empty body.
-- * The invariant procedure does not need to be declared as abstract.
- -- This allows for a proper body which in turn avoids redundant
+ -- This allows for a proper body, which in turn avoids redundant
-- processing of the same invariants for types with multiple views.
-- * The class-wide type allows for calls to abstract primitives
- -- within a non-abstract subprogram. The calls are treated as
+ -- within a nonabstract subprogram. The calls are treated as
-- dispatching and require additional processing when they are
-- remapped to call primitives of derived types. See routine
-- Replace_References for details.
function Replace_Ref (Ref : Node_Id) return Traverse_Result is
procedure Remove_Controlling_Arguments (From_Arg : Node_Id);
- -- Reset the Controlling_Argument of all function calls which
+ -- Reset the Controlling_Argument of all function calls that
-- encapsulate node From_Arg.
----------------------------------
New_Ref := New_Occurrence_Of (Deriv_Obj, Loc);
-- The type of the _object parameter is class-wide when the
- -- expression comes from an assertion pragma which applies to
+ -- expression comes from an assertion pragma that applies to
-- an abstract parent type or an interface. The class-wide type
-- facilitates the preanalysis of the expression by treating
- -- calls to abstract primitives which mention the current
+ -- calls to abstract primitives that mention the current
-- instance of the type as dispatching. Once the calls are
-- remapped to invoke overriding or inherited primitives, the
-- calls no longer need to be dispatching. Examine all function
- -- calls which encapsule the _object parameter and reset their
+ -- calls that encapsulate the _object parameter and reset their
-- Controlling_Argument attribute.
if Is_Class_Wide_Type (Etype (Par_Obj))
end if;
-- Apply legality checks in RM 6.1.1 (10-13) concerning
- -- non-conforming preconditions in both an ancestor and
+ -- nonconforming preconditions in both an ancestor and
-- a progenitor operation.
if Present (Anc)
if Is_Interface (Typ) then
-- Interfaces are treated as the partial view of a private
- -- type in order to achieve uniformity with the general
+ -- type, in order to achieve uniformity with the general
-- case. As a result, an interface receives only a "partial"
- -- invariant procedure which is never called.
+ -- invariant procedure, which is never called.
if Has_Own_Invariants (Typ) then
Build_Invariant_Procedure_Body
New_Overloaded_Entity (New_Subp, Derived_Type);
- -- Ada RM 6.1.1 (15): If a subprogram inherits non-conforming class-wide
+ -- Ada RM 6.1.1 (15): If a subprogram inherits nonconforming class-wide
-- preconditions and the derived type is abstract, the derived operation
-- is abstract as well if parent subprogram is not abstract or null.
Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
- -- Create the declaration of the invariant procedure which will
- -- verify the invariant at run-time. Interfaces are treated as the
+ -- Create the declaration of the invariant procedure that will
+ -- verify the invariant at run time. Interfaces are treated as the
-- partial view of a private type in order to achieve uniformity
-- with the general case. As a result, an interface receives only
- -- a "partial" invariant procedure which is never called.
+ -- a "partial" invariant procedure, which is never called.
Build_Invariant_Procedure_Declaration
(Typ => Typ,
projects / gcc.git / commitdiff