@ @ requires \valid(file); @ requires \valid_read(fat + (0 .. fat_entries-1)); @ requires \valid_read(header); @ requires 9 == le16(header->uSectorShift) || 12 == le16(header->uSectorShift); @ requires 6 == le16(header->uMiniSectorShift); @ requires \valid(ext); @ requires \valid(title + (0 .. 1024-1)); @ requires \valid(file_time); @ requires *ext == \null || valid_read_string(*
| 1471 | @ ensures valid_string(title); |
| 1472 | @*/ |
| 1473 | static void OLE_parse_summary(FILE *file, const uint32_t *fat, const unsigned int fat_entries, |
| 1474 | const struct OLE_HDR *header, const unsigned int ministream_block, const unsigned int ministream_size, |
| 1475 | const unsigned int block, const unsigned int len, const char **ext, char *title, time_t *file_time, |
| 1476 | const uint64_t offset) |
| 1477 | { |
| 1478 | const unsigned int uSectorShift=le16(header->uSectorShift); |
| 1479 | /*@ assert 9 == uSectorShift || 12 == uSectorShift; */ |
| 1480 | char *summary=NULL; |
| 1481 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1482 | /*@ assert valid_string(title); */ |
| 1483 | if(len < 48 || len>1024*1024) |
| 1484 | { |
| 1485 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1486 | /*@ assert valid_string(title); */ |
| 1487 | return ; |
| 1488 | } |
| 1489 | /*@ assert 48 <= len <= 1024*1024; */ |
| 1490 | if(len < le32(header->miniSectorCutoff)) |
| 1491 | { |
| 1492 | if(le32(header->csectMiniFat)==0 || ministream_size == 0) |
| 1493 | { |
| 1494 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1495 | /*@ assert valid_string(title); */ |
| 1496 | return ; |
| 1497 | } |
| 1498 | if(ministream_size > 1024*1024 || le32(header->csectMiniFat) > 2048) |
| 1499 | { |
| 1500 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1501 | /*@ assert valid_string(title); */ |
| 1502 | return ; |
| 1503 | } |
| 1504 | /*@ assert 0 < le32(header->csectMiniFat) <= 2048; */ |
| 1505 | /*@ assert 9 == uSectorShift || 12 == uSectorShift; */ |
| 1506 | { |
| 1507 | const unsigned int mini_fat_entries=(le32(header->csectMiniFat) << uSectorShift) / 4; |
| 1508 | uint32_t *minifat; |
| 1509 | unsigned char *ministream; |
| 1510 | if((minifat=OLE_load_MiniFAT(file, header, fat, fat_entries, offset))==NULL) |
| 1511 | { |
| 1512 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1513 | /*@ assert valid_string(title); */ |
| 1514 | return ; |
| 1515 | } |
| 1516 | /*@ assert \initialized((char *)minifat + (0 .. (le32(header->csectMiniFat) << le16(header->uSectorShift)) - 1)); */ |
| 1517 | ministream=(unsigned char *)OLE_read_stream(file, |
| 1518 | fat, fat_entries, uSectorShift, |
| 1519 | ministream_block, ministream_size, offset); |
| 1520 | if(ministream != NULL) |
| 1521 | { |
| 1522 | summary=(char*)OLE_read_ministream(ministream, |
| 1523 | minifat, mini_fat_entries, le16(header->uMiniSectorShift), |
| 1524 | block, len, ministream_size); |
| 1525 | /*@ assert summary == \null || \initialized(summary + (0 .. len-1)); */ |
| 1526 | free(ministream); |
| 1527 | } |
| 1528 | free(minifat); |
| 1529 | } |
| 1530 | } |
no test coverage detected