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

9 files changed, 85 insertions, 11 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index f6c096b1..7ad5878 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -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
diff --git a/gcc/ada/g-rannum.adb b/gcc/ada/g-rannum.adb
index a868f08..39e92e1 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 010c21c..8eadf66 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 e30af5c..ceaefd9 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 af620d7..e31a2dc 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 a412b9c..8331c03 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 8ce79d8..3ec6e73 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 f0e0ec6..4cbea2a 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 41c5a22..c441f28 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);