| method | String doTable(String[], String[][]) |
| pre | data != null |
| pre | data.length <= 232-1 |
| pre | headers != null |
| pre | (soft) data[...] != null |
| pre | (soft) data[...].length in {1..232-1} |
| pre | (soft) data[...].length - headers.length in {0..232-2} |
| pre | (soft) data[...][...] != null |
| pre | (soft) headers.length in {1..232-1} |
| pre | (soft) headers[...] != null |
| presumption | java.lang.String:length(...)@87 <= 232-4 |
| presumption | java.lang.String:length(...)@90 <= 232-4 |
| post | init'ed(java.lang.StringBuilder:toString(...)._ tainted) |
| post | return_value == &java.lang.StringBuilder:toStri ng(...) |
| unanalyzed | call on java.lang.String:length |