move struct ext2_super_block from src/ext2.h to src/ext2_common.h

This commit is contained in:
Christophe Grenier 2021-01-29 22:53:48 +01:00
parent 0c59aa8d22
commit 90e8f7414d
13 changed files with 268 additions and 185 deletions

View file

@ -34,7 +34,6 @@
#include "types.h" #include "types.h"
#include "common.h" #include "common.h"
#include "ext2.h" #include "ext2.h"
#include "ext2_common.h"
#include "fnctdsk.h" #include "fnctdsk.h"
#include "log.h" #include "log.h"
#include "guid_cpy.h" #include "guid_cpy.h"

View file

@ -21,189 +21,25 @@
*/ */
#ifndef _EXT2_H #ifndef _EXT2_H
#define _EXT2_H #define _EXT2_H
#include "ext2_common.h"
#ifdef __cplusplus #ifdef __cplusplus
extern "C" { extern "C" {
#endif #endif
/*@
@ requires \valid(disk_car);
@ requires valid_disk(disk_car);
@ requires \valid(partition);
@ requires \separated(disk_car, partition);
@*/
int check_EXT2(disk_t *disk_car, partition_t *partition, const int verbose);
#define EXT2_SUPERBLOCK_SIZE 1024 /*@
@ requires \valid(disk_car);
#define EXT2_SB(sb) (sb) @ requires valid_disk(disk_car);
@ requires \valid_read(sb);
/* @ requires \valid(partition);
* The second extended file system magic number @ requires \separated(disk_car, partition);
*/ @*/
#define EXT2_SUPER_MAGIC 0xEF53
#define EXT2_MIN_BLOCK_SIZE 1024
#define EXT2_MAX_BLOCK_SIZE 4096
#define EXT2_MIN_BLOCK_LOG_SIZE 10
#define EXT2_MIN_BLOCK (EXT2_MIN_BLOCK_SIZE/DEFAULT_SECTOR_SIZE)
/*
* File system states
*/
#define EXT2_VALID_FS 0x0001 /* Unmounted cleanly */
#define EXT2_ERROR_FS 0x0002 /* Errors detected */
/*
* Behaviour when detecting errors
*/
#define EXT2_ERRORS_CONTINUE 1 /* Continue execution */
#define EXT2_ERRORS_RO 2 /* Remount fs read-only */
#define EXT2_ERRORS_PANIC 3 /* Panic */
#define EXT2_ERRORS_DEFAULT EXT2_ERRORS_CONTINUE
/*
* Feature set definitions
*/
#define EXT2_HAS_COMPAT_FEATURE(sb,mask) \
( le32(EXT2_SB(sb)->s_feature_compat) & (mask) )
#define EXT2_HAS_RO_COMPAT_FEATURE(sb,mask) \
( le32(EXT2_SB(sb)->s_feature_ro_compat) & (mask) )
#define EXT2_HAS_INCOMPAT_FEATURE(sb,mask) \
( le32(EXT2_SB(sb)->s_feature_incompat) & (mask) )
#define EXT2_FEATURE_COMPAT_DIR_PREALLOC 0x0001
#define EXT2_FEATURE_COMPAT_IMAGIC_INODES 0x0002
#define EXT3_FEATURE_COMPAT_HAS_JOURNAL 0x0004
#define EXT2_FEATURE_COMPAT_EXT_ATTR 0x0008
#define EXT2_FEATURE_COMPAT_RESIZE_INO 0x0010
#define EXT2_FEATURE_COMPAT_DIR_INDEX 0x0020
#define EXT2_FEATURE_COMPAT_LAZY_BG 0x0040
#define EXT2_FEATURE_COMPAT_ANY 0xffffffff
#define EXT2_FEATURE_RO_COMPAT_SPARSE_SUPER 0x0001
#define EXT2_FEATURE_RO_COMPAT_LARGE_FILE 0x0002
//#define EXT2_FEATURE_RO_COMPAT_BTREE_DIR 0x0004
#define EXT4_FEATURE_RO_COMPAT_HUGE_FILE 0x0008
#define EXT4_FEATURE_RO_COMPAT_GDT_CSUM 0x0010
#define EXT4_FEATURE_RO_COMPAT_DIR_NLINK 0x0020
#define EXT4_FEATURE_RO_COMPAT_EXTRA_ISIZE 0x0040
#define EXT2_FEATURE_RO_COMPAT_ANY 0xffffffff
#define EXT2_FEATURE_INCOMPAT_COMPRESSION 0x0001
#define EXT2_FEATURE_INCOMPAT_FILETYPE 0x0002
#define EXT3_FEATURE_INCOMPAT_RECOVER 0x0004
#define EXT3_FEATURE_INCOMPAT_JOURNAL_DEV 0x0008
#define EXT2_FEATURE_INCOMPAT_META_BG 0x0010
#define EXT3_FEATURE_INCOMPAT_EXTENTS 0x0040
#define EXT4_FEATURE_INCOMPAT_64BIT 0x0080
#define EXT4_FEATURE_INCOMPAT_MMP 0x0100
#define EXT2_FEATURE_INCOMPAT_ANY 0xffffffff
/*
* Structure of the super block
*/
struct ext2_super_block {
uint32_t s_inodes_count; /* Inodes count */
uint32_t s_blocks_count; /* Blocks count */
uint32_t s_r_blocks_count; /* Reserved blocks count */
uint32_t s_free_blocks_count; /* Free blocks count */
uint32_t s_free_inodes_count; /* Free inodes count */
uint32_t s_first_data_block; /* First Data Block */
uint32_t s_log_block_size; /* Block size */
int32_t s_log_frag_size; /* Fragment size */
uint32_t s_blocks_per_group; /* # Blocks per group */
uint32_t s_frags_per_group; /* # Fragments per group */
uint32_t s_inodes_per_group; /* # Inodes per group */
uint32_t s_mtime; /* Mount time */
uint32_t s_wtime; /* Write time */
uint16_t s_mnt_count; /* Mount count */
int16_t s_max_mnt_count; /* Maximal mount count */
uint16_t s_magic; /* Magic signature */
uint16_t s_state; /* File system state */
uint16_t s_errors; /* Behaviour when detecting errors */
uint16_t s_minor_rev_level; /* minor revision level */
uint32_t s_lastcheck; /* time of last check */
uint32_t s_checkinterval; /* max. time between checks */
uint32_t s_creator_os; /* OS */
uint32_t s_rev_level; /* Revision level */
uint16_t s_def_resuid; /* Default uid for reserved blocks */
uint16_t s_def_resgid; /* Default gid for reserved blocks */
/*
* These fields are for EXT2_DYNAMIC_REV superblocks only.
*
* Note: the difference between the compatible feature set and
* the incompatible feature set is that if there is a bit set
* in the incompatible feature set that the kernel doesn't
* know about, it should refuse to mount the filesystem.
*
* e2fsck's requirements are more strict; if it doesn't know
* about a feature in either the compatible or incompatible
* feature set, it must abort and not try to meddle with
* things it doesn't understand...
*/
uint32_t s_first_ino; /* First non-reserved inode */
uint16_t s_inode_size; /* size of inode structure */
uint16_t s_block_group_nr; /* block group # of this superblock */
uint32_t s_feature_compat; /* compatible feature set */
uint32_t s_feature_incompat; /* incompatible feature set */
uint32_t s_feature_ro_compat; /* readonly-compatible feature set */
uint8_t s_uuid[16]; /* 128-bit uuid for volume */
char s_volume_name[16]; /* volume name */
char s_last_mounted[64]; /* directory where last mounted */
uint32_t s_algorithm_usage_bitmap; /* For compression */
/*
* Performance hints. Directory preallocation should only
* happen if the EXT2_COMPAT_PREALLOC flag is on.
*/
uint8_t s_prealloc_blocks; /* Nr of blocks to try to preallocate*/
uint8_t s_prealloc_dir_blocks; /* Nr to preallocate for dirs */
uint16_t s_reserved_gdt_blocks; /* Per group table for online growth */
/*
* Journaling support valid if EXT2_FEATURE_COMPAT_HAS_JOURNAL set.
*/
uint8_t s_journal_uuid[16]; /* uuid of journal superblock */
uint32_t s_journal_inum; /* inode number of journal file */
uint32_t s_journal_dev; /* device number of journal file */
uint32_t s_last_orphan; /* start of list of inodes to delete */
uint32_t s_hash_seed[4]; /* HTREE hash seed */
uint8_t s_def_hash_version; /* Default hash version to use */
uint8_t s_jnl_backup_type; /* Default type of journal backup */
uint16_t s_desc_size; /* Group desc. size: INCOMPAT_64BIT */
uint32_t s_default_mount_opts;
uint32_t s_first_meta_bg; /* First metablock group */
uint32_t s_mkfs_time; /* When the filesystem was created */
uint32_t s_jnl_blocks[17]; /* Backup of the journal inode */
uint32_t s_blocks_count_hi; /* Blocks count high 32bits */
uint32_t s_r_blocks_count_hi; /* Reserved blocks count high 32 bits*/
uint32_t s_free_blocks_hi; /* Free blocks count */
uint16_t s_min_extra_isize; /* All inodes have at least # bytes */
uint16_t s_want_extra_isize; /* New inodes should reserve # bytes */
uint32_t s_flags; /* Miscellaneous flags */
uint16_t s_raid_stride; /* RAID stride */
uint16_t s_mmp_update_interval; /* # seconds to wait in MMP checking */
uint64_t s_mmp_block; /* Block for multi-mount protection */
uint32_t s_raid_stripe_width; /* blocks on all data disks (N*stride)*/
uint8_t s_log_groups_per_flex; /* FLEX_BG group size */
uint8_t s_reserved_char_pad;
uint16_t s_reserved_pad; /* Padding to next 32bits */
uint64_t s_kbytes_written; /* nr of lifetime kilobytes written */
uint32_t s_snapshot_inum; /* Inode number of active snapshot */
uint32_t s_snapshot_id; /* sequential ID of active snapshot */
uint64_t s_snapshot_r_blocks_count; /* reserved blocks for active
snapshot's future use */
uint32_t s_snapshot_list; /* inode number of the head of the on-disk snapshot list */
uint32_t s_error_count; /* number of fs errors */
uint32_t s_first_error_time; /* first time an error happened */
uint32_t s_first_error_ino; /* inode involved in first error */
uint64_t s_first_error_block; /* block involved of first error */
uint8_t s_first_error_func[32]; /* function where the error happened */
uint32_t s_first_error_line; /* line number where error happened */
uint32_t s_last_error_time; /* most recent time of an error */
uint32_t s_last_error_ino; /* inode involved in last error */
uint32_t s_last_error_line; /* line number where error happened */
uint64_t s_last_error_block; /* block involved of last error */
uint8_t s_last_error_func[32]; /* function where the error happened */
uint8_t s_mount_opts[64];
uint32_t s_usr_quota_inum; /* inode number of user quota file */
uint32_t s_grp_quota_inum; /* inode number of group quota file */
uint32_t s_overhead_blocks; /* overhead blocks/clusters in fs */
uint32_t s_reserved[108]; /* Padding to the end of the block */
uint32_t s_checksum; /* crc32c(superblock) */
};
int check_EXT2(disk_t *disk_car,partition_t *partition,const int verbose);
int recover_EXT2(const disk_t *disk_car, const struct ext2_super_block *sb, partition_t *partition, const int verbose, const int dump_ind); int recover_EXT2(const disk_t *disk_car, const struct ext2_super_block *sb, partition_t *partition, const int verbose, const int dump_ind);
#ifdef __cplusplus #ifdef __cplusplus

View file

@ -32,7 +32,6 @@
#endif #endif
#include "types.h" #include "types.h"
#include "common.h" #include "common.h"
#include "ext2.h"
#include "ext2_common.h" #include "ext2_common.h"
uint64_t td_ext2fs_blocks_count(const struct ext2_super_block *super) uint64_t td_ext2fs_blocks_count(const struct ext2_super_block *super)

View file

@ -25,8 +25,205 @@
extern "C" { extern "C" {
#endif #endif
#define EXT2_SUPERBLOCK_SIZE 1024
#define EXT2_SB(sb) (sb)
/*
* The second extended file system magic number
*/
#define EXT2_SUPER_MAGIC 0xEF53
#define EXT2_MIN_BLOCK_SIZE 1024
#define EXT2_MAX_BLOCK_SIZE 4096
#define EXT2_MIN_BLOCK_LOG_SIZE 10
#define EXT2_MIN_BLOCK (EXT2_MIN_BLOCK_SIZE/DEFAULT_SECTOR_SIZE)
/*
* File system states
*/
#define EXT2_VALID_FS 0x0001 /* Unmounted cleanly */
#define EXT2_ERROR_FS 0x0002 /* Errors detected */
/*
* Behaviour when detecting errors
*/
#define EXT2_ERRORS_CONTINUE 1 /* Continue execution */
#define EXT2_ERRORS_RO 2 /* Remount fs read-only */
#define EXT2_ERRORS_PANIC 3 /* Panic */
#define EXT2_ERRORS_DEFAULT EXT2_ERRORS_CONTINUE
/*
* Feature set definitions
*/
#define EXT2_HAS_COMPAT_FEATURE(sb,mask) \
( le32(EXT2_SB(sb)->s_feature_compat) & (mask) )
#define EXT2_HAS_RO_COMPAT_FEATURE(sb,mask) \
( le32(EXT2_SB(sb)->s_feature_ro_compat) & (mask) )
#define EXT2_HAS_INCOMPAT_FEATURE(sb,mask) \
( le32(EXT2_SB(sb)->s_feature_incompat) & (mask) )
#define EXT2_FEATURE_COMPAT_DIR_PREALLOC 0x0001
#define EXT2_FEATURE_COMPAT_IMAGIC_INODES 0x0002
#define EXT3_FEATURE_COMPAT_HAS_JOURNAL 0x0004
#define EXT2_FEATURE_COMPAT_EXT_ATTR 0x0008
#define EXT2_FEATURE_COMPAT_RESIZE_INO 0x0010
#define EXT2_FEATURE_COMPAT_DIR_INDEX 0x0020
#define EXT2_FEATURE_COMPAT_LAZY_BG 0x0040
#define EXT2_FEATURE_COMPAT_ANY 0xffffffff
#define EXT2_FEATURE_RO_COMPAT_SPARSE_SUPER 0x0001
#define EXT2_FEATURE_RO_COMPAT_LARGE_FILE 0x0002
//#define EXT2_FEATURE_RO_COMPAT_BTREE_DIR 0x0004
#define EXT4_FEATURE_RO_COMPAT_HUGE_FILE 0x0008
#define EXT4_FEATURE_RO_COMPAT_GDT_CSUM 0x0010
#define EXT4_FEATURE_RO_COMPAT_DIR_NLINK 0x0020
#define EXT4_FEATURE_RO_COMPAT_EXTRA_ISIZE 0x0040
#define EXT2_FEATURE_RO_COMPAT_ANY 0xffffffff
#define EXT2_FEATURE_INCOMPAT_COMPRESSION 0x0001
#define EXT2_FEATURE_INCOMPAT_FILETYPE 0x0002
#define EXT3_FEATURE_INCOMPAT_RECOVER 0x0004
#define EXT3_FEATURE_INCOMPAT_JOURNAL_DEV 0x0008
#define EXT2_FEATURE_INCOMPAT_META_BG 0x0010
#define EXT3_FEATURE_INCOMPAT_EXTENTS 0x0040
#define EXT4_FEATURE_INCOMPAT_64BIT 0x0080
#define EXT4_FEATURE_INCOMPAT_MMP 0x0100
#define EXT2_FEATURE_INCOMPAT_ANY 0xffffffff
/*
* Structure of the super block
*/
struct ext2_super_block {
uint32_t s_inodes_count; /* Inodes count */
uint32_t s_blocks_count; /* Blocks count */
uint32_t s_r_blocks_count; /* Reserved blocks count */
uint32_t s_free_blocks_count; /* Free blocks count */
uint32_t s_free_inodes_count; /* Free inodes count */
uint32_t s_first_data_block; /* First Data Block */
uint32_t s_log_block_size; /* Block size */
int32_t s_log_frag_size; /* Fragment size */
uint32_t s_blocks_per_group; /* # Blocks per group */
uint32_t s_frags_per_group; /* # Fragments per group */
uint32_t s_inodes_per_group; /* # Inodes per group */
uint32_t s_mtime; /* Mount time */
uint32_t s_wtime; /* Write time */
uint16_t s_mnt_count; /* Mount count */
int16_t s_max_mnt_count; /* Maximal mount count */
uint16_t s_magic; /* Magic signature */
uint16_t s_state; /* File system state */
uint16_t s_errors; /* Behaviour when detecting errors */
uint16_t s_minor_rev_level; /* minor revision level */
uint32_t s_lastcheck; /* time of last check */
uint32_t s_checkinterval; /* max. time between checks */
uint32_t s_creator_os; /* OS */
uint32_t s_rev_level; /* Revision level */
uint16_t s_def_resuid; /* Default uid for reserved blocks */
uint16_t s_def_resgid; /* Default gid for reserved blocks */
/*
* These fields are for EXT2_DYNAMIC_REV superblocks only.
*
* Note: the difference between the compatible feature set and
* the incompatible feature set is that if there is a bit set
* in the incompatible feature set that the kernel doesn't
* know about, it should refuse to mount the filesystem.
*
* e2fsck's requirements are more strict; if it doesn't know
* about a feature in either the compatible or incompatible
* feature set, it must abort and not try to meddle with
* things it doesn't understand...
*/
uint32_t s_first_ino; /* First non-reserved inode */
uint16_t s_inode_size; /* size of inode structure */
uint16_t s_block_group_nr; /* block group # of this superblock */
uint32_t s_feature_compat; /* compatible feature set */
uint32_t s_feature_incompat; /* incompatible feature set */
uint32_t s_feature_ro_compat; /* readonly-compatible feature set */
uint8_t s_uuid[16]; /* 128-bit uuid for volume */
char s_volume_name[16]; /* volume name */
char s_last_mounted[64]; /* directory where last mounted */
uint32_t s_algorithm_usage_bitmap; /* For compression */
/*
* Performance hints. Directory preallocation should only
* happen if the EXT2_COMPAT_PREALLOC flag is on.
*/
uint8_t s_prealloc_blocks; /* Nr of blocks to try to preallocate*/
uint8_t s_prealloc_dir_blocks; /* Nr to preallocate for dirs */
uint16_t s_reserved_gdt_blocks; /* Per group table for online growth */
/*
* Journaling support valid if EXT2_FEATURE_COMPAT_HAS_JOURNAL set.
*/
uint8_t s_journal_uuid[16]; /* uuid of journal superblock */
uint32_t s_journal_inum; /* inode number of journal file */
uint32_t s_journal_dev; /* device number of journal file */
uint32_t s_last_orphan; /* start of list of inodes to delete */
uint32_t s_hash_seed[4]; /* HTREE hash seed */
uint8_t s_def_hash_version; /* Default hash version to use */
uint8_t s_jnl_backup_type; /* Default type of journal backup */
uint16_t s_desc_size; /* Group desc. size: INCOMPAT_64BIT */
uint32_t s_default_mount_opts;
uint32_t s_first_meta_bg; /* First metablock group */
uint32_t s_mkfs_time; /* When the filesystem was created */
uint32_t s_jnl_blocks[17]; /* Backup of the journal inode */
uint32_t s_blocks_count_hi; /* Blocks count high 32bits */
uint32_t s_r_blocks_count_hi; /* Reserved blocks count high 32 bits*/
uint32_t s_free_blocks_hi; /* Free blocks count */
uint16_t s_min_extra_isize; /* All inodes have at least # bytes */
uint16_t s_want_extra_isize; /* New inodes should reserve # bytes */
uint32_t s_flags; /* Miscellaneous flags */
uint16_t s_raid_stride; /* RAID stride */
uint16_t s_mmp_update_interval; /* # seconds to wait in MMP checking */
uint64_t s_mmp_block; /* Block for multi-mount protection */
uint32_t s_raid_stripe_width; /* blocks on all data disks (N*stride)*/
uint8_t s_log_groups_per_flex; /* FLEX_BG group size */
uint8_t s_reserved_char_pad;
uint16_t s_reserved_pad; /* Padding to next 32bits */
uint64_t s_kbytes_written; /* nr of lifetime kilobytes written */
uint32_t s_snapshot_inum; /* Inode number of active snapshot */
uint32_t s_snapshot_id; /* sequential ID of active snapshot */
uint64_t s_snapshot_r_blocks_count; /* reserved blocks for active
snapshot's future use */
uint32_t s_snapshot_list; /* inode number of the head of the on-disk snapshot list */
uint32_t s_error_count; /* number of fs errors */
uint32_t s_first_error_time; /* first time an error happened */
uint32_t s_first_error_ino; /* inode involved in first error */
uint64_t s_first_error_block; /* block involved of first error */
uint8_t s_first_error_func[32]; /* function where the error happened */
uint32_t s_first_error_line; /* line number where error happened */
uint32_t s_last_error_time; /* most recent time of an error */
uint32_t s_last_error_ino; /* inode involved in last error */
uint32_t s_last_error_line; /* line number where error happened */
uint64_t s_last_error_block; /* block involved of last error */
uint8_t s_last_error_func[32]; /* function where the error happened */
uint8_t s_mount_opts[64];
uint32_t s_usr_quota_inum; /* inode number of user quota file */
uint32_t s_grp_quota_inum; /* inode number of group quota file */
uint32_t s_overhead_blocks; /* overhead blocks/clusters in fs */
uint32_t s_reserved[108]; /* Padding to the end of the block */
uint32_t s_checksum; /* crc32c(superblock) */
};
/*@
@ requires \valid_read(super);
@ assigns \nothing;
@*/
uint64_t td_ext2fs_blocks_count(const struct ext2_super_block *super); uint64_t td_ext2fs_blocks_count(const struct ext2_super_block *super);
/*@
@ requires \valid_read(super);
@ assigns \nothing;
@*/
uint64_t td_ext2fs_free_blocks_count(const struct ext2_super_block *super); uint64_t td_ext2fs_free_blocks_count(const struct ext2_super_block *super);
/*@
@ requires \valid_read(sb);
@ requires partition==\null || (\valid_read(partition) && valid_partition(partition));
@ requires \separated(sb, partition);
@ assigns \nothing;
@ ensures \result == 7 ==> le32(sb->s_log_block_size) > 6;
@ ensures \result == 0 ==> le32(sb->s_log_block_size) < 32;
@ */
int test_EXT2(const struct ext2_super_block *sb, const partition_t *partition); int test_EXT2(const struct ext2_super_block *sb, const partition_t *partition);
#ifdef __cplusplus #ifdef __cplusplus

View file

@ -25,7 +25,14 @@
extern "C" { extern "C" {
#endif #endif
/*@
@ requires \valid(disk_car);
@ requires valid_disk(disk_car);
@ requires \valid_read(partition);
@*/
dir_partition_t dir_partition_ext2_init(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const int verbose); dir_partition_t dir_partition_ext2_init(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const int verbose);
/*@ assigns \nothing; */
const char*td_ext2fs_version(void); const char*td_ext2fs_version(void);
#ifdef __cplusplus #ifdef __cplusplus

View file

@ -25,6 +25,15 @@
extern "C" { extern "C" {
#endif #endif
/*@
@ requires \valid(disk_car);
@ requires valid_disk(disk_car);
@ requires valid_list_part(list_part);
@ requires \valid(current_cmd);
@ requires valid_read_string(*current_cmd);
@ requires separation: \separated(disk_car, list_part, current_cmd);
@ ensures valid_read_string(*current_cmd);
@*/
int interface_superblock(disk_t *disk_car, const list_part_t *list_part, char**current_cmd); int interface_superblock(disk_t *disk_car, const list_part_t *list_part, char**current_cmd);
#ifdef __cplusplus #ifdef __cplusplus

View file

@ -25,6 +25,13 @@
extern "C" { extern "C" {
#endif #endif
/*@
@ requires \valid(disk_car);
@ requires valid_disk(disk_car);
@ requires \valid(partition);
@ requires valid_partition(partition);
@ ensures valid_list_part(\result);
@*/
list_part_t *search_superblock(disk_t *disk_car, partition_t *partition, const int verbose, const int dump_ind); list_part_t *search_superblock(disk_t *disk_car, partition_t *partition, const int verbose, const int dump_ind);
#ifdef __cplusplus #ifdef __cplusplus

View file

@ -32,7 +32,7 @@
#include "filegen.h" #include "filegen.h"
#include "dir.h" #include "dir.h"
#include "ext2grp.h" #include "ext2grp.h"
#include "ext2.h" #include "ext2_common.h"
#include "log.h" #include "log.h"
#include "photorec.h" #include "photorec.h"

View file

@ -25,7 +25,30 @@
extern "C" { extern "C" {
#endif #endif
/*@
@ requires valid_list_search_space(list_search_space);
@ requires valid_disk(disk);
@ requires valid_partition(partition);
@ requires \valid(disk);
@ requires \valid_read(partition);
@ requires \separated(list_search_space, disk, partition);
@ ensures valid_disk(disk);
@*/
// ensures valid_list_search_space(list_search_space);
// ensures valid_partition(partition);
unsigned int ext2_fix_group(alloc_data_t *list_search_space, disk_t *disk, const partition_t *partition); unsigned int ext2_fix_group(alloc_data_t *list_search_space, disk_t *disk, const partition_t *partition);
/*@
@ requires valid_list_search_space(list_search_space);
@ requires valid_disk(disk);
@ requires valid_partition(partition);
@ requires \valid(disk);
@ requires \valid_read(partition);
@ requires \separated(list_search_space, disk, partition);
@ ensures valid_disk(disk);
@*/
// ensures valid_list_search_space(list_search_space);
// ensures valid_partition(partition);
unsigned int ext2_fix_inode(alloc_data_t *list_search_space, disk_t *disk, const partition_t *partition); unsigned int ext2_fix_inode(alloc_data_t *list_search_space, disk_t *disk, const partition_t *partition);
#ifdef __cplusplus #ifdef __cplusplus

View file

@ -26,6 +26,14 @@ extern "C" {
#endif #endif
#ifdef HAVE_LIBEXT2FS #ifdef HAVE_LIBEXT2FS
/*@
@ requires \valid(disk);
@ requires valid_disk(disk);
@ requires \valid_read(partition);
@ requires valid_list_search_space(list_search_space);
@ requires \separated(disk, partition, list_search_space);
@ ensures valid_list_search_space(list_search_space);
@*/
unsigned int ext2_remove_used_space(disk_t *disk, const partition_t *partition, alloc_data_t *list_search_space); unsigned int ext2_remove_used_space(disk_t *disk, const partition_t *partition, alloc_data_t *list_search_space);
#endif #endif

View file

@ -30,7 +30,6 @@
#include <stdio.h> #include <stdio.h>
#include "types.h" #include "types.h"
#include "common.h" #include "common.h"
#include "ext2.h"
#include "ext2_common.h" #include "ext2_common.h"
#include "filegen.h" #include "filegen.h"
#include "log.h" #include "log.h"

View file

@ -30,7 +30,6 @@
#include <stdio.h> #include <stdio.h>
#include "types.h" #include "types.h"
#include "common.h" #include "common.h"
#include "ext2.h"
#include "ext2_common.h" #include "ext2_common.h"
#include "filegen.h" #include "filegen.h"

View file

@ -30,7 +30,7 @@
#include "types.h" #include "types.h"
#include "common.h" #include "common.h"
#include "ext2.h" #include "ext2_common.h"
#include "next.h" #include "next.h"
extern const arch_fnct_t arch_i386; extern const arch_fnct_t arch_i386;
extern const arch_fnct_t arch_mac; extern const arch_fnct_t arch_mac;