| 1425 | #if defined(MAIN_zip) |
| 1426 | #define BLOCKSIZE 65536u |
| 1427 | int main() |
| 1428 | { |
| 1429 | const char fn[] = "recup_dir.1/f0000000.zip"; |
| 1430 | unsigned char buffer[BLOCKSIZE]; |
| 1431 | file_recovery_t file_recovery_new; |
| 1432 | file_recovery_t file_recovery; |
| 1433 | file_stat_t file_stats; |
| 1434 | |
| 1435 | /*@ assert \valid(buffer + (0 .. (BLOCKSIZE - 1))); */ |
| 1436 | #if defined(__FRAMAC__) |
| 1437 | Frama_C_make_unknown((char *)buffer, BLOCKSIZE); |
| 1438 | #endif |
| 1439 | |
| 1440 | reset_file_recovery(&file_recovery); |
| 1441 | /*@ assert file_recovery.file_stat == \null; */ |
| 1442 | file_recovery.blocksize=BLOCKSIZE; |
| 1443 | file_recovery_new.blocksize=BLOCKSIZE; |
| 1444 | file_recovery_new.data_check=NULL; |
| 1445 | file_recovery_new.extension=NULL; |
| 1446 | file_recovery_new.file_stat=NULL; |
| 1447 | file_recovery_new.file_check=NULL; |
| 1448 | file_recovery_new.file_rename=NULL; |
| 1449 | file_recovery_new.calculated_file_size=0; |
| 1450 | file_recovery_new.file_size=0; |
| 1451 | file_recovery_new.location.start=0; |
| 1452 | |
| 1453 | file_stats.file_hint=&file_hint_zip; |
| 1454 | file_stats.not_recovered=0; |
| 1455 | file_stats.recovered=0; |
| 1456 | register_header_check_zip(&file_stats); |
| 1457 | if(header_check_zip(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1) |
| 1458 | return 0; |
| 1459 | /*@ assert valid_read_string(file_recovery_new.extension); */ |
| 1460 | /*@ assert valid_read_string((char *)&fn); */ |
| 1461 | memcpy(file_recovery_new.filename, fn, sizeof(fn)); |
| 1462 | file_recovery_new.file_stat=&file_stats; |
| 1463 | /*@ assert valid_read_string((char *)file_recovery_new.filename); */ |
| 1464 | /*@ assert file_recovery_new.min_filesize == 30; */ |
| 1465 | /*@ assert file_recovery_new.file_check == &file_check_zip || file_recovery_new.file_check == \null; */ |
| 1466 | /*@ assert file_recovery_new.file_stat->file_hint!=NULL; */ |
| 1467 | /*@ assert file_recovery_new.time == 0; */ |
| 1468 | { |
| 1469 | file_recovery_t file_recovery_new2; |
| 1470 | file_recovery_new2.blocksize=BLOCKSIZE; |
| 1471 | file_recovery_new2.file_stat=NULL; |
| 1472 | file_recovery_new2.file_check=NULL; |
| 1473 | file_recovery_new2.location.start=BLOCKSIZE; |
| 1474 | file_recovery_new.handle=NULL; /* In theory should be not null */ |
| 1475 | /*@ assert file_recovery_new.extension == file_hint_zip.extension || |
| 1476 | file_recovery_new.extension == extension_docx || |
| 1477 | file_recovery_new.extension == extension_epub || |
| 1478 | file_recovery_new.extension == extension_kra || |
| 1479 | file_recovery_new.extension == extension_numbers || |
| 1480 | file_recovery_new.extension == extension_odg || |
| 1481 | file_recovery_new.extension == extension_odp || |
| 1482 | file_recovery_new.extension == extension_ods || |
| 1483 | file_recovery_new.extension == extension_odt || |
| 1484 | file_recovery_new.extension == extension_ora || |
nothing calls this directly
no test coverage detected