@ @ requires buffer_size >= sizeof(struct ext2_super_block); @ requires separation: \separated(&file_hint_ext2_fs, buffer+(..), file_recovery, file_recovery_new); @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new); @ ensures valid_header_check_result(\result, file_recovery_new); @*/
| 52 | @ ensures valid_header_check_result(\result, file_recovery_new); |
| 53 | @*/ |
| 54 | static int header_check_ext2_fs(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new) |
| 55 | { |
| 56 | const struct ext2_super_block *sb=(const struct ext2_super_block *)&buffer[0x400]; |
| 57 | if(test_EXT2(sb, NULL)!=0) |
| 58 | return 0; |
| 59 | /*@ assert le32(sb->s_log_block_size) <= 6; */ |
| 60 | if(le16(sb->s_block_group_nr)!=0) |
| 61 | return 0; |
| 62 | if(file_recovery->file_stat!=NULL && |
| 63 | file_recovery->file_stat->file_hint==&file_hint_ext2_fs && |
| 64 | file_recovery->calculated_file_size==(uint64_t)le32(sb->s_blocks_count)*(EXT2_MIN_BLOCK_SIZE<<le32(sb->s_log_block_size))) |
| 65 | { |
| 66 | if(header_ignored_adv(file_recovery, file_recovery_new)==0) |
| 67 | return 0; |
| 68 | } |
| 69 | reset_file_recovery(file_recovery_new); |
| 70 | file_recovery_new->extension=file_hint_ext2_fs.extension; |
| 71 | file_recovery_new->calculated_file_size=(uint64_t)le32(sb->s_blocks_count)*(EXT2_MIN_BLOCK_SIZE<<le32(sb->s_log_block_size)); |
| 72 | file_recovery_new->data_check=&data_check_size; |
| 73 | file_recovery_new->file_check=&file_check_size; |
| 74 | return 1; |
| 75 | } |
| 76 | |
| 77 | static void register_header_check_ext2_fs(file_stat_t *file_stat) |
| 78 | { |
nothing calls this directly
no test coverage detected