@ @ requires 8 <= size <= 1024*1024; @ requires \valid_read(buffer+ (0 .. size-1)); @ requires \initialized(buffer+ (0 .. size-1)); @ requires \valid(ext); @ requires \valid(title + (0 .. 1024-1)); @ requires \valid(file_time); @ requires valid_string(title); @ requires *ext == \null || valid_read_string(*ext); @ requires separation: \separated(buffer+(..), ext, title + (0 .. 102
| 1254 | @ assigns *ext, *(title + (0..1023)), *file_time; |
| 1255 | @*/ |
| 1256 | static void OLE_parse_PropertySet(const char *buffer, const unsigned int size, const char **ext, char *title, time_t *file_time) |
| 1257 | { |
| 1258 | const struct summary_entry *entries=(const struct summary_entry *)&buffer[8]; |
| 1259 | const unsigned int numEntries=get32u(buffer, 4); |
| 1260 | unsigned int i; |
| 1261 | #ifdef DEBUG_OLE |
| 1262 | log_info("Property Info %u entries - %u bytes\n", numEntries, size); |
| 1263 | #endif |
| 1264 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1265 | /*@ assert valid_string(title); */ |
| 1266 | if(numEntries == 0 || numEntries > 1024*1024) |
| 1267 | { |
| 1268 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1269 | /*@ assert valid_string(title); */ |
| 1270 | return ; |
| 1271 | } |
| 1272 | /*@ assert 0 < numEntries <= 1024*1024; */ |
| 1273 | if(8 + numEntries * 8 > size) |
| 1274 | { |
| 1275 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1276 | /*@ assert valid_string(title); */ |
| 1277 | return ; |
| 1278 | } |
| 1279 | /*@ assert 8 + numEntries * 8 <= size; */ |
| 1280 | /*@ assert numEntries * 8 <= size - 8; */ |
| 1281 | /*@ assert numEntries < size/8; */ |
| 1282 | if((const char *)&entries[numEntries] > &buffer[size]) |
| 1283 | { |
| 1284 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1285 | /*@ assert valid_string(title); */ |
| 1286 | return ; |
| 1287 | } |
| 1288 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1289 | /*@ assert valid_string(title); */ |
| 1290 | /*@ assert \valid_read(buffer + (0 .. size - 1)); */ |
| 1291 | /*@ assert \valid_read((buffer+8) + (8 .. size - 8 - 1)); */ |
| 1292 | /*@ |
| 1293 | @ loop invariant *ext == \null || valid_read_string(*ext); |
| 1294 | @ loop invariant valid_string(title); |
| 1295 | @ loop invariant 0 <= i <= numEntries; |
| 1296 | @ loop assigns i, *ext, *(title + (0..1023)), *file_time; |
| 1297 | @ loop variant numEntries-i; |
| 1298 | @*/ |
| 1299 | for(i=0; i<numEntries; i++) |
| 1300 | { |
| 1301 | const struct summary_entry *entry; |
| 1302 | const unsigned int entry_offset=8+8*i; |
| 1303 | const char *entry_ptr; |
| 1304 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1305 | /*@ assert valid_string(title); */ |
| 1306 | if(entry_offset + 8 > size) |
| 1307 | { |
| 1308 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1309 | /*@ assert valid_string(title); */ |
| 1310 | return ; |
| 1311 | } |
| 1312 | /*@ assert entry_offset + 8 <= size; */ |
| 1313 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
no test coverage detected