SocketState.java |
| current inspection = 2009-09-03 21:56:13 (id #1) |
|
|
| Kind | Annotation Text |
|---|
| Kind | Annotation Text |
|---|---|
| post | $VALUES == &new SocketState[]( |
| post | $VALUES.length == 3 |
| post | $VALUES[0] == &new SocketState( |
| post | $VALUES[1] == &new SocketState( |
| post | $VALUES[2] == &new SocketState( |
| post | CLOSED == &new SocketState( |
| post | NULL == &new SocketState( |
| post | OPEN == &new SocketState( |
| post | new SocketState( |
| post | new SocketState( |
| post | new SocketState( |
| post | new SocketState[]( |
| unanalyzed | call on java. |
| Kind | Annotation Text |
|---|---|
| post | init'ed(return_value) |
| Kind | Annotation Text |
|---|---|
| pre | (soft) init'ed( |
| post | new SocketState[]( |
| post | return_value == &new SocketState[]( |
| post | return_value. |
| post | return_value[. |