src/hfsp_struct.h: move struct from src/hfsp.h

src/file_hfsp.c: add frama-c annotations
This commit is contained in:
Christophe Grenier 2021-02-22 20:41:15 +01:00
parent dab7c27606
commit e1124cc355
4 changed files with 194 additions and 128 deletions

View file

@ -42,7 +42,7 @@ base_C = $(smallbase_C) autoset.c ewf.c fnctdsk.c hdaccess.c hdcache.c hdwin32
base_H = $(smallbase_H) alignio.h autoset.h ewf.h fnctdsk.h hdaccess.h hdwin32.h hidden.h guid_cmp.h guid_cpy.h hdcache.h hpa_dco.h intrf.h iso.h iso9660.h lang.h list.h list_sort.h log_part.h types.h io_redir.h msdos.h ntfs_utl.h parti386.h partgpt.h parthumax.h partmac.h partsun.h partxbox.h partauto.h sudo.h unicode.h win32.h
fs_C = analyse.c bfs.c bsd.c btrfs.c cramfs.c exfat.c ext2.c fat.c fatx.c f2fs.c jfs.c gfs2.c hfs.c hfsp.c hpfs.c luks.c lvm.c md.c netware.c ntfs.c refs.c rfs.c savehdr.c sun.c swap.c sysv.c ufs.c vmfs.c wbfs.c xfs.c zfs.c
fs_H = analyse.h bfs.h bsd.h btrfs.h cramfs.h exfat.h ext2.h fat.h fatx.h f2fs.h f2fs_fs.h jfs_superblock.h jfs.h gfs2.h hfs.h hfsp.h hpfs.h luks.h lvm.h md.h netware.h ntfs.h ntfs_struct.h refs.h rfs.h savehdr.h sun.h swap.h sysv.h ufs.h vmfs.h wbfs.h xfs.h zfs.h
fs_H = analyse.h bfs.h bsd.h btrfs.h cramfs.h exfat.h ext2.h fat.h fatx.h f2fs.h f2fs_fs.h jfs_superblock.h jfs.h gfs2.h hfs.h hfsp.h hpfs.h hfsp_struct.h luks.h lvm.h md.h netware.h ntfs.h ntfs_struct.h refs.h rfs.h savehdr.h sun.h swap.h sysv.h ufs.h vmfs.h wbfs.h xfs.h zfs.h
testdisk_ncurses_C = addpart.c addpartn.c adv.c askloc.c chgarch.c chgarchn.c chgtype.c chgtypen.c dimage.c dirn.c dirpart.c diskacc.c diskcapa.c edit.c ext2_sb.c ext2_sbn.c fat1x.c fat32.c fat_adv.c fat_cluster.c fatn.c geometry.c geometryn.c godmode.c hiddenn.c intrface.c intrfn.c nodisk.c ntfs_adv.c ntfs_fix.c ntfs_udl.c parti386n.c partgptn.c partmacn.c partsunn.c partxboxn.c tanalyse.c tbanner.c tdelete.c tdiskop.c tdisksel.c testdisk.c texfat.c thfs.c tload.c tlog.c tmbrcode.c tntfs.c toptions.c tpartwr.c
testdisk_ncurses_H = addpart.h addpartn.h adv.h askloc.h chgarch.h chgarchn.h chgtype.h chgtypen.h dimage.h dirn.h dirpart.h diskacc.h diskcapa.h edit.h ext2_sb.h ext2_sbn.h fat1x.h fat32.h fat_adv.h fat_cluster.h fatn.h geometry.h geometryn.h godmode.h hiddenn.h intrface.h intrfn.h nodisk.h ntfs_adv.h ntfs_fix.h ntfs_udl.h partgptn.h parti386n.h partmacn.h partsunn.h partxboxn.h tanalyse.h tdelete.h tdiskop.h tdisksel.h texfat.h thfs.h tload.h tlog.h tmbrcode.h tntfs.h toptions.h tpartwr.h
@ -389,7 +389,7 @@ file_C = filegen.c \
file_zip.c \
file_zpr.c
file_H = ext2.h filegen.h file_doc.h file_jpg.h file_gz.h file_sp3.h file_tar.h file_tiff.h file_txt.h ole.h pe.h suspend.h
file_H = ext2.h hfsp_struct.h filegen.h file_doc.h file_jpg.h file_gz.h file_sp3.h file_tar.h file_tiff.h file_txt.h ntfs_struct.h ole.h pe.h suspend.h
photorec_C = photorec.c phcfg.c addpart.c chgarch.c chgtype.c dir.c exfatp.c ext2grp.c ext2_dir.c ext2p.c fat_dir.c fatp.c file_found.c geometry.c ntfs_dir.c ntfsp.c pdisksel.c poptions.c sessionp.c dfxml.c partgptro.c

View file

@ -31,8 +31,9 @@
#include "types.h"
#include "filegen.h"
#include "common.h"
#include "hfsp.h"
#include "hfsp_struct.h"
/*@ requires \valid(file_stat); */
static void register_header_check_hfsp(file_stat_t *file_stat);
const file_hint_t file_hint_hfsp= {
@ -44,6 +45,17 @@ const file_hint_t file_hint_hfsp= {
.register_header_check=&register_header_check_hfsp
};
/*@
@ requires buffer_size >= sizeof(struct hfsp_vh);
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires valid_file_recovery(file_recovery);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@ requires separation: \separated(&file_hint_hfsp, buffer+(..), file_recovery, file_recovery_new);
@ ensures \result == 0 || \result == 1;
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
@ assigns *file_recovery_new;
@*/
static int header_check_hfsp(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)
{
const struct hfsp_vh *vh=(const struct hfsp_vh *)buffer;
@ -57,7 +69,9 @@ reset_file_recovery(file_recovery_new);
static void register_header_check_hfsp(file_stat_t *file_stat)
{
register_header_check(0, "H+\0\4", 4, &header_check_hfsp, file_stat);
#ifndef __FRAMAC__
register_header_check(0, "HX\0\5", 4, &header_check_hfsp, file_stat);
#endif
}
#endif

View file

@ -1,12 +1,7 @@
/*
File: hfsp.h, TestDisk
Copyright (C) 2005-2006 Christophe GRENIER <grenier@cgsecurity.org>
Original header comes from libhfs - library for reading and writing
Macintosh HFS volumes
Copyright (C) 2000 Klaus Halfmann <klaus.halfmann@feri.de>
Original work by 1996-1998 Robert Leslie <rob@mars.org>
other work 2000 from Brad Boyer (flar@pants.nu)
Copyright (C) 2005-2021 Christophe GRENIER <grenier@cgsecurity.org>
This software is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
@ -28,128 +23,32 @@
#ifdef __cplusplus
extern "C" {
#endif
#include "hfsp_struct.h"
#define HFSP_BOOT_SECTOR_SIZE 512
#define HFSP_BLOCKSZ 512 /* A sector for Apple is always 512 bytes */
#define HFSP_BLOCKSZ_BITS 9 /* 1<<9 == 512 */
#define HFSP_VOLHEAD_SIG 0x482B /* 'H+' */
#define HFSX_VOLHEAD_SIG 0x4858 /* 'HX' */
/*@
@ requires \valid(disk_car);
@ requires valid_disk(disk_car);
@ requires \valid(partition);
@ requires \separated(disk_car, partition);
@*/
int check_HFSP(disk_t *disk_car, partition_t *partition, const int verbose);
#define HFSP_VERSION 4
#define HFSX_VERSION 5
// Minimum Key size for all btrees
#define HFSP_CAT_KEY_MIN_LEN 6
// Maximum Key size for all btrees
#define HFSP_CAT_KEY_MAX_LEN 516
/* HFS+ includes POSIX permissions , although marked as reserved they will be
* used as such. Is ignored by MacOS 8-9 but probably not by MacOS X.
*/
typedef struct {
uint32_t owner;
uint32_t group;
uint32_t mode;
uint32_t dev;
} hfsp_perm;
/* A single contiguous area (fragment) of a file */
typedef struct {
uint32_t start_block;
uint32_t block_count;
} hfsp_extent;
/* A file may contain up to 8 normale extents, all other
are found in some extra extent area */
typedef hfsp_extent hfsp_extent_rec[8];
/* Information for a "Fork" in a file
* Forks are the "usual" DATA and RSRC forks or special files
* (e.g. the Volume Bitmap)
*/
typedef struct {
uint64_t total_size; // logical size
uint32_t clump_size; // number of bytes to preallocate
uint32_t total_blocks;
hfsp_extent_rec extents; // initial (8) extents
} hfsp_fork_raw;
/* HFS+ Volume Header
* Always found at block 2 of the disk, a copy is stored
* at the second to last block of the disk.
*/
typedef struct hfsp_vh {
uint16_t signature; // 00: must be HFSPLUS_VOLHEAD_SIG 'H+'
uint16_t version; // 02: 4 for HFS+, 5 for HFSX
uint32_t attributes; // 04: See bit constants below
uint32_t last_mount_vers; // 08
// Use a registered creator code here (See libhfsp.h)
// Mac OS uses '8.10' well
uint32_t reserved; // 0C
uint32_t create_date; // 10 local time !
uint32_t modify_date; // 14 GMT (?)
uint32_t backup_date; // 18 GMT (?)
uint32_t checked_date; // 1C GMT (?) fsck ?
uint32_t file_count; // 20
// not including special files but including DATA and RSRC forks
uint32_t folder_count; // 24 excluding the root folder
uint32_t blocksize; // 28
// must be multiple of HFSPLUS_SECTOR_SIZE,
// should be a multiple of 4k for harddisk
uint32_t total_blocks; // 2C
uint32_t free_blocks; // 30
// The total number of unused allocation blocks on the disk.
uint32_t next_alloc;
// hint where to search for next allocation blocks
uint32_t rsrc_clump_sz;
// default clump size for rsrc forks
uint32_t data_clump_sz;
// default clump size for data forks
uint32_t next_cnid;
// next unused catalog id
uint32_t write_count;
// increment on every mount (and write ?)
uint64_t encodings_bmp;
// for every encoding used on the disk a bit is set
// ignored but eventually must be cared for
char finder_info[32];
hfsp_fork_raw alloc_file;
// stores bitmap of use/free blocks
hfsp_fork_raw ext_file;
// stores oferflow extents
hfsp_fork_raw cat_file;
// This contains the root directory
hfsp_fork_raw attr_file;
hfsp_fork_raw start_file;
// a special startup file may be described here (used by ?)
} hfsp_vh;
/* HFS+ volume attributes */
/* 0-6 reserved, may be used in memory only */
#define HFSPLUS_VOL_RESERVED1 0x000000FF
#define HFSPLUS_VOL_HARDLOCK 0x00000080 // Used in Memory by finder only
#define HFSPLUS_VOL_UNMNT 0x00000100
// clear this bit when mounting, set as last step of unmounting
// This is checked by (slower) ROM code
#define HFSPLUS_VOL_SPARE_BLK 0x00000200
#define HFSPLUS_VOL_NOCACHE 0x00000400
// in case of RAM or ROM disk (try a HFS+ Ramdisk :)
#define HFSPLUS_VOL_INCNSTNT 0x00000800
// Reverse meaning as of HFSPLUS_VOL_UNMNT
// This is checked by (faster) Mac OS code
/* 12-14 reserved */
#define HFSPLUS_VOL_RESERVED2 0x00007000
#define HFSPLUS_VOL_SOFTLOCK 0x00008000
#define HFSPLUS_VOL_RESERVED3 0xFFFF0000
int check_HFSP(disk_t *disk_car,partition_t *partition,const int verbose);
/*@
@ requires \valid_read(disk_car);
@ requires valid_disk(disk_car);
@ requires \valid_read(vh);
@ requires \valid_read(partition);
@ requires \separated(disk_car, vh, partition);
@*/
int test_HFSP(const disk_t *disk_car, const struct hfsp_vh *vh, const partition_t *partition, const int verbose, const int dump_ind);
/*@
@ requires \valid(disk_car);
@ requires valid_disk(disk_car);
@ requires \valid_read(vh);
@ requires \valid(partition);
@ requires \separated(disk_car, vh, partition);
@*/
int recover_HFSP(disk_t *disk_car, const struct hfsp_vh *vh, partition_t *partition, const int verbose, const int dump_ind, const int backup);
#ifdef __cplusplus

153
src/hfsp_struct.h Normal file
View file

@ -0,0 +1,153 @@
/*
File: hfsp_struct.h, TestDisk
Copyright (C) 2005-2006 Christophe GRENIER <grenier@cgsecurity.org>
Original header comes from libhfs - library for reading and writing
Macintosh HFS volumes
Copyright (C) 2000 Klaus Halfmann <klaus.halfmann@feri.de>
Original work by 1996-1998 Robert Leslie <rob@mars.org>
other work 2000 from Brad Boyer (flar@pants.nu)
This software is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License along
with this program; if not, write the Free Software Foundation, Inc., 51
Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*/
#ifndef _HFSP_STRUCT_H
#define _HFSP_STRUCT_H
#ifdef __cplusplus
extern "C" {
#endif
#define HFSP_BOOT_SECTOR_SIZE 512
#define HFSP_BLOCKSZ 512 /* A sector for Apple is always 512 bytes */
#define HFSP_BLOCKSZ_BITS 9 /* 1<<9 == 512 */
#define HFSP_VOLHEAD_SIG 0x482B /* 'H+' */
#define HFSX_VOLHEAD_SIG 0x4858 /* 'HX' */
#define HFSP_VERSION 4
#define HFSX_VERSION 5
// Minimum Key size for all btrees
#define HFSP_CAT_KEY_MIN_LEN 6
// Maximum Key size for all btrees
#define HFSP_CAT_KEY_MAX_LEN 516
/* HFS+ includes POSIX permissions , although marked as reserved they will be
* used as such. Is ignored by MacOS 8-9 but probably not by MacOS X.
*/
typedef struct {
uint32_t owner;
uint32_t group;
uint32_t mode;
uint32_t dev;
} hfsp_perm;
/* A single contiguous area (fragment) of a file */
typedef struct {
uint32_t start_block;
uint32_t block_count;
} hfsp_extent;
/* A file may contain up to 8 normale extents, all other
are found in some extra extent area */
typedef hfsp_extent hfsp_extent_rec[8];
/* Information for a "Fork" in a file
* Forks are the "usual" DATA and RSRC forks or special files
* (e.g. the Volume Bitmap)
*/
typedef struct {
uint64_t total_size; // logical size
uint32_t clump_size; // number of bytes to preallocate
uint32_t total_blocks;
hfsp_extent_rec extents; // initial (8) extents
} hfsp_fork_raw;
/* HFS+ Volume Header
* Always found at block 2 of the disk, a copy is stored
* at the second to last block of the disk.
*/
typedef struct hfsp_vh {
uint16_t signature; // 00: must be HFSPLUS_VOLHEAD_SIG 'H+'
uint16_t version; // 02: 4 for HFS+, 5 for HFSX
uint32_t attributes; // 04: See bit constants below
uint32_t last_mount_vers; // 08
// Use a registered creator code here (See libhfsp.h)
// Mac OS uses '8.10' well
uint32_t reserved; // 0C
uint32_t create_date; // 10 local time !
uint32_t modify_date; // 14 GMT (?)
uint32_t backup_date; // 18 GMT (?)
uint32_t checked_date; // 1C GMT (?) fsck ?
uint32_t file_count; // 20
// not including special files but including DATA and RSRC forks
uint32_t folder_count; // 24 excluding the root folder
uint32_t blocksize; // 28
// must be multiple of HFSPLUS_SECTOR_SIZE,
// should be a multiple of 4k for harddisk
uint32_t total_blocks; // 2C
uint32_t free_blocks; // 30
// The total number of unused allocation blocks on the disk.
uint32_t next_alloc;
// hint where to search for next allocation blocks
uint32_t rsrc_clump_sz;
// default clump size for rsrc forks
uint32_t data_clump_sz;
// default clump size for data forks
uint32_t next_cnid;
// next unused catalog id
uint32_t write_count;
// increment on every mount (and write ?)
uint64_t encodings_bmp;
// for every encoding used on the disk a bit is set
// ignored but eventually must be cared for
char finder_info[32];
hfsp_fork_raw alloc_file;
// stores bitmap of use/free blocks
hfsp_fork_raw ext_file;
// stores oferflow extents
hfsp_fork_raw cat_file;
// This contains the root directory
hfsp_fork_raw attr_file;
hfsp_fork_raw start_file;
// a special startup file may be described here (used by ?)
} hfsp_vh;
/* HFS+ volume attributes */
/* 0-6 reserved, may be used in memory only */
#define HFSPLUS_VOL_RESERVED1 0x000000FF
#define HFSPLUS_VOL_HARDLOCK 0x00000080 // Used in Memory by finder only
#define HFSPLUS_VOL_UNMNT 0x00000100
// clear this bit when mounting, set as last step of unmounting
// This is checked by (slower) ROM code
#define HFSPLUS_VOL_SPARE_BLK 0x00000200
#define HFSPLUS_VOL_NOCACHE 0x00000400
// in case of RAM or ROM disk (try a HFS+ Ramdisk :)
#define HFSPLUS_VOL_INCNSTNT 0x00000800
// Reverse meaning as of HFSPLUS_VOL_UNMNT
// This is checked by (faster) Mac OS code
/* 12-14 reserved */
#define HFSPLUS_VOL_RESERVED2 0x00007000
#define HFSPLUS_VOL_SOFTLOCK 0x00008000
#define HFSPLUS_VOL_RESERVED3 0xFFFF0000
#ifdef __cplusplus
} /* closing brace for extern "C" */
#endif
#endif