From: Arnaud Charlet Date: Tue, 25 Apr 2017 12:11:12 +0000 (+0200) Subject: [multiple changes] X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ca0b6141fa6a9c98939224ebc3b7ddc171df5b96;p=gcc.git [multiple changes] 2017-04-25 Gary Dismukes * sem_ch3.adb, exp_util.adb, sem_prag.adb, exp_ch4.adb: Minor reformatting. 2017-04-25 Yannick Moy * a-ngelfu.adb, a-ngelfu.ads: Add SPARK_Mode On on spec, Off on body. From-SVN: r247207 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 492070248fd..a3a79cd89cc 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,13 @@ +2017-04-25 Gary Dismukes + + * sem_ch3.adb, exp_util.adb, sem_prag.adb, exp_ch4.adb: Minor + reformatting. + +2017-04-25 Yannick Moy + + * a-ngelfu.adb, a-ngelfu.ads: Add SPARK_Mode On on spec, Off + on body. + 2017-04-25 Ed Schonberg * sem_disp.adb (Check_Dispatching_Context): Add guard to refine diff --git a/gcc/ada/a-ngelfu.adb b/gcc/ada/a-ngelfu.adb index f17d92497ac..e7a75eea8cf 100644 --- a/gcc/ada/a-ngelfu.adb +++ b/gcc/ada/a-ngelfu.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -38,7 +38,9 @@ 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; diff --git a/gcc/ada/a-ngelfu.ads b/gcc/ada/a-ngelfu.ads index 8b257b62b41..767708d5209 100644 --- a/gcc/ada/a-ngelfu.ads +++ b/gcc/ada/a-ngelfu.ads @@ -6,7 +6,7 @@ -- -- -- 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 -- @@ -36,7 +36,9 @@ 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 diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb index 658c3d8fbea..bc0aea2e2cd 100644 --- a/gcc/ada/exp_ch4.adb +++ b/gcc/ada/exp_ch4.adb @@ -10779,9 +10779,9 @@ package body Exp_Ch4 is 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). diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 35c5ed2c831..19ba42b024a 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -1292,7 +1292,8 @@ package body Exp_Util is 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 (, ); @@ -2245,7 +2246,7 @@ package body Exp_Util is -- 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 @@ -2417,7 +2418,7 @@ package body Exp_Util is 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 ( @@ -3395,11 +3396,11 @@ package body Exp_Util is -- 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. @@ -11506,7 +11507,7 @@ package body Exp_Util is 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. ---------------------------------- @@ -11630,14 +11631,14 @@ package body Exp_Util is 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)) diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index f40d142ec74..7a9e52d43aa 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -1729,7 +1729,7 @@ package body Sem_Ch3 is 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) @@ -2289,9 +2289,9 @@ package body Sem_Ch3 is 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 @@ -15335,7 +15335,7 @@ package body Sem_Ch3 is 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. diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index d67beeb0b10..53f6b42d7e5 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -17112,11 +17112,11 @@ package body Sem_Prag is 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,