diff options
| author | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2015-02-05 11:13:41 +0000 |
|---|---|---|
| committer | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2015-02-05 11:13:41 +0000 |
| commit | 258a7f5c0f045b4c7e4fed79b83a0a5eca8631d6 (patch) | |
| tree | b79045467ca5b8321023c258eb4ade468927b1d0 /gcc/ada/s-rannum.ads | |
| parent | 2271bce4dea8b55959c615d2bb55e91340c79da9 (diff) | |
| download | gcc-258a7f5c0f045b4c7e4fed79b83a0a5eca8631d6.tar.gz | |
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.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@220444 138bc75d-0d04-0410-961f-82ee72b054a4
Diffstat (limited to 'gcc/ada/s-rannum.ads')
| -rw-r--r-- | gcc/ada/s-rannum.ads | 10 |
1 files changed, 8 insertions, 2 deletions
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 |