From 71140fc6ca792f3666e126b5eec4640193741ae2 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Thu, 5 Feb 2015 11:13:41 +0000 Subject: [PATCH] opt.ads (Warn_On_Suspicious_Contract): Update comment describing use. 2015-02-05 Yannick Moy * 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 --- gcc/ada/ChangeLog | 11 +++++++++++ gcc/ada/g-rannum.adb | 6 ++++-- gcc/ada/g-rannum.ads | 10 ++++++++-- gcc/ada/opt.ads | 6 ++++-- gcc/ada/s-rannum.adb | 6 ++++-- gcc/ada/s-rannum.ads | 10 ++++++++-- gcc/ada/sem_attr.adb | 3 +++ gcc/ada/sem_warn.adb | 34 ++++++++++++++++++++++++++++++++++ gcc/ada/sem_warn.ads | 10 +++++++++- 9 files changed, 85 insertions(+), 11 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f6c096b1d48..7ad5878c342 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,14 @@ +2015-02-05 Yannick Moy + + * 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 * sem_prag.adb (Set_Elab_Unit_Name): New name for Set_Unit_Name diff --git a/gcc/ada/g-rannum.adb b/gcc/ada/g-rannum.adb index a868f08123e..39e92e19a31 100644 --- a/gcc/ada/g-rannum.adb +++ b/gcc/ada/g-rannum.adb @@ -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; diff --git a/gcc/ada/g-rannum.ads b/gcc/ada/g-rannum.ads index 010c21c6cde..8eadf669a2b 100644 --- a/gcc/ada/g-rannum.ads +++ b/gcc/ada/g-rannum.ads @@ -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 diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index e30af5c9cc4..ceaefd91d32 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -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; diff --git a/gcc/ada/s-rannum.adb b/gcc/ada/s-rannum.adb index af620d70420..e31a2dca36e 100644 --- a/gcc/ada/s-rannum.adb +++ b/gcc/ada/s-rannum.adb @@ -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); diff --git a/gcc/ada/s-rannum.ads b/gcc/ada/s-rannum.ads index a412b9c85c9..8331c039c5c 100644 --- a/gcc/ada/s-rannum.ads +++ b/gcc/ada/s-rannum.ads @@ -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 diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 8ce79d80588..3ec6e73003e 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -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; --------- diff --git a/gcc/ada/sem_warn.adb b/gcc/ada/sem_warn.adb index f0e0ec6ca1d..4cbea2a6ba8 100644 --- a/gcc/ada/sem_warn.adb +++ b/gcc/ada/sem_warn.adb @@ -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 -- -------------------------------------- diff --git a/gcc/ada/sem_warn.ads b/gcc/ada/sem_warn.ads index 41c5a22e3e9..c441f28b889 100644 --- a/gcc/ada/sem_warn.ads +++ b/gcc/ada/sem_warn.ads @@ -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); -- 2.30.2