| <html> | |
| <body> | |
| Reports any calls to | |
| <b>java.util.Random.getDouble()</b> which are then multiplied | |
| by some factor and cast to an integer. For generating a random integer in some range, | |
| <b>java.util.Random.getInt()</b> is more efficient. | |
| <!-- tooltip end --> | |
| <p> | |
| </body> | |
| </html> |