andersk / splint.git / blame
| Commit | Line | Data |
|---|---|---|
| 885824d3 | 1 | extern unknown (int *x); |
| 2 | extern inparam (/*@in@*/ int *x); | |
| 3 | ||
| 4 | void f (/*@out@*/ int *x) | |
| 5 | { | |
| 6 | if (3 > 4) | |
| 7 | { | |
| 15b3d2b2 | 8 | unknown (x); /* x not completely defined */ |
| 885824d3 | 9 | } |
| 10 | else | |
| 11 | { | |
| 15b3d2b2 | 12 | inparam (x); /* x not completely defined */ |
| 885824d3 | 13 | } |
| 14 | } |