MediaSourceComparator.java |
| current inspection = 2009-09-03 21:56:13 (id #1) |
|
|
| Kind | Annotation Text |
|---|---|
| post | init'ed(this.order) |
| post | this.order == order |
| Kind | Annotation Text |
|---|
| Kind | Annotation Text |
|---|---|
| pre | o1 != null |
| pre | o2 != null |
| pre | this.order != null |
| presumption | java.util. |
| post | init'ed(return_value) |
| unanalyzed | call on getAppName |
| unanalyzed | call on java. |
| unanalyzed | call on java. |
| unanalyzed | call on java. |
| Kind | Annotation Text |
|---|---|
| pre | this.order != null |
| pre | x0 != null |
| pre | x1 != null |
| post | return_value == 0 |
| unanalyzed | call on getAppName |
| unanalyzed | call on java. |
| unanalyzed | call on java. |
| unanalyzed | call on java. |
| Kind | Annotation Text |
|---|---|
| pre | source != null |
| pre | this.order != null |
| post | init'ed(return_value) |
| test_vector | java.util. |