OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

opt.ads (Warn_On_Suspicious_Contract): Update comment describing use. 

2015-02-05  Yannick Moy  <moy@adacore.com>

	* opt.ads (Warn_On_Suspicious_Contract): Update comment
	describing use.
	* sem_attr.adb (Analyze_Attribute/Attribute_Update): Warn on
	suspicious uses of 'Update.
	* sem_warn.adb, sem_warn.ads (Warn_On_Suspicious_Update): New
	function issues warning on suspicious uses of 'Update.
	* g-rannum.adb, g-rannum.ads, s-rannum.adb, s-rannum.ads: Mark
	package spec and body as SPARK_Mode Off.

From-SVN: r220444
This commit is contained in:
Yannick Moy 2015-02-05 11:13:41 +00:00 committed by Arnaud Charlet
parent e0709184ee
commit 71140fc6ca
9 changed files with 85 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
gcc/ada/ChangeLog
View File

@ -1,3 +1,14 @@
2015-02-05 Yannick Moy <moy@adacore.com>
* opt.ads (Warn_On_Suspicious_Contract): Update comment
describing use.
* sem_attr.adb (Analyze_Attribute/Attribute_Update): Warn on
suspicious uses of 'Update.
* sem_warn.adb, sem_warn.ads (Warn_On_Suspicious_Update): New
function issues warning on suspicious uses of 'Update.
* g-rannum.adb, g-rannum.ads, s-rannum.adb, s-rannum.ads: Mark
package spec and body as SPARK_Mode Off.
2015-02-05 Robert Dewar <dewar@adacore.com>
* sem_prag.adb (Set_Elab_Unit_Name): New name for Set_Unit_Name

6
gcc/ada/g-rannum.adb
View File

@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2007-2013, Free Software Foundation, Inc. --
-- Copyright (C) 2007-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- --
@ -35,7 +35,9 @@ with Ada.Unchecked_Conversion;
with System.Random_Numbers; use System.Random_Numbers;
package body GNAT.Random_Numbers is
package body GNAT.Random_Numbers with
SPARK_Mode => Off
is
Sys_Max_Image_Width : constant := System.Random_Numbers.Max_Image_Width;

10
gcc/ada/g-rannum.ads
View File

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2007-2013, Free Software Foundation, Inc. --
-- Copyright (C) 2007-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- --
@ -47,10 +47,16 @@
-- Generator type itself suffices for this purpose. The parameter modes on
-- Reset procedures better reflect the effect of these routines.
-- Note: this package is marked SPARK_Mode Off, because functions Random work
-- by side-effect to change the value of the generator, hence they should not
-- be called from SPARK code.
with System.Random_Numbers;
with Interfaces; use Interfaces;
package GNAT.Random_Numbers is
package GNAT.Random_Numbers with
SPARK_Mode => Off
is
type Generator is limited private;
subtype Initialization_Vector is

6
gcc/ada/opt.ads
View File

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 1992-2014, 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- --
@ -1759,7 +1759,9 @@ package Opt is
Warn_On_Suspicious_Contract : Boolean := True;
-- GNAT
-- Set to True to generate warnings for suspicious contracts expressed as
-- pragmas or aspects precondition and postcondition. The default is that
-- pragmas or aspects precondition and postcondition, as well as other
-- suspicious cases of expressions typically found in contracts like
-- quantified expressions and uses of Update attribute. The default is that
-- this warning is enabled. Modified by use of -gnatw.t/.T.
Warn_On_Suspicious_Modulus_Value : Boolean := True;

6
gcc/ada/s-rannum.adb
View File

@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2007-2014, Free Software Foundation, Inc. --
-- Copyright (C) 2007-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- --
@ -94,7 +94,9 @@ with Interfaces; use Interfaces;
use Ada;
package body System.Random_Numbers is
package body System.Random_Numbers with
SPARK_Mode => Off
is
Image_Numeral_Length : constant := Max_Image_Width / N;
subtype Image_String is String (1 .. Max_Image_Width);

10
gcc/ada/s-rannum.ads
View File

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2007-2013, Free Software Foundation, Inc. --
-- Copyright (C) 2007-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- --
@ -51,9 +51,15 @@
-- standard random-number packages Ada.Numerics.Float_Random and
-- Ada.Numerics.Discrete_Random.
-- Note: this package is marked SPARK_Mode Off, because functions Random work
-- by side-effect to change the value of the generator, hence they should not
-- be called from SPARK code.
with Interfaces;
package System.Random_Numbers is
package System.Random_Numbers with
SPARK_Mode => Off
is
type Generator is limited private;
-- Generator encodes the current state of a random number stream, it is

3
gcc/ada/sem_attr.adb
View File

@ -62,6 +62,7 @@ with Sem_Eval; use Sem_Eval;
with Sem_Res; use Sem_Res;
with Sem_Type; use Sem_Type;
with Sem_Util; use Sem_Util;
with Sem_Warn;
with Stand; use Stand;
with Sinfo; use Sinfo;
with Sinput; use Sinput;
@ -6441,6 +6442,8 @@ package body Sem_Attr is
-- The type of attribute 'Update is that of the prefix
Set_Etype (N, P_Type);
Sem_Warn.Warn_On_Suspicious_Update (N);
end Update;
---------

34
gcc/ada/sem_warn.adb
View File

@ -3930,6 +3930,40 @@ package body Sem_Warn is
end if;
end Warn_On_Suspicious_Index;
-------------------------------
-- Warn_On_Suspicious_Update --
-------------------------------
procedure Warn_On_Suspicious_Update (N : Node_Id) is
Par : constant Node_Id := Parent (N);
Arg : Node_Id;
begin
-- Only process if warnings activated
if Warn_On_Suspicious_Contract then
if Nkind_In (Par, N_Op_Eq, N_Op_Ne) then
if N = Left_Opnd (Par) then
Arg := Right_Opnd (Par);
else
Arg := Left_Opnd (Par);
end if;
if Same_Object (Prefix (N), Arg) then
if Nkind (Par) = N_Op_Eq then
Error_Msg_N
("suspicious equality test with modified version of "
& "same object?T?", Par);
else
Error_Msg_N
("suspicious inequality test with modified version of "
& "same object?T?", Par);
end if;
end if;
end if;
end if;
end Warn_On_Suspicious_Update;
--------------------------------------
-- Warn_On_Unassigned_Out_Parameter --
--------------------------------------

10
gcc/ada/sem_warn.ads
View File

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 1999-2014, Free Software Foundation, Inc. --
-- Copyright (C) 1999-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- --
@ -214,6 +214,14 @@ package Sem_Warn is
-- a warning is generated that the subscripting operation is possibly
-- incorrectly assuming a lower bound of 1.
procedure Warn_On_Suspicious_Update (N : Node_Id);
-- N is a semantically analyzed attribute reference Prefix'Update. Issue
-- a warning if Warn_On_Suspicious_Contract is set, and N is the left-hand
-- side or right-hand side of an equality or disequality of the form:
-- Prefix = Prefix'Update(...)
-- or
-- Prefix'Update(...) = Prefix
procedure Warn_On_Unassigned_Out_Parameter
(Return_Node : Node_Id;
Scope_Id : Entity_Id);