luisgulo/testdisk
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Use "DISABLED_FOR_FRAMAC" to disable code to facilitate verification

Browse source 
using frama-c
This commit is contained in:
Christophe Grenier 2022-04-13 09:20:45 +02:00
parent 952415ee99
commit 305d71ea0a
127 changed files with 1768 additions and 711 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Makefile.am
View file

@ -488,20 +488,20 @@ session_%.framac: file_%.c common.c filegen.c log.c
frama-c $^ -cpp-extra-args="-DMAIN_$* -DHAVE_CONFIG_H -DSINGLE_FORMAT -DSINGLE_FORMAT_$* -D__x86_64__ -I.." $(FRAMA_C_FLAGS) -save $@
session_fidentify-%.framac: $(fidentify_C_SOURCES)
$(CC) $(CFLAGS) -DMAIN_fidentify -DHAVE_CONFIG_H -DSINGLE_FORMAT -DSINGLE_FORMAT_$* -I.. $^ -o fidentify_$*
frama-c $^ -cpp-extra-args="-DMAIN_fidentify -DHAVE_CONFIG_H -DSINGLE_FORMAT -DSINGLE_FORMAT_$* -D__x86_64__ -I.." $(FRAMA_C_FLAGS) -save $@
$(CC) $(CFLAGS) -DDISABLED_FOR_FRAMAC -DHAVE_CONFIG_H -DSINGLE_FORMAT -DSINGLE_FORMAT_$* -I.. $^ -o fidentify_$*
frama-c $^ -cpp-extra-args="-DDISABLED_FOR_FRAMAC -DHAVE_CONFIG_H -DSINGLE_FORMAT -DSINGLE_FORMAT_$* -D__x86_64__ -I.." $(FRAMA_C_FLAGS) -save $@
session_fidentify.framac: $(fidentify_C_SOURCES)
$(CC) $(CFLAGS) -DMAIN_fidentify -DHAVE_CONFIG_H -I.. $^ -o demo_fidentify
frama-c $^ -cpp-extra-args="-DMAIN_fidentify -DHAVE_CONFIG_H -D__x86_64__ -I.." $(FRAMA_C_FLAGS) -save $@
$(CC) $(CFLAGS) -DDISABLED_FOR_FRAMAC -DHAVE_CONFIG_H -I.. $^ -o demo_fidentify
frama-c $^ -cpp-extra-args="-DDISABLED_FOR_FRAMAC -DHAVE_CONFIG_H -D__x86_64__ -I.." $(FRAMA_C_FLAGS) -save $@
session_photorec-%.framac: $(photorec_C_SOURCES)
$(CC) $(CFLAGS) -DMAIN_photorec -DHAVE_CONFIG_H -DSINGLE_FORMAT -DSINGLE_FORMAT_$* -DSINGLE_PARTITION_TYPE -I.. $^ -o photorec_$*
frama-c $^ -cpp-extra-args="-DMAIN_photorec -DHAVE_CONFIG_H -DSINGLE_FORMAT -DSINGLE_FORMAT_$* -DSINGLE_PARTITION_TYPE -D__x86_64__ -I.." $(FRAMA_C_FLAGS) -save $@
$(CC) $(CFLAGS) -DDISABLED_FOR_FRAMAC -DHAVE_CONFIG_H -DSINGLE_FORMAT -DSINGLE_FORMAT_$* -DSINGLE_PARTITION_TYPE -I.. $^ -o photorec_$*
frama-c $^ -cpp-extra-args="-DDISABLED_FOR_FRAMAC -DHAVE_CONFIG_H -DSINGLE_FORMAT -DSINGLE_FORMAT_$* -DSINGLE_PARTITION_TYPE -D__x86_64__ -I.." $(FRAMA_C_FLAGS) -save $@
session_photorec.framac: $(photorec_C_SOURCES)
$(CC) $(CFLAGS) -DMAIN_photorec -DHAVE_CONFIG_H -I.. $^ -o demo_photorec
frama-c $^ -cpp-extra-args="-DMAIN_photorec -DHAVE_CONFIG_H -D__x86_64__ -I.." $(FRAMA_C_FLAGS) -save $@
$(CC) $(CFLAGS) -DDISABLED_FOR_FRAMAC -DHAVE_CONFIG_H -I.. $^ -o demo_photorec
frama-c $^ -cpp-extra-args="-DDISABLED_FOR_FRAMAC -DHAVE_CONFIG_H -D__x86_64__ -I.." $(FRAMA_C_FLAGS) -save $@
moc_qphotorec.cpp: qphotorec.h
$(AM_V_GEN) QT_SELECT=$(QT_SELECT) $(MOC) $< -o $@

2
src/addpartn.c
View file

@ -24,7 +24,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_NCURSES
#endif

24
src/analyse.c
View file

@ -32,7 +32,7 @@
#include "analyse.h"
#include "fat.h"
#include "exfat.h"
#if !defined(__FRAMAC__) && !defined(MAIN_photorec)
#if !defined(DISABLED_FOR_FRAMAC)
#include "apfs.h"
#include "bfs.h"
#include "bsd.h"
@ -73,7 +73,7 @@ int search_NTFS_backup(unsigned char *buffer, disk_t *disk, partition_t *partiti
return -1;
{
const struct ntfs_boot_sector *ntfs_header=(const struct ntfs_boot_sector*)buffer;
#if !defined(__FRAMAC__) && !defined(MAIN_photorec)
#if !defined(DISABLED_FOR_FRAMAC)
/* NTFS recovery using backup sector */
if(le16(ntfs_header->marker)==0xAA55 &&
recover_NTFS(disk, ntfs_header, partition, verbose, dump_ind, 1)==0)
@ -87,7 +87,7 @@ int search_HFS_backup(unsigned char *buffer, disk_t *disk, partition_t *partitio
{
if(disk->pread(disk, buffer, 0x400, partition->part_offset)!= 0x400)
return -1;
#if !defined(__FRAMAC__) && !defined(MAIN_photorec)
#if !defined(DISABLED_FOR_FRAMAC)
{
const hfs_mdb_t *hfs_mdb=(const hfs_mdb_t *)buffer;
const struct hfsp_vh *vh=(const struct hfsp_vh *)buffer;
@ -142,7 +142,7 @@ int search_FAT_backup(unsigned char *buffer, disk_t *disk, partition_t *partitio
int search_type_0(const unsigned char *buffer, disk_t *disk, partition_t *partition, const int verbose, const int dump_ind)
{
#if !defined(__FRAMAC__) && !defined(MAIN_photorec)
#if !defined(DISABLED_FOR_FRAMAC)
/* Expect a buffer filled with 8k to handle the SWAP detection */
const pv_disk_t *pv=(const pv_disk_t *)buffer;
const struct cramfs_super *cramfs=(const struct cramfs_super *)buffer;
@ -237,7 +237,7 @@ int search_type_0(const unsigned char *buffer, disk_t *disk, partition_t *partit
int search_type_1(const unsigned char *buffer, const disk_t *disk, partition_t *partition, const int verbose, const int dump_ind)
{
#if !defined(__FRAMAC__) && !defined(MAIN_photorec)
#if !defined(DISABLED_FOR_FRAMAC)
const struct disklabel *bsd_header=(const struct disklabel *)(buffer+0x200);
const struct disk_super_block *beos_block=(const struct disk_super_block*)(buffer+0x200);
const struct cramfs_super *cramfs=(const struct cramfs_super *)(buffer+0x200);
@ -278,7 +278,7 @@ int search_type_1(const unsigned char *buffer, const disk_t *disk, partition_t *
int search_type_2(const unsigned char *buffer, disk_t *disk, partition_t *partition, const int verbose, const int dump_ind)
{
#if !defined(__FRAMAC__) && !defined(MAIN_photorec)
#if !defined(DISABLED_FOR_FRAMAC)
const hfs_mdb_t *hfs_mdb=(const hfs_mdb_t *)(buffer+0x400);
const struct hfsp_vh *vh=(const struct hfsp_vh *)(buffer+0x400);
const struct ext2_super_block *sb=(const struct ext2_super_block*)(buffer+0x400);
@ -317,7 +317,7 @@ int search_type_8(unsigned char *buffer, disk_t *disk,partition_t *partition,con
}
if(disk->pread(disk, buffer, 4096, partition->part_offset + 4096) != 4096)
return -1;
#if !defined(__FRAMAC__) && !defined(MAIN_photorec)
#if !defined(DISABLED_FOR_FRAMAC)
{ /* MD 1.2 */
const struct mdp_superblock_1 *sb1=(const struct mdp_superblock_1 *)buffer;
if(le32(sb1->major_version)==1 &&
@ -341,7 +341,7 @@ int search_type_16(unsigned char *buffer, disk_t *disk,partition_t *partition,co
/* 8k offset */
if(disk->pread(disk, buffer, 3 * DEFAULT_SECTOR_SIZE, partition->part_offset + 16 * 512) != 3 * DEFAULT_SECTOR_SIZE)
return -1;
#if !defined(__FRAMAC__) && !defined(MAIN_photorec)
#if !defined(DISABLED_FOR_FRAMAC)
{
const struct ufs_super_block *ufs=(const struct ufs_super_block *)buffer;
const struct vdev_boot_header *zfs=(const struct vdev_boot_header*)buffer;
@ -368,7 +368,7 @@ int search_type_64(unsigned char *buffer, disk_t *disk,partition_t *partition,co
/* 32k offset */
if(disk->pread(disk, buffer, 3 * DEFAULT_SECTOR_SIZE, partition->part_offset + 63 * 512) != 3 * DEFAULT_SECTOR_SIZE)
return -1;
#if !defined(__FRAMAC__) && !defined(MAIN_photorec)
#if !defined(DISABLED_FOR_FRAMAC)
{
const struct jfs_superblock* jfs=(const struct jfs_superblock*)(buffer+0x200);
/* Test JFS */
@ -389,7 +389,7 @@ int search_type_128(unsigned char *buffer, disk_t *disk, partition_t *partition,
}
if(disk->pread(disk, buffer, 11 * DEFAULT_SECTOR_SIZE, partition->part_offset + 126 * 512) != 11 * DEFAULT_SECTOR_SIZE)
return -1;
#if !defined(__FRAMAC__) && !defined(MAIN_photorec)
#if !defined(DISABLED_FOR_FRAMAC)
{
const unsigned char *buffer_1024=buffer+0x400;
const struct reiserfs_super_block *rfs=(const struct reiserfs_super_block *)buffer_1024;
@ -428,7 +428,7 @@ int search_type_2048(unsigned char *buffer, disk_t *disk, partition_t *partition
}
if(disk->pread(disk, buffer, 2*DEFAULT_SECTOR_SIZE, partition->part_offset + 2048 * 512) != 2*DEFAULT_SECTOR_SIZE)
return -1;
#if !defined(__FRAMAC__) && !defined(MAIN_photorec)
#if !defined(DISABLED_FOR_FRAMAC)
{
const struct vmfs_volume *sb_vmfs=(const struct vmfs_volume *)buffer;
if(le32(sb_vmfs->magic)==0xc001d00d &&
@ -441,7 +441,7 @@ int search_type_2048(unsigned char *buffer, disk_t *disk, partition_t *partition
int check_linux(disk_t *disk, partition_t *partition, const int verbose)
{
#if !defined(__FRAMAC__) && !defined(MAIN_photorec)
#if !defined(DISABLED_FOR_FRAMAC)
if(check_JFS(disk, partition)==0 ||
check_rfs(disk, partition, verbose)==0 ||
check_EXT2(disk, partition, verbose)==0 ||

2
src/askloc.c
View file

@ -23,7 +23,7 @@
#include <config.h>
#endif
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
#undef HAVE_GETCWD
#endif

2
src/askloc.h
View file

@ -26,7 +26,7 @@
extern "C" {
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_NCURSES
#endif

59
src/chgarch.c
View file

@ -38,33 +38,76 @@
#include "hdaccess.h"
#include "chgarch.h"
extern const arch_fnct_t arch_i386;
extern const arch_fnct_t arch_gpt;
extern const arch_fnct_t arch_humax;
extern const arch_fnct_t arch_mac;
extern const arch_fnct_t arch_none;
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_GPT)
extern const arch_fnct_t arch_gpt;
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_HUMAX)
extern const arch_fnct_t arch_humax;
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_I386)
extern const arch_fnct_t arch_i386;
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_MAC)
extern const arch_fnct_t arch_mac;
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_SUN)
extern const arch_fnct_t arch_sun;
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_XBOX)
extern const arch_fnct_t arch_xbox;
#endif
/* return 1 if user need to give the partition table type */
int change_arch_type_cli(disk_t *disk, const int verbose, char**current_cmd)
{
const arch_fnct_t *arch_list[]={&arch_i386, &arch_gpt, &arch_humax, &arch_mac, &arch_none, &arch_sun, &arch_xbox, NULL};
#ifndef DISABLED_FOR_FRAMAC
const arch_fnct_t *arch_list[]={
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_I386)
&arch_i386,
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_GPT)
&arch_gpt,
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_HUMAX)
&arch_humax,
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_MAC)
&arch_mac,
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_NONE)
&arch_none,
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_SUN)
&arch_sun,
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_XBOX)
&arch_xbox,
#endif
NULL};
int keep_asking;
if(*current_cmd==NULL)
return 1;
/*@ assert valid_read_string(*current_cmd); */
/*@
loop invariant valid_read_string(*current_cmd);
*/
do
{
int i;
keep_asking=0;
skip_comma_in_command(current_cmd);
for(i=0;arch_list[i]!=NULL;i++)
/*@
loop unroll 10;
@*/
for(i=0; arch_list[i]!=NULL; i++)
{
if(check_command(current_cmd, arch_list[i]->part_name_option, strlen(arch_list[i]->part_name_option))==0)
{
disk->arch=arch_list[i];
keep_asking=1;
}
}
if(check_command(current_cmd, "ask_type", 8)==0)
{
return 1;
@ -74,5 +117,7 @@ int change_arch_type_cli(disk_t *disk, const int verbose, char**current_cmd)
hd_update_geometry(disk, verbose);
log_info("%s\n",disk->description_short(disk));
log_info("Partition table type: %s\n", disk->arch->part_name);
#endif
/*@ assert valid_disk(disk); */
return 0;
}

4
src/chgarchn.c
View file

@ -23,7 +23,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_NCURSES
#endif
@ -44,11 +44,11 @@
#include "autoset.h"
#include "chgarchn.h"
extern const arch_fnct_t arch_none;
extern const arch_fnct_t arch_i386;
extern const arch_fnct_t arch_gpt;
extern const arch_fnct_t arch_humax;
extern const arch_fnct_t arch_mac;
extern const arch_fnct_t arch_none;
extern const arch_fnct_t arch_sun;
extern const arch_fnct_t arch_xbox;

19
src/chgtype.c
View file

@ -34,14 +34,27 @@
#include "log.h"
#include "log_part.h"
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_GPT)
extern const arch_fnct_t arch_gpt;
extern const arch_fnct_t arch_none;
#endif
/*@
@ requires \valid(current_cmd);
@ requires valid_read_string(*current_cmd);
@ ensures valid_read_string(*current_cmd);
@*/
// TODO assigns *current_cmd;
static int get_hex_from_command(char **current_cmd)
{
const int tmp=strtol(*current_cmd, NULL, 16);
/*@
@ loop invariant valid_read_string(*current_cmd);
@ loop assigns *current_cmd;
@*/
while(*current_cmd[0]!=',' && *current_cmd[0]!='\0')
(*current_cmd)++;
/*@ assert valid_read_string(*current_cmd); */
return tmp;
}
@ -53,6 +66,7 @@ void change_part_type_cli(const disk_t *disk_car,partition_t *partition, char **
return ;
if(partition->arch==NULL)
return;
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_GPT)
if(partition->arch==&arch_gpt)
{
partition->arch=&arch_none;
@ -61,11 +75,14 @@ void change_part_type_cli(const disk_t *disk_car,partition_t *partition, char **
const int tmp_val=get_hex_from_command(current_cmd);
partition->arch->set_part_type(partition,tmp_val);
}
#ifndef DISABLED_FOR_FRAMAC
log_info("Change partition type:\n");
log_partition(disk_car,partition);
#endif
partition->arch=&arch_gpt;
return;
}
#endif
if(partition->arch->set_part_type==NULL)
return ;
skip_comma_in_command(current_cmd);
@ -73,7 +90,9 @@ void change_part_type_cli(const disk_t *disk_car,partition_t *partition, char **
const int tmp_val=get_hex_from_command(current_cmd);
partition->arch->set_part_type(partition,tmp_val);
}
#ifndef DISABLED_FOR_FRAMAC
log_info("Change partition type:\n");
log_partition(disk_car,partition);
#endif
return ;
}

2
src/chgtypen.c
View file

@ -23,7 +23,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_NCURSES
#endif

34
src/common.c
View file

@ -25,7 +25,7 @@
#include <config.h>
#endif
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
#undef HAVE_POSIX_MEMALIGN
#undef HAVE_MEMALIGN
#undef HAVE_NCURSES
@ -84,13 +84,23 @@ void *MALLOC(size_t size)
}
}
#endif
#ifdef DISABLED_FOR_FRAMAC
if((res=calloc(1,size))==NULL)
{
exit(EXIT_FAILURE);
}
#else
if((res=malloc(size))==NULL)
{
#ifndef DISABLED_FOR_FRAMAC
log_critical("\nCan't allocate %lu bytes of memory.\n", (long unsigned)size);
log_close();
#endif
exit(EXIT_FAILURE);
}
memset(res,0,size);
#endif
/*@ assert \valid((char *)res + (0 .. size - 1)); */
return res;
}
@ -171,7 +181,7 @@ char * strcasestr (const char *haystack, const char *needle)
}
#endif
#if ! defined(HAVE_LOCALTIME_R) && ! defined(__MINGW32__) && !defined(__FRAMAC__)
#if ! defined(HAVE_LOCALTIME_R) && ! defined(__MINGW32__) && !defined(DISABLED_FOR_FRAMAC)
struct tm *localtime_r(const time_t *timep, struct tm *result)
{
return localtime(timep);
@ -179,6 +189,7 @@ struct tm *localtime_r(const time_t *timep, struct tm *result)
#endif
/*@
@ decreases number;
@ assigns \nothing;
@*/
static unsigned int up2power_aux(const unsigned int number)
@ -312,7 +323,7 @@ time_t date_dos2unix(const unsigned short f_time, const unsigned short f_date)
void set_secwest(void)
{
const time_t t = time(NULL);
#if defined(__MINGW32__) || defined(__FRAMAC__)
#if defined(__MINGW32__) || defined(DISABLED_FOR_FRAMAC)
const struct tm *tmptr = localtime(&t);
#else
struct tm tmp;
@ -359,14 +370,21 @@ int check_command(char **current_cmd, const char *cmd, const size_t n)
const int res=strncmp(*current_cmd, cmd, n);
if(res==0)
{
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
const char *src=*current_cmd;
unsigned int i;
/*@
@ loop invariant valid_read_string(*current_cmd);
@ loop assigns i, *current_cmd;
@ loop invariant valid_read_string(src);
@ loop assigns i, src;
@*/
for(i=0; i<n && *current_cmd!='\0'; i++)
(*current_cmd)++;
for(i=0; i<n && src[0]!='\0'; i++)
{
/*@ assert valid_read_string(src); */
/*@ assert src[0]!= '\0'; */
src++;
/*@ assert valid_read_string(src); */
}
*current_cmd=src;
#else
(*current_cmd)+=n;
#endif

32
src/common.h
View file

@ -24,10 +24,10 @@
#ifdef __cplusplus
extern "C" {
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_NCURSES
#endif
#if defined(__FRAMAC__) && defined(HAVE_STRING_H)
#if defined(DISABLED_FOR_FRAMAC) && defined(HAVE_STRING_H)
#include <string.h>
#endif
@ -344,8 +344,15 @@ struct list_part_struct
list_part_t *next;
int to_be_removed;
};
/*@
predicate valid_list_part(list_part_t *list) = ((list == \null) || (\valid_read(list) && valid_list_part(list->next)));
inductive valid_list_part{L} (list_part_t *list)
{
case list_null{L}:
valid_list_part(\null);
case list_not_null{L}:
\forall list_part_t *list; \valid_read(list) ==> valid_list_part(list->next) ==> valid_list_part(list);
}
@*/
typedef struct list_disk_struct list_disk_t;
@ -441,7 +448,7 @@ struct param_disk_struct
};
/*@
predicate valid_disk(disk_t *disk) = ((disk == \null) ||
predicate valid_disk(disk_t *disk) =
(\valid_read(disk) &&
\freeable(disk) &&
valid_read_string(disk->device) &&
@ -457,13 +464,18 @@ struct param_disk_struct
(disk->wbuffer == \null || (\freeable(disk->wbuffer) && disk->wbuffer_size > 0)) &&
valid_arch(disk->arch) &&
disk->sector_size > 0
));
);
*/
/*@ predicate valid_list_disk(list_disk_t* root) = ((root == \null) || (\valid_read(root))); */
/* TODO predicate valid_list_disk{L}(list_disk_t* root) =
\forall list_disk_t *node; \valid(node) && ld_reachable(root,node) ==> \valid(node->disk);
*/
/*@
inductive valid_list_disk{L} (list_disk_t *list)
{
case list_null{L}:
valid_list_disk(\null);
case list_not_null{L}:
\forall list_disk_t *list; \valid_read(list) ==> valid_disk(list->disk) && valid_list_disk(list->next) ==> valid_list_disk(list);
}
@*/
struct partition_struct
@ -605,7 +617,7 @@ int strncasecmp(const char * s1, const char * s2, size_t len);
#ifndef HAVE_STRCASESTR
char * strcasestr (const char *haystack, const char *needle);
#endif
#if ! defined(HAVE_LOCALTIME_R) && ! defined(__MINGW32__) && !defined(__FRAMAC__)
#if ! defined(HAVE_LOCALTIME_R) && ! defined(__MINGW32__) && !defined(DISABLED_FOR_FRAMAC)
/*@
@ requires valid_timer: \valid_read(timep);
@ requires \valid(result);

8
src/dfxml.c
View file

@ -24,7 +24,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_LIBEWF
#undef HAVE_SYS_UTSNAME_H
#undef ENABLE_DFXML
@ -206,13 +206,11 @@ void xml_add_DFXML_creator(const char *package, const char *version)
#ifdef RECORD_COMPILATION_DATE
xml_out2s("compilation_date", get_compilation_date());
#endif
#ifndef MAIN_photorec
xml_printf("<library name='libext2fs' version='%s'/>\n", td_ext2fs_version());
xml_printf("<library name='libewf' version='%s'/>\n", td_ewf_version());
xml_printf("<library name='libjpeg' version='%s'/>\n", td_jpeg_version());
xml_printf("<library name='libntfs' version='%s'/>\n", td_ntfs_version());
xml_printf("<library name='zlib' version='%s'/>\n", td_zlib_version());
#endif
xml_pop("build_environment");
xml_push("execution_environment","");
#if defined(__CYGWIN__) || defined(__MINGW32__)
@ -247,11 +245,11 @@ void xml_add_DFXML_creator(const char *package, const char *version)
#ifdef HAVE_GETEUID
xml_out2i("uid", geteuid());
#endif
#if !defined(__FRAMAC__)
#if !defined(DISABLED_FOR_FRAMAC)
{
char outstr[200];
const time_t t = time(NULL);
#if defined(__MINGW32__) || defined(__FRAMAC__)
#if defined(__MINGW32__) || defined(DISABLED_FOR_FRAMAC)
const struct tm *tmp = localtime(&t);
#else
struct tm tm_tmp;

2
src/dimage.c
View file

@ -126,7 +126,7 @@ int disk_image(disk_t *disk, const partition_t *partition, const char *image_dd)
free(buffer);
return -1;
}
#if !defined(__FRAMAC__)
#if !defined(DISABLED_FOR_FRAMAC)
if(fstat(disk_dst, &stat_buf)==0)
{
int res=1;

12
src/dir.c
View file

@ -23,7 +23,7 @@
#include <config.h>
#endif
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
#undef HAVE_CHMOD
#endif
@ -115,6 +115,7 @@ static char ftypelet (unsigned int bits)
void mode_string (const unsigned int mode, char *str)
{
#ifndef DISABLED_FOR_FRAMAC
str[0] = ftypelet(mode);
str[1] = (mode & LINUX_S_IRUSR) ? 'r' : '-';
str[2] = (mode & LINUX_S_IWUSR) ? 'w' : '-';
@ -156,6 +157,7 @@ void mode_string (const unsigned int mode, char *str)
str[9] = 't';
}
#endif
#endif
}
int set_datestr(char *datestr, size_t n, const time_t timev)
@ -169,7 +171,7 @@ int set_datestr(char *datestr, size_t n, const time_t timev)
strncpy(datestr, " ", n);
return 0;
}
#if defined(__MINGW32__) || defined(__FRAMAC__)
#if defined(__MINGW32__) || defined(DISABLED_FOR_FRAMAC)
tm_p=localtime(&timev);
#else
tm_p=localtime_r(&timev, &tmp);
@ -196,7 +198,7 @@ int dir_aff_log(const dir_data_t *dir_data, const file_info_t *dir_list)
{
log_info("Directory %s\n",dir_data->current_directory);
}
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
td_list_for_each(file_walker, &dir_list->list)
{
const file_info_t *current_file=td_list_entry_const(file_walker, const file_info_t, list);
@ -230,7 +232,7 @@ int dir_aff_log(const dir_data_t *dir_data, const file_info_t *dir_list)
void log_list_file(const disk_t *disk, const partition_t *partition, const dir_data_t *dir_data, const file_info_t*list)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
struct td_list_head *tmp;
log_partition(disk, partition);
if(dir_data!=NULL)
@ -301,6 +303,7 @@ static int is_inode_valid(const file_info_t *current_file, const unsigned int di
@ requires valid_partition(partition);
@ requires \valid(dir_data);
@ requires \separated(disk, partition, dir_data);
@ decreases 0;
@*/
static int dir_whole_partition_log_aux(disk_t *disk, const partition_t *partition, dir_data_t *dir_data, const unsigned long int inode)
{
@ -353,6 +356,7 @@ int dir_whole_partition_log(disk_t *disk, const partition_t *partition, dir_data
@ requires \valid(copy_ok);
@ requires \valid(copy_bad);
@ requires \separated(disk, partition, dir_data, copy_ok, copy_bad);
@ decreases 0;
@*/
static int dir_whole_partition_copy_aux(disk_t *disk, const partition_t *partition, dir_data_t *dir_data, const unsigned long int inode, unsigned int *copy_ok, unsigned int *copy_bad)
{

2
src/dirn.c
View file

@ -23,7 +23,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_NCURSES
#endif

2
src/ewf.c
View file

@ -23,7 +23,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_LIBEWF
#endif

2
src/ewf.h
View file

@ -25,7 +25,7 @@
extern "C" {
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_LIBEWF
#endif

2
src/ext2_dir.c
View file

@ -23,7 +23,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_LIBEXT2FS
#endif

2
src/ext2_inc.h
View file

@ -22,7 +22,7 @@
#ifndef _EXT2_INC_H
#define _EXT2_INC_H
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_LIBEXT2FS
#endif

2
src/ext2p.c
View file

@ -23,7 +23,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_LIBEXT2FS
#endif

45
src/fat.c
View file

@ -46,11 +46,12 @@
#include "dir.h"
#include "fat_dir.h"
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_I386)
extern const arch_fnct_t arch_i386;
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_MAC)
extern const arch_fnct_t arch_mac;
static int log_fat_info(const struct fat_boot_sector*fh1, const upart_type_t upart_type, const unsigned int sector_size);
static int test_OS2MB(const disk_t *disk, const struct fat_boot_sector *fat_header, const partition_t *partition, const int verbose, const int dump_ind);
#endif
/*@
@ requires \valid_read(partition);
@ -77,6 +78,7 @@ static int is_fat32(const partition_t *partition);
@ requires valid_partition(partition);
@ requires \valid_read(fat_header);
@ requires \separated(disk_car, partition, fat_header);
@ decreases 0;
@*/
static int fat32_set_part_name(disk_t *disk_car, partition_t *partition, const struct fat_boot_sector*fat_header)
{
@ -303,6 +305,7 @@ int check_FAT(disk_t *disk_car, partition_t *partition, const int verbose)
@ requires \valid_read(partition);
@ requires valid_partition(partition);
@ requires \separated(disk, partition);
@ decreases 0;
@*/
static unsigned int get_next_cluster_fat12(disk_t *disk, const partition_t *partition, const int offset, const unsigned int cluster)
{
@ -333,6 +336,7 @@ static unsigned int get_next_cluster_fat12(disk_t *disk, const partition_t *part
@ requires \valid_read(partition);
@ requires valid_partition(partition);
@ requires \separated(disk, partition);
@ decreases 0;
@*/
static unsigned int get_next_cluster_fat16(disk_t *disk, const partition_t *partition, const int offset, const unsigned int cluster)
{
@ -361,6 +365,7 @@ static unsigned int get_next_cluster_fat16(disk_t *disk, const partition_t *part
@ requires \valid_read(partition);
@ requires valid_partition(partition);
@ requires \separated(disk, partition);
@ decreases 0;
@*/
static unsigned int get_next_cluster_fat32(disk_t *disk, const partition_t *partition, const int offset, const unsigned int cluster)
{
@ -862,6 +867,7 @@ unsigned long int fat32_get_next_free(const unsigned char *boot_fat32, const uns
@ requires \valid_read(partition);
@ requires valid_partition(partition);
@ requires \separated(disk, partition);
@ decreases 0;
@*/
static int fat_has_EFI_entry(disk_t *disk, const partition_t *partition, const int verbose)
{
@ -977,7 +983,7 @@ static int test_OS2MB(const disk_t *disk, const struct fat_boot_sector *fat_head
const char*buffer=(const char*)fat_header;
if(le16(fat_header->marker)==0xAA55 && memcmp(buffer+FAT_NAME1,"FAT ",8)==0)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
if(verbose||dump_ind)
{
log_info("OS2MB at %u/%u/%u\n",
@ -1043,6 +1049,7 @@ int is_part_fat(const partition_t *partition)
int is_part_fat12(const partition_t *partition)
{
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_I386)
if(partition->arch==&arch_i386)
{
switch(partition->part_type_i386)
@ -1054,13 +1061,7 @@ int is_part_fat12(const partition_t *partition)
break;
}
}
/*
else if(partition->arch==&arch_gpt)
{
if(guid_cmp(partition->part_type_gpt,GPT_ENT_TYPE_MS_BASIC_DATA)==0)
return 1;
}
*/
#endif
return 0;
}
@ -1071,6 +1072,7 @@ static int is_fat12(const partition_t *partition)
int is_part_fat16(const partition_t *partition)
{
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_I386)
if(partition->arch==&arch_i386)
{
switch(partition->part_type_i386)
@ -1086,13 +1088,7 @@ int is_part_fat16(const partition_t *partition)
break;
}
}
/*
else if(partition->arch==&arch_gpt)
{
if(guid_cmp(partition->part_type_gpt,GPT_ENT_TYPE_MS_BASIC_DATA)==0)
return 1;
}
*/
#endif
return 0;
}
@ -1103,6 +1099,7 @@ static int is_fat16(const partition_t *partition)
int is_part_fat32(const partition_t *partition)
{
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_I386)
if(partition->arch==&arch_i386)
{
switch(partition->part_type_i386)
@ -1116,18 +1113,14 @@ int is_part_fat32(const partition_t *partition)
break;
}
}
else if(partition->arch==&arch_mac)
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_MAC)
if(partition->arch==&arch_mac)
{
if(partition->part_type_mac==PMAC_FAT32)
return 1;
}
/*
else if(partition->arch==&arch_gpt)
{
if(guid_cmp(partition->part_type_gpt,GPT_ENT_TYPE_MS_BASIC_DATA)==0)
return 1;
}
*/
#endif
return 0;
}

5
src/fat_dir.c
View file

@ -64,6 +64,7 @@ struct fat_dir_struct
@ requires \valid_read(fat_header);
@ requires \valid(dir_list);
@ requires \separated(disk_car, partition, dir_data, fat_header, dir_list);
@ decreases 0;
@*/
static int fat1x_rootdir(disk_t *disk_car, const partition_t *partition, const dir_data_t *dir_data, const struct fat_boot_sector*fat_header, file_info_t *dir_list);
@ -109,6 +110,7 @@ int dir_fat_aux(const unsigned char*buffer, const unsigned int size, const unsig
if(wctomb(NULL, 0) < 0)
utf8=0;
#endif
#ifndef DISABLED_FOR_FRAMAC
GetNew:
status=0;
long_slots = 0;
@ -325,6 +327,7 @@ RecEnd:
if((const void *)de<(const void *)(buffer+size-1) &&
de->name[0] != (int8_t) 0)
goto GetNew;
#endif
return 0;
}
@ -351,6 +354,7 @@ static int is_EOC(const unsigned int cluster, const upart_type_t upart_type)
@ requires \valid_read(dir_data);
@ requires \valid(dir_list);
@ requires \separated(disk_car, partition, dir_data, dir_list);
@ decreases 0;
@*/
static int fat_dir(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const unsigned long int first_cluster, file_info_t *dir_list)
{
@ -529,6 +533,7 @@ static void dir_partition_fat_close(dir_data_t *dir_data)
@ requires \valid(dir_data);
@ requires \valid_read(file);
@ requires \separated(disk_car, partition, dir_data, file);
@ decreases 0;
@*/
static int fat_copy(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const file_info_t *file)
{

2
src/fat_unformat.c
View file

@ -55,6 +55,7 @@
#include "fat_common.h"
#include <assert.h>
#ifndef DISABLED_FOR_FRAMAC
extern int need_to_stop;
#define READ_SIZE 4*1024*1024
@ -440,3 +441,4 @@ pstatus_t fat_unformat(struct ph_param *params, const struct ph_options *options
/* start_data is relative to the disk */
return fat_unformat_aux(params, options, start_data, list_search_space);
}
#endif

9
src/fat_unformat.h
View file

@ -25,7 +25,16 @@
extern "C" {
#endif
#ifndef DISABLED_FOR_FRAMAC
/*@
@ requires \valid(params);
@ requires \valid_read(options);
@ requires valid_list_search_space(list_search_space);
@ requires \separated(params, options, list_search_space);
@ ensures valid_list_search_space(list_search_space);
@*/
pstatus_t fat_unformat(struct ph_param *params, const struct ph_options *options, alloc_data_t *list_search_space);
#endif
#ifdef __cplusplus
} /* closing brace for extern "c" */

2
src/fatn.c
View file

@ -24,7 +24,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_NCURSES
#endif

1
src/fatx.h
View file

@ -39,6 +39,7 @@ struct disk_fatx
@ requires valid_disk(disk_car);
@ requires \valid(partition);
@ requires \separated(disk_car, partition);
@ decreases 0;
@*/
int check_FATX(disk_t *disk_car, partition_t *partition);

200
src/fidentify.c
View file

@ -24,7 +24,7 @@
#include <config.h>
#endif
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
#undef HAVE_FTELLO
#endif
@ -66,6 +66,110 @@ extern file_check_list_t file_check_list;
#define OPT_CHECK 1
#define OPT_TIME 2
/*@
@ requires \valid_function(file_recovery->data_check);
@ requires valid_data_check_param(buffer, buffer_size, file_recovery);
@ decreases 0;
@ ensures valid_file_recovery(file_recovery);
@ ensures valid_data_check_result(\result, file_recovery);
@ assigns file_recovery->calculated_file_size, file_recovery->data_check_tmp;
@ assigns file_recovery->data_check, file_recovery->file_check, file_recovery->offset_error, file_recovery->offset_ok, file_recovery->time, file_recovery->data_check_tmp;
@*/
static data_check_t data_check_wrapper(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{
data_check_t tmp;
//@ split file_recovery->data_check;
tmp=file_recovery->data_check(buffer, buffer_size, file_recovery);
/*@ assert valid_data_check_result(tmp, file_recovery); */
return tmp;
}
/*@
@ requires \valid(file_recovery);
@ requires valid_file_recovery(file_recovery);
@ requires \valid_function(file_recovery->data_check);
@ requires 0 < blocksize <= READ_SIZE;
@ requires READ_SIZE % blocksize == 0;
@ requires \valid(buffer_start + (0 .. blocksize + READ_SIZE -1));
@ requires \separated(file_recovery, &errno, buffer_start + (..));
@ decreases 0;
@ ensures valid_file_recovery(file_recovery);
@ assigns *file_recovery->handle, errno;
@ assigns buffer_start[0 .. blocksize + READ_SIZE -1];
@ assigns file_recovery->file_size;
@ assigns file_recovery->calculated_file_size, file_recovery->data_check_tmp;
@ assigns file_recovery->data_check, file_recovery->file_check, file_recovery->offset_error, file_recovery->offset_ok, file_recovery->time, file_recovery->data_check_tmp;
@*/
static data_check_t data_check_aux(file_recovery_t *file_recovery, const unsigned int blocksize, char *buffer_start)
{
/*@ ghost const unsigned int buffer_size=blocksize + READ_SIZE; */
/*@
@ loop invariant valid_file_recovery(file_recovery);
@ loop invariant file_recovery == \at(file_recovery, Pre);
@ loop invariant file_recovery->calculated_file_size < PHOTOREC_MAX_FILE_SIZE;
@ loop invariant \separated(file_recovery, &errno, buffer_start + (..));
@ loop assigns *file_recovery->handle, errno;
@ loop assigns buffer_start[0 .. blocksize + READ_SIZE -1];
@ loop assigns file_recovery->file_size;
@ loop assigns file_recovery->calculated_file_size, file_recovery->data_check_tmp;
@ loop assigns file_recovery->data_check, file_recovery->file_check, file_recovery->offset_error, file_recovery->offset_ok, file_recovery->time, file_recovery->data_check_tmp;
@*/
while(1)
{
char *buffer=buffer_start+blocksize;
unsigned int i;
size_t lu=0;
memset(buffer, 0, READ_SIZE);
lu=fread(buffer, 1, READ_SIZE, file_recovery->handle);
if(lu <= 0)
{
/*@ assert valid_file_recovery(file_recovery); */
return DC_STOP;
}
/*@ assert 0 < lu <= READ_SIZE; */
/*@
@ loop invariant valid_file_recovery(file_recovery);
@ loop invariant file_recovery == \at(file_recovery, Pre);
@ loop invariant \valid_read(buffer_start + (0 .. blocksize + READ_SIZE - 1));
@ loop invariant file_recovery->calculated_file_size < PHOTOREC_MAX_FILE_SIZE;
@ loop invariant \valid_function(file_recovery->data_check);
@ loop invariant \separated(file_recovery, &errno, buffer_start + (..));
@ loop assigns i, file_recovery->file_size;
@ loop assigns file_recovery->calculated_file_size, file_recovery->data_check_tmp;
@ loop assigns file_recovery->data_check, file_recovery->file_check, file_recovery->offset_error, file_recovery->offset_ok, file_recovery->time, file_recovery->data_check_tmp;
@*/
for(i=0; i<lu; i+=blocksize)
{
/*@ assert i + 2*blocksize <= buffer_size; */
/*@ assert \valid_read(&buffer_start[i] + (0 .. 2*blocksize-1)); */
const data_check_t res=data_check_wrapper((const unsigned char *) &buffer_start[i], 2*blocksize, file_recovery);
/*@ assert valid_data_check_result(res, file_recovery); */
/*@ assert \valid_read(&buffer_start[i] + (0 .. 2*blocksize-1)); */
file_recovery->file_size+=blocksize;
if(res != DC_CONTINUE || file_recovery->data_check==NULL)
{
/*@ assert valid_file_recovery(file_recovery); */
return res;
}
if( file_recovery->calculated_file_size >= PHOTOREC_MAX_FILE_SIZE ||
file_recovery->file_size >= PHOTOREC_MAX_FILE_SIZE)
{
/*@ assert valid_file_recovery(file_recovery); */
return DC_STOP;
}
/*@ assert file_recovery->calculated_file_size < PHOTOREC_MAX_FILE_SIZE; */
}
if(lu != READ_SIZE)
{
/*@ assert valid_file_recovery(file_recovery); */
return DC_STOP;
}
memcpy(buffer_start, &buffer_start[READ_SIZE], blocksize);
/*@ assert valid_file_recovery(file_recovery); */
}
/*@ assert valid_file_recovery(file_recovery); */
}
/*@
@ requires \valid(file_recovery);
@ requires valid_file_recovery(file_recovery);
@ -77,70 +181,31 @@ extern file_check_list_t file_check_list;
@*/
static data_check_t data_check(file_recovery_t *file_recovery, const unsigned int blocksize)
{
unsigned char *buffer_start;
char *buffer_start;
const unsigned int buffer_size=blocksize + READ_SIZE;
data_check_t res;
if( file_recovery->calculated_file_size >= PHOTOREC_MAX_FILE_SIZE )
return DC_STOP;
if(my_fseek(file_recovery->handle, 0, SEEK_SET) < 0)
return DC_STOP;
buffer_start=(unsigned char *)MALLOC(buffer_size);
/*@
@ loop invariant valid_file_recovery(file_recovery);
@ loop invariant file_recovery == \at(file_recovery, Pre);
@ loop invariant file_recovery->calculated_file_size < PHOTOREC_MAX_FILE_SIZE;
@*/
while(1)
{
unsigned char *buffer=buffer_start+blocksize;
unsigned int i;
size_t lu;
memset(buffer, 0, READ_SIZE);
lu=fread(buffer, 1, READ_SIZE, file_recovery->handle);
if(lu <= 0)
{
free(buffer_start);
return DC_STOP;
}
/*@ assert 0 < lu <= READ_SIZE; */
/*@
@ loop invariant valid_file_recovery(file_recovery);
@ loop invariant file_recovery == \at(file_recovery, Pre);
@ loop invariant \valid_read(buffer_start + (0 .. blocksize + READ_SIZE - 1));
@ loop invariant file_recovery->calculated_file_size < PHOTOREC_MAX_FILE_SIZE;
@ loop invariant \valid_function(file_recovery->data_check);
@*/
for(i=0; i<lu; i+=blocksize)
{
/*@ assert i + 2*blocksize <= buffer_size; */
/*@ assert \valid_read(&buffer_start[i] + (0 .. 2*blocksize-1)); */
const data_check_t res=file_recovery->data_check(&buffer_start[i], 2*blocksize, file_recovery);
/*@ assert \valid_read(&buffer_start[i] + (0 .. 2*blocksize-1)); */
file_recovery->file_size+=blocksize;
if(res != DC_CONTINUE || file_recovery->data_check==NULL)
{
free(buffer_start);
return res;
}
if( file_recovery->calculated_file_size >= PHOTOREC_MAX_FILE_SIZE ||
file_recovery->file_size >= PHOTOREC_MAX_FILE_SIZE)
{
free(buffer_start);
return DC_STOP;
}
/*@ assert file_recovery->calculated_file_size < PHOTOREC_MAX_FILE_SIZE; */
}
if(lu != READ_SIZE)
{
free(buffer_start);
return DC_STOP;
}
memcpy(buffer_start, &buffer_start[READ_SIZE], blocksize);
/*@ assert valid_file_recovery(file_recovery); */
return DC_STOP;
}
if(my_fseek(file_recovery->handle, 0, SEEK_SET) < 0)
{
/*@ assert valid_file_recovery(file_recovery); */
return DC_STOP;
}
buffer_start=(char *)MALLOC(buffer_size);
res=data_check_aux(file_recovery, blocksize, buffer_start);
/*@ assert valid_file_recovery(file_recovery); */
free(buffer_start);
/*@ assert valid_file_recovery(file_recovery); */
return res;
}
/*@
@ requires valid_read_string(filename);
@ requires \separated(filename + (..), &errno, &Frama_C_entropy_source, stdout);
@ decreases 0;
@*/
static int file_identify(const char *filename, const unsigned int options)
{
@ -194,8 +259,9 @@ static int file_identify(const char *filename, const unsigned int options)
/*TODO assert tmp!=tmp_list; */
const file_check_t *file_check=td_list_entry_const(tmp, const file_check_t, list);
/*@ assert \valid_read(file_check); */
/* TODO assert valid_file_check_node(file_check); */
if(
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
file_check->header_check!=NULL &&
#endif
(file_check->length==0 || memcmp(buffer + file_check->offset, file_check->value, file_check->length)==0) &&
@ -213,7 +279,7 @@ static int file_identify(const char *filename, const unsigned int options)
if(file_recovery_new.file_stat!=NULL &&
file_recovery_new.file_stat->file_hint!=NULL &&
(file_recovery_new.file_check!=NULL || file_recovery_new.data_check!=NULL) &&
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
file_recovery_new.extension != NULL &&
#endif
((options&OPT_CHECK)!=0 || ((options&OPT_TIME)!=0 && file_recovery_new.time==0))
@ -269,14 +335,14 @@ static int file_identify(const char *filename, const unsigned int options)
if((options&OPT_CHECK)!=0 && (file_recovery_new.file_check!=NULL || file_recovery_new.data_check!=NULL))
printf(" file_size=%llu", (long long unsigned)file_recovery_new.file_size);
if((options&OPT_TIME)!=0 && file_recovery_new.time!=0 && file_recovery_new.time!=(time_t)-1)
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
{
printf(" time=%lld", (long long)file_recovery_new.time);
}
#else
{
char outstr[200];
#if defined(__MINGW32__) || defined(__FRAMAC__)
#if defined(__MINGW32__) || defined(DISABLED_FOR_FRAMAC)
const struct tm *tmp = localtime(&file_recovery_new.time);
#else
struct tm tm_tmp;
@ -306,7 +372,7 @@ static int file_identify(const char *filename, const unsigned int options)
return 0;
}
#if !defined(__AFL_COMPILER) && !defined(MAIN_fidentify)
#if !defined(__AFL_COMPILER) && !defined(DISABLED_FOR_FRAMAC)
static void file_identify_dir(const char *current_dir, const unsigned int options)
{
DIR *dir;
@ -359,7 +425,7 @@ static void display_version(void)
#ifdef RECORD_COMPILATION_DATE
printf("Compilation date: %s\n", get_compilation_date());
#endif
#ifndef MAIN_fidentify
#ifndef DISABLED_FOR_FRAMAC
printf("libjpeg: %s, zlib: %s\n", td_jpeg_version(), td_zlib_version());
printf("OS: %s\n" , get_os());
#endif
@ -368,7 +434,7 @@ static void display_version(void)
int main(int argc, char **argv)
{
int i;
#ifdef MAIN_fidentify
#ifdef DISABLED_FOR_FRAMAC
unsigned int options=OPT_CHECK|OPT_TIME;
#else
unsigned int options=0;
@ -378,7 +444,7 @@ int main(int argc, char **argv)
int scan_dir=1;
file_stat_t *file_stats;
log_set_levels(LOG_LEVEL_DEBUG|LOG_LEVEL_TRACE|LOG_LEVEL_QUIET|LOG_LEVEL_INFO|LOG_LEVEL_VERBOSE|LOG_LEVEL_PROGRESS|LOG_LEVEL_WARNING|LOG_LEVEL_ERROR|LOG_LEVEL_PERROR|LOG_LEVEL_CRITICAL);
#ifndef MAIN_fidentify
#ifndef DISABLED_FOR_FRAMAC
for(i=1; i<argc; i++)
{
if( strcmp(argv[i], "/check")==0 || strcmp(argv[i], "-check")==0 || strcmp(argv[i], "--check")==0)
@ -412,7 +478,7 @@ int main(int argc, char **argv)
log_info("\n\n%s",ctime(&my_time));
}
log_info("Command line: fidentify");
#ifndef MAIN_fidentify
#ifndef DISABLED_FOR_FRAMAC
for(i=1;i<argc;i++)
log_info(" %s", argv[i]);
#endif
@ -420,7 +486,7 @@ int main(int argc, char **argv)
log_info("fidentify %s, Data Recovery Utility, %s\nChristophe GRENIER <grenier@cgsecurity.org>\nhttps://www.cgsecurity.org\n", VERSION, TESTDISKDATE);
log_flush();
#endif
#ifndef MAIN_fidentify
#ifndef DISABLED_FOR_FRAMAC
for(i=1; i<argc; i++)
{
file_enable_t *file_enable;
@ -442,7 +508,7 @@ int main(int argc, char **argv)
file_enable->enable=1;
}
file_stats=init_file_stats(array_file_enable);
#ifndef MAIN_fidentify
#ifndef DISABLED_FOR_FRAMAC
for(i=1; i<argc; i++)
{
if(strcmp(argv[i], "/check")==0 || strcmp(argv[i], "-check")==0 || strcmp(argv[i], "--check")==0 ||

2
src/file_asf.c
View file

@ -112,7 +112,7 @@ static int header_check_asf(const unsigned char *buffer, const unsigned int buff
};
if(object_size < 0x18)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("header_check_asf object_size too small %llu\n", (long long unsigned)object_size);
#endif
return 0;

2
src/file_bac.c
View file

@ -85,7 +85,7 @@ static data_check_t data_check_bac(const unsigned char *buffer, const unsigned i
#endif
if(memcmp(hdr->ID, "BB02", 4)!=0 || block_size<0x18)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_error("file_bac.c: invalid block at %llu\n",
(long long unsigned)file_recovery->calculated_file_size);
#endif

2
src/file_bdm.c
View file

@ -59,7 +59,7 @@ static int header_check_bdm(const unsigned char *buffer, const unsigned int buff
static void register_header_check_bdm(file_stat_t *file_stat)
{
register_header_check(0, "INDX0100", 8, &header_check_bdm, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, "MOBJ0100", 8, &header_check_bdm, file_stat);
#endif
}

2
src/file_berkeley.c
View file

@ -76,7 +76,7 @@ static void register_header_check_berkeley_le(file_stat_t *file_stat)
static unsigned char berkeley_db_btree_8[8]={0x62, 0x31, 0x05, 0x00, 0x08, 0x00, 0x00, 0x00};
static unsigned char berkeley_db_btree_9[8]={0x62, 0x31, 0x05, 0x00, 0x09, 0x00, 0x00, 0x00};
register_header_check(0xC, berkeley_db_hash_8, 8, &header_check_berkeley_le, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0xC, berkeley_db_hash_9, 8, &header_check_berkeley_le, file_stat);
register_header_check(0xC, berkeley_db_btree_8, 8, &header_check_berkeley_le, file_stat);
register_header_check(0xC, berkeley_db_btree_9, 8, &header_check_berkeley_le, file_stat);

2
src/file_crw.c
View file

@ -81,7 +81,7 @@ static void register_header_check_crw(file_stat_t *file_stat)
static const unsigned char crw_header_be[2]= {'I','I'};
static const unsigned char crw_header_le[2]= {'M','M'};
register_header_check(0, crw_header_be, sizeof(crw_header_be), &header_check_crw, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, crw_header_le, sizeof(crw_header_le), &header_check_crw, file_stat);
#endif
}

4
src/file_dir.c
View file

@ -20,7 +20,7 @@
*/
#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_dir) || defined(MAIN_photorec)
#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_dir)
#ifdef HAVE_CONFIG_H
#include <config.h>
#endif
@ -69,7 +69,7 @@ static void file_rename_fatdir(file_recovery_t *file_recovery)
/*@ assert buffer_size >= 32; */
cluster=fat_get_cluster_from_entry((const struct msdos_dir_entry *)&buffer[0]);
sprintf(buffer_cluster, "cluster_%u", cluster);
#if defined(__FRAMAC__)
#if defined(DISABLED_FOR_FRAMAC)
buffer_cluster[sizeof(buffer_cluster)-1]='\0';
#endif
file_rename(file_recovery, buffer_cluster, strlen(buffer_cluster), 0, NULL, 1);

18
src/file_doc.c
View file

@ -142,7 +142,7 @@ static uint32_t *OLE_load_FAT(FILE *IN, const struct OLE_HDR *header, const uint
/*@ assert uSectorShift == le16(header->uSectorShift); */
/*@ assert num_FAT_blocks==le32(header->num_FAT_blocks); */
/*@ assert num_FAT_blocks <= 109+le32(header->num_extra_FAT_blocks)*((1<<uSectorShift)/4-1); */
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
const unsigned int dif_size=109*4+(50<<12);
#else
const unsigned int dif_size=109*4+(num_extra_FAT_blocks<<uSectorShift);
@ -171,7 +171,7 @@ static uint32_t *OLE_load_FAT(FILE *IN, const struct OLE_HDR *header, const uint
}
}
}
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
/*@ assert (109+50*((1<<12)/4-1))<<12 >= num_FAT_blocks<<uSectorShift; */
fat=(uint32_t*)MALLOC((109+50*((1<<12)/4-1))<<12);
#else
@ -307,7 +307,7 @@ void file_check_doc_aux(file_recovery_t *file_recovery, const uint64_t offset)
free(fat);
return ;
}
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
dir_entries=(struct OLE_DIR *)MALLOC(1<<12);
#else
dir_entries=(struct OLE_DIR *)MALLOC(1<<uSectorShift);
@ -655,7 +655,7 @@ static void *OLE_read_stream(FILE *IN,
unsigned int block;
unsigned int i;
const unsigned int i_max=((len+(1<<uSectorShift)-1) >> uSectorShift);
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
dataPt=(char *)MALLOC(((1024*1024+(1<<uSectorShift)-1) >> uSectorShift) << uSectorShift);
#else
dataPt=(char *)MALLOC(i_max << uSectorShift);
@ -712,7 +712,7 @@ static uint32_t *OLE_load_MiniFAT(FILE *IN, const struct OLE_HDR *header, const
return NULL;
/*@ assert 0 < csectMiniFat; */
/*@ assert 0 < csectMiniFat <= 2048; */
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
minifat=(char *)MALLOC(2048 << 12);
#else
minifat=(char *)MALLOC(minifat_length);
@ -1067,7 +1067,7 @@ static void OLE_parse_title_entry(const char *buffer, const unsigned int size, c
/*@ assert \valid_read((char*)(src + offset_tmp)) && \valid_read(((char*)(src+offset_tmp))+(1..count-1)); */
/*@ assert valid_read_or_empty((void const *)(src + offset_tmp), count); */
/*@ assert valid_read_or_empty((void const *)(src + offset_tmp), count); */
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
if(count < 1024)
{
memcpy(title, &src[offset_tmp], count);
@ -1300,7 +1300,7 @@ static void OLE_parse_summary_aux(const char *dataPt, const unsigned int dirLen,
{
unsigned int pos;
const unsigned char *udataPt=(const unsigned char *)dataPt;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
assert(dirLen >= 48 && dirLen<=1024*1024);
#endif
/*@ assert *ext == \null || valid_read_string(*ext); */
@ -1367,7 +1367,7 @@ static void *OLE_read_ministream(const unsigned char *ministream,
unsigned char *dataPt;
unsigned int mblock=miniblock_start;
unsigned int size_read;
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
const unsigned int len_aligned=(1024*1024+(1<<uMiniSectorShift)-1) / (1<<uMiniSectorShift) * (1<<uMiniSectorShift);
#else
const unsigned int len_aligned=(len+(1<<uMiniSectorShift)-1) / (1<<uMiniSectorShift) * (1<<uMiniSectorShift);
@ -1576,7 +1576,7 @@ static void file_rename_doc(file_recovery_t *file_recovery)
{
/*@ assert valid_string(&title[0]); */
struct OLE_DIR *dir_entries;
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
dir_entries=(struct OLE_DIR *)MALLOC(1<<12);
#else
dir_entries=(struct OLE_DIR *)MALLOC(1<<uSectorShift);

2
src/file_dpx.c
View file

@ -97,7 +97,7 @@ static int header_check_dpx(const unsigned char *buffer, const unsigned int buff
static void register_header_check_dpx(file_stat_t *file_stat)
{
register_header_check(0, "SDPX", 4, &header_check_dpx, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, "XPDS", 4, &header_check_dpx, file_stat);
#endif
}

2
src/file_dta.c
View file

@ -71,7 +71,7 @@ static void register_header_check_dta(file_stat_t *file_stat)
static const unsigned char dta_header_71le[3]= {0x71, 0x02, 0x01};
static const unsigned char dta_header_72le[3]= {0x72, 0x02, 0x01};
register_header_check(0, dta_header_71le,sizeof(dta_header_71le), &header_check_dta, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, dta_header_72le,sizeof(dta_header_72le), &header_check_dta, file_stat);
#endif
}

2
src/file_dump.c
View file

@ -152,7 +152,7 @@ static void register_header_check_dump(file_stat_t *file_stat)
static const unsigned char dump_header_le_old_fs[4] = { 0x6b, 0xea, 0x00, 0x00};
static const unsigned char dump_header_le_new_fs[4] = { 0x6c, 0xea, 0x00, 0x00};
register_header_check(0x18, dump_header_le_old_fs,sizeof(dump_header_le_old_fs), &header_check_dump, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0x18, dump_header_le_new_fs,sizeof(dump_header_le_new_fs), &header_check_dump, file_stat);
#endif
}

2
src/file_dwg.c
View file

@ -68,7 +68,7 @@ static void register_header_check_dwg(file_stat_t *file_stat)
static const unsigned char dwg_header_24[11]= {'A', 'C', '1', '0', '2', '4', 0x00, 0x00, 0x00, 0x00, 0x00};
static const unsigned char dwg_header_27[11]= {'A', 'C', '1', '0', '2', '7', 0x00, 0x00, 0x00, 0x00, 0x00};
register_header_check(0, dwg_header_12,sizeof(dwg_header_12), &header_check_dwg, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, dwg_header_13,sizeof(dwg_header_13), &header_check_dwg, file_stat);
register_header_check(0, dwg_header_14,sizeof(dwg_header_14), &header_check_dwg, file_stat);
register_header_check(0, dwg_header_15,sizeof(dwg_header_15), &header_check_dwg, file_stat);

2
src/file_dxf.c
View file

@ -112,7 +112,7 @@ static void register_header_check_dxf(file_stat_t *file_stat)
'S', 'E', 'C', 'T', 'I', 'O', 'N'};
register_header_check(0, header_dxf, sizeof(header_dxf), &header_check_dxf, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, header_dxf_dos, sizeof(header_dxf_dos), &header_check_dxf, file_stat);
register_header_check(0, header_dxflib, sizeof(header_dxflib), &header_check_dxf, file_stat);
register_header_check(0, header_dxflib_dos, sizeof(header_dxflib_dos), &header_check_dxf, file_stat);

6
src/file_exe.c
View file

@ -428,7 +428,7 @@ static void pe_resource_language(FILE *file, const unsigned int base, const unsi
if(count==0 || count > 1024)
return ;
/*@ assert 0 < count <= 1024; */
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
rsrc_entries=(struct rsrc_entries_s *)MALLOC(1024 * sizeof(struct rsrc_entries_s));
#else
rsrc_entries=(struct rsrc_entries_s *)MALLOC(count * sizeof(struct rsrc_entries_s));
@ -489,7 +489,7 @@ static void pe_resource_id(FILE *file, const unsigned int base, const unsigned i
if(count==0 || count > 1024)
return ;
/*@ assert 0 < count <= 1024; */
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
rsrc_entries=(struct rsrc_entries_s *)MALLOC(1024 * sizeof(struct rsrc_entries_s));
#else
rsrc_entries=(struct rsrc_entries_s *)MALLOC(count * sizeof(struct rsrc_entries_s));
@ -559,7 +559,7 @@ static void pe_resource_type(FILE *file, const unsigned int base, const unsigned
if(count==0 || count > 1024)
return ;
/*@ assert 0 < count <= 1024; */
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
rsrc_entries=(struct rsrc_entries_s *)MALLOC(1024 * sizeof(struct rsrc_entries_s));
#else
rsrc_entries=(struct rsrc_entries_s *)MALLOC(count * sizeof(struct rsrc_entries_s));

4
src/file_ext.c
View file

@ -72,7 +72,7 @@ static void file_rename_ext(file_recovery_t *file_recovery)
/*@ assert \initialized(buffer + (0 .. sizeof(buffer)-1)); */
block_nr=(unsigned long int)le32(sb->s_first_data_block) + (unsigned long int)le16(sb->s_block_group_nr)*le32(sb->s_blocks_per_group);
sprintf(buffer_cluster, "sb_%lu", block_nr);
#if defined(__FRAMAC__)
#if defined(DISABLED_FOR_FRAMAC)
buffer_cluster[sizeof(buffer_cluster)-1]='\0';
#endif
file_rename(file_recovery, buffer_cluster, strlen(buffer_cluster), 0, NULL, 1);
@ -136,7 +136,7 @@ static void file_rename_extdir(file_recovery_t *file_recovery)
#endif
/*@ assert \initialized(buffer + (0 .. sizeof(buffer)-1)); */
sprintf(buffer_cluster, "inode_%u", (unsigned int)le32(*inode));
#if defined(__FRAMAC__)
#if defined(DISABLED_FOR_FRAMAC)
buffer_cluster[sizeof(buffer_cluster)-1]='\0';
#endif
file_rename(file_recovery, buffer_cluster, strlen(buffer_cluster), 0, NULL, 1);

2
src/file_flac.c
View file

@ -111,7 +111,7 @@ static void register_header_check_flac(file_stat_t *file_stat)
static const unsigned char flac_header[5]= {'f', 'L', 'a', 'C', 0x00};
static const unsigned char flac_header2[5]= {'f', 'L', 'a', 'C', 0x80};
register_header_check(0, flac_header,sizeof(flac_header), &header_check_flac, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, flac_header2,sizeof(flac_header2), &header_check_flac, file_stat);
#endif
}

2
src/file_fob.c
View file

@ -73,7 +73,7 @@ static int header_check_fob(const unsigned char *buffer, const unsigned int buff
static void register_header_check_fob(file_stat_t *file_stat)
{
register_header_check(0, "Codeunit ", 9, &header_check_fob, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, "Dataport ", 9, &header_check_fob, file_stat);
register_header_check(0, "Form ", 5, &header_check_fob, file_stat);
register_header_check(0, "MenuSuite ", 10, &header_check_fob, file_stat);

2
src/file_gif.c
View file

@ -210,7 +210,7 @@ static void register_header_check_gif(file_stat_t *file_stat)
static const unsigned char gif_header[6]= { 'G','I','F','8','7','a'};
static const unsigned char gif_header2[6]= { 'G','I','F','8','9','a'};
register_header_check(0, gif_header,sizeof(gif_header), &header_check_gif, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, gif_header2,sizeof(gif_header2), &header_check_gif, file_stat);
#endif
}

2
src/file_gpg.c
View file

@ -788,7 +788,7 @@ static void register_header_check_gpg(file_stat_t *file_stat)
static const unsigned char gpg_header_seckey[1]= {0x95};
static const unsigned char gpg_header_pkey[1]= {0x99};
register_header_check(0, gpg_header_seckey, sizeof(gpg_header_seckey), &header_check_gpg, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, gpg_header_symkey_enc, sizeof(gpg_header_symkey_enc), &header_check_gpg, file_stat);
register_header_check(0, gpg_header_pkey_enc, sizeof(gpg_header_pkey_enc), &header_check_gpg, file_stat);
register_header_check(0, pgp_header, sizeof(pgp_header), &header_check_gpg, file_stat);

2
src/file_gsm.c
View file

@ -137,7 +137,7 @@ static void register_header_check_gsm(file_stat_t *file_stat)
static const unsigned char gsm_header16[1]={ 0xdf };
register_header_check(0, gsm_header1, sizeof(gsm_header1), &header_check_gsm, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, gsm_header2, sizeof(gsm_header2), &header_check_gsm, file_stat);
register_header_check(0, gsm_header3, sizeof(gsm_header3), &header_check_gsm, file_stat);
register_header_check(0, gsm_header4, sizeof(gsm_header4), &header_check_gsm, file_stat);

2
src/file_gz.c
View file

@ -24,7 +24,7 @@
#include <config.h>
#endif
#if defined(MAIN_fidentify) || defined(MAIN_photorec) || defined(__FRAMAC__)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_LIBZ
#undef HAVE_ZLIB_H
#endif

2
src/file_hfsp.c
View file

@ -65,7 +65,7 @@ static int header_check_hfsp(const unsigned char *buffer, const unsigned int buf
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__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, "HX\0\5", 4, &header_check_hfsp, file_stat);
#endif
}

2
src/file_ibd.c
View file

@ -50,7 +50,7 @@ const file_hint_t file_hint_ibd= {
#define FIL_PAGE_TYPE_FSP_HDR 8 /* File space header */
#define DICT_TF_BITS 6 /* number of flag bits */
#define DICT_TF_FORMAT_SHIFT 5 /* file format */
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
#define DICT_TF_FORMAT_MASK 0x20
#else
#define DICT_TF_FORMAT_MASK \

2
src/file_ico.c
View file

@ -158,7 +158,7 @@ static int header_check_ico(const unsigned char *buffer, const unsigned int buff
static void register_header_check_ico(file_stat_t *file_stat)
{
register_header_check(0, header_ico1, sizeof(header_ico1), &header_check_ico, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, header_ico2, sizeof(header_ico2), &header_check_ico, file_stat);
register_header_check(0, header_ico3, sizeof(header_ico3), &header_check_ico, file_stat);
register_header_check(0, header_ico4, sizeof(header_ico4), &header_check_ico, file_stat);

2
src/file_ifo.c
View file

@ -74,7 +74,7 @@ static void register_header_check_ifo(file_stat_t *file_stat)
static const unsigned char ifo_header_vmg[12]= { 'D', 'V', 'D', 'V', 'I', 'D', 'E', 'O', '-', 'V', 'M', 'G'};
static const unsigned char ifo_header_vts[12]= { 'D', 'V', 'D', 'V', 'I', 'D', 'E', 'O', '-', 'V', 'T', 'S'};
register_header_check(0, ifo_header_vmg, sizeof(ifo_header_vmg), &header_check_ifo, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, ifo_header_vts, sizeof(ifo_header_vts), &header_check_ifo, file_stat);
#endif
}

41
src/file_jpg.c
View file

@ -25,7 +25,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(SINGLE_FORMAT) || defined(MAIN_fidentify)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_LIBJPEG
#undef DEBUG_JPEG
#undef HAVE_JPEGLIB_H
@ -756,7 +756,7 @@ static void file_check_mpo(file_recovery_t *fr)
}
if(file_check_mpo_aux(fr->handle, buffer+8, offset+8, size-8) == 0)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("file_check_mpo %s failed, limiting to first jpeg: %llu\n", fr->filename, (long long unsigned)jpg_fs);
#endif
fr->file_size=jpg_fs;
@ -925,7 +925,7 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff
if( file_recovery->file_size <= 1024 &&
buffer[3]==0xec) /* APP12 */
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("jpg %llu %llu\n",
(long long unsigned)file_recovery->calculated_file_size,
(long long unsigned)file_recovery->file_size);
@ -1986,7 +1986,7 @@ static void jpg_search_marker(file_recovery_t *file_recovery)
)
{
file_recovery->extra=tmp - offset_error;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
if(file_recovery->extra % file_recovery->blocksize != 0)
{
log_info("jpg_search_marker %s extra=%llu\n",
@ -2022,16 +2022,16 @@ static void jpg_save_thumbnail(const file_recovery_t *file_recovery, const char
/*@ assert valid_read_string(&thumbname[0]); */
sep=strrchr(thumbname,'/');
if(sep!=NULL
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
&& *(sep+1)=='f'
#endif
)
{
FILE *out;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
*(sep+1)='t';
#endif
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
if((out=fopen(thumbname,"wb"))!=NULL)
{
/*@ assert \valid_read(buffer + (0 .. nbytes - 1)); */
@ -2047,7 +2047,7 @@ static void jpg_save_thumbnail(const file_recovery_t *file_recovery, const char
/*@ assert \valid_read(thumb_char + (0 .. thumb_size - 1)); */
if(fwrite(&buffer[thumb_offset], thumb_size, 1, out) < 1)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_error("Can't write to %s: %s\n", thumbname, strerror(errno));
#endif
}
@ -2057,7 +2057,7 @@ static void jpg_save_thumbnail(const file_recovery_t *file_recovery, const char
}
else
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_error("fopen %s failed\n", thumbname);
#endif
}
@ -2221,7 +2221,7 @@ static int jpg_check_app1(file_recovery_t *file_recovery, const unsigned int ext
}
else
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("%s thumb unknown marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j);
#endif
file_recovery->offset_error=j;
@ -2703,6 +2703,16 @@ static data_check_t data_check_jpg(const unsigned char *buffer, const unsigned i
return DC_CONTINUE;
}
/*@
@ requires valid_register_header_check(file_stat);
@*/
static void register_header_check_jpg(file_stat_t *file_stat)
{
static const unsigned char jpg_header[3]= { 0xff,0xd8,0xff};
register_header_check(0, jpg_header, sizeof(jpg_header), &header_check_jpg, file_stat);
}
#endif
const char*td_jpeg_version(void)
{
#if defined(HAVE_LIBJPEG)
@ -2724,17 +2734,6 @@ const char*td_jpeg_version(void)
#endif
}
/*@
@ requires valid_register_header_check(file_stat);
@*/
static void register_header_check_jpg(file_stat_t *file_stat)
{
static const unsigned char jpg_header[3]= { 0xff,0xd8,0xff};
register_header_check(0, jpg_header, sizeof(jpg_header), &header_check_jpg, file_stat);
}
#endif
#if defined(MAIN_jpg)
#define BLOCKSIZE 65536u
int main()

6
src/file_lzh.c
View file

@ -57,7 +57,7 @@ struct lzh_level0
uint8_t level;
uint8_t filename_len;
/* Size should be 0, be carefull when using sizeof to decrement */
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
uint8_t filename[0];
#endif
} __attribute__ ((gcc_struct, __packed__));
@ -73,7 +73,7 @@ struct lzh_level1
uint8_t reserved_20;
uint8_t level;
uint8_t filename_len;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
uint8_t filename[0];
#endif
} __attribute__ ((gcc_struct, __packed__));
@ -171,7 +171,7 @@ static int header_check_lzh(const unsigned char *buffer, const unsigned int buff
static void register_header_check_lzh(file_stat_t *file_stat)
{
register_header_check(2, "-lh0-", 5, &header_check_lzh, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(2, "-lh1-", 5, &header_check_lzh, file_stat);
register_header_check(2, "-lh2-", 5, &header_check_lzh, file_stat);
register_header_check(2, "-lh3-", 5, &header_check_lzh, file_stat);

4
src/file_m2ts.c
View file

@ -105,7 +105,7 @@ static void file_rename_ts_188(file_recovery_t *file_recovery)
#endif
pid=((buffer[1]<<8)|buffer[2])&0x1fff;
sprintf(buffer_pid, "pid_%u", pid);
#if defined(__FRAMAC__)
#if defined(DISABLED_FOR_FRAMAC)
buffer_pid[sizeof(buffer_pid)-1]='\0';
#endif
file_rename(file_recovery, (const unsigned char*)buffer_pid, strlen(buffer_pid), 0, NULL, 1);
@ -136,7 +136,7 @@ static void file_rename_ts_192(file_recovery_t *file_recovery)
#endif
pid=((buffer[5]<<8)|buffer[6])&0x1fff;
sprintf(buffer_pid, "pid_%u", pid);
#if defined(__FRAMAC__)
#if defined(DISABLED_FOR_FRAMAC)
buffer_pid[sizeof(buffer_pid)-1]='\0';
#endif
file_rename(file_recovery, (const unsigned char*)buffer_pid, strlen(buffer_pid), 0, NULL, 1);

2
src/file_mft.c
View file

@ -67,7 +67,7 @@ static void file_rename_mft(file_recovery_t *file_recovery)
#endif
/*@ assert \initialized(buffer + (0 .. sizeof(buffer)-1)); */
sprintf(buffer_cluster, "record_%u", (unsigned int)le32(record->mft_record_number));
#if defined(__FRAMAC__)
#if defined(DISABLED_FOR_FRAMAC)
buffer_cluster[sizeof(buffer_cluster)-1]='\0';
#endif
file_rename(file_recovery, buffer_cluster, strlen(buffer_cluster), 0, NULL, 1);

2
src/file_mig.c
View file

@ -55,7 +55,7 @@ struct MIG_HDR
uint32_t unk1;
uint32_t unk2;
uint32_t unk3;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
unsigned char fn[0];
#endif
} __attribute__ ((gcc_struct, __packed__));

2
src/file_mlv.c
View file

@ -175,7 +175,7 @@ static void file_rename_mlv(file_recovery_t *file_recovery)
}
fclose(file);
sprintf(ext, "M%02u", le16(hdr->fileNum));
#if defined(__FRAMAC__)
#if defined(DISABLED_FOR_FRAMAC)
ext[sizeof(ext)-1]='\0';
#endif
/*@ assert valid_read_string(ext_ptr); */

4
src/file_mov.c
View file

@ -198,7 +198,7 @@ static data_check_t data_check_mov(const unsigned char *buffer, const unsigned i
}
else
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
if(!(buffer[i+4]==0 && buffer[i+5]==0 && buffer[i+6]==0 && buffer[i+7]==0))
log_warning("file_mov.c: unknown atom 0x%02x%02x%02x%02x at %llu\n",
buffer[i+4],buffer[i+5],buffer[i+6],buffer[i+7],
@ -523,7 +523,7 @@ static void register_header_check_mov_mdat(file_stat_t *file_stat)
static void register_header_check_mov(file_stat_t *file_stat)
{
register_header_check(4, (const unsigned char*)"cmov",4, &header_check_mov, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(4, (const unsigned char*)"cmvd",4, &header_check_mov, file_stat);
register_header_check(4, (const unsigned char*)"dcom",4, &header_check_mov, file_stat);
register_header_check(4, (const unsigned char*)"free",4, &header_check_mov, file_stat);

2
src/file_msa.c
View file

@ -85,7 +85,7 @@ static void register_header_check_msa(file_stat_t *file_stat)
0xfc, 0xff, 0xff, 0xff
};
register_header_check(0, msa_header_fb, sizeof(msa_header_fb), &header_check_msa, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, msa_header_fc, sizeof(msa_header_fc), &header_check_msa, file_stat);
#endif
}

2
src/file_mxf.c
View file

@ -64,7 +64,7 @@ struct partition_pack_next
uint64_t body_offset;
uint32_t body_SID;
char op_pattern[16];
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
char essence_container[0];
#endif
} __attribute__ ((gcc_struct, __packed__));

2
src/file_pcap.c
View file

@ -65,7 +65,7 @@ static void register_header_check_pcap(file_stat_t *file_stat)
static const unsigned char pcap_le_header1[6] = {0xd4, 0xc3, 0xb2, 0xa1, 0x01, 0x00};
static const unsigned char pcap_le_header2[6] = {0xd4, 0xc3, 0xb2, 0xa1, 0x02, 0x00};
register_header_check(0, pcap_le_header1, sizeof(pcap_le_header1), &header_check_pcap, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, pcap_le_header2, sizeof(pcap_le_header2), &header_check_pcap, file_stat);
#endif
}

2
src/file_pyc.c
View file

@ -88,7 +88,7 @@ static void register_header_check_pyc(file_stat_t *file_stat)
static const unsigned char pyc_33_magic[4]= { 0x9e, 0x0c, '\r', '\n'};
static const unsigned char pyc_34_magic[4]= { 0xee, 0x0c, '\r', '\n'};
register_header_check(0, pyc_15_magic, sizeof(pyc_15_magic), &header_check_pyc, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, pyc_20_magic, sizeof(pyc_20_magic), &header_check_pyc, file_stat);
register_header_check(0, pyc_21_magic, sizeof(pyc_21_magic), &header_check_pyc, file_stat);
register_header_check(0, pyc_22_magic, sizeof(pyc_22_magic), &header_check_pyc, file_stat);

648
src/file_sig.c
View file

@ -65,11 +65,23 @@ struct signature_s
{
struct td_list_head list;
const char *extension;
unsigned char *sig;
const unsigned char *sig;
unsigned int sig_size;
unsigned int offset;
};
/*@
predicate valid_signature(signature_t *sig) = (\valid_read(sig) &&
valid_read_string(sig->extension) &&
\initialized(&sig->offset) &&
\initialized(&sig->sig_size) &&
sig->offset <= PHOTOREC_MAX_SIG_OFFSET &&
0 < sig->sig_size <= PHOTOREC_MAX_SIG_SIZE &&
sig->offset + sig->sig_size <= PHOTOREC_MAX_SIG_OFFSET &&
\valid_read((const char *)sig->sig+(0..sig->sig_size-1))
);
@*/
static signature_t signatures={
.list = TD_LIST_HEAD_INIT(signatures.list)
};
@ -82,6 +94,8 @@ int signature_cmp(const struct td_list_head *a, const struct td_list_head *b)
const signature_t *sig_a=td_list_entry_const(a, const signature_t, list);
const signature_t *sig_b=td_list_entry_const(b, const signature_t, list);
int res;
/*@ assert valid_signature(sig_a); */
/*@ assert valid_signature(sig_b); */
if(sig_a->sig_size==0 && sig_b->sig_size!=0)
return -1;
if(sig_a->sig_size!=0 && sig_b->sig_size==0)
@ -105,27 +119,64 @@ int signature_cmp(const struct td_list_head *a, const struct td_list_head *b)
}
}
static void signature_insert(const char *extension, unsigned int offset, unsigned char *sig, unsigned int sig_size)
/*@
@ requires offset <= PHOTOREC_MAX_SIG_OFFSET;
@ requires 0 < sig_size <= PHOTOREC_MAX_SIG_SIZE;
@ requires offset + sig_size <= PHOTOREC_MAX_SIG_OFFSET;
@ requires \valid_read((const char *)sig + (0 .. sig_size-1));
@ requires valid_read_string(ext);
@*/
static void signature_insert(const char *ext, unsigned int offset, const void*sig, unsigned int sig_size)
{
/* FIXME: small memory leak */
signature_t *newsig=(signature_t*)MALLOC(sizeof(*newsig));
newsig->extension=extension;
newsig->sig=sig;
/* FIXME: memory leak for newsig */
signature_t *newsig;
/*@ assert \valid_read((const char *)sig+(0..sig_size-1)); */
/*@ assert valid_read_string(ext); */
newsig=(signature_t*)MALLOC(sizeof(*newsig));
newsig->extension=ext;
newsig->sig=(const unsigned char *)sig;
newsig->sig_size=sig_size;
newsig->offset=offset;
/*@ assert newsig->sig_size == sig_size; */
/*@ assert \valid_read(newsig); */
/*@ assert valid_read_string(newsig->extension); */
/*@ assert \initialized(&newsig->offset); */
/*@ assert \initialized(&newsig->sig_size); */
/*@ assert newsig->offset <= PHOTOREC_MAX_SIG_OFFSET; */
/*@ assert 0 < newsig->sig_size <= PHOTOREC_MAX_SIG_SIZE; */
/*@ assert newsig->offset + newsig->sig_size <= PHOTOREC_MAX_SIG_OFFSET; */
/*@ assert \valid_read((const char *)sig+(0..sig_size-1)); */
/*@ assert \valid_read((const char *)sig+(0..newsig->sig_size-1)); */
/*@ assert (const char *)newsig->sig ==(const char *)sig; */
/*@ assert \valid_read((const char *)newsig->sig+(0..0)); */
/*@ assert \valid_read((const char *)newsig->sig+(0..newsig->sig_size-1)); */
/*@ assert valid_signature(newsig); */
td_list_add_sorted(&newsig->list, &signatures.list, signature_cmp);
}
/*@
@ requires separation: \separated(&file_hint_sig, 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);
@ assigns *file_recovery_new;
@*/
static int header_check_sig(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)
{
struct td_list_head *pos;
/*@ loop assigns pos; */
td_list_for_each(pos, &signatures.list)
{
const signature_t *sig = td_list_entry(pos, signature_t, list);
/*@ assert sig->offset + sig->sig_size <= buffer_size; */
/*@ assert valid_read_string(sig->extension); */
/*@ assert valid_signature(sig); */
if(memcmp(&buffer[sig->offset], sig->sig, sig->sig_size)==0)
{
reset_file_recovery(file_recovery_new);
file_recovery_new->extension=sig->extension;
/*@ assert valid_file_recovery(file_recovery_new); */
return 1;
}
}
@ -164,13 +215,27 @@ static FILE *open_signature_file(void)
if (home != NULL)
{
FILE*handle;
char *filename=(char*)MALLOC(strlen(home)+strlen(DOT_PHOTOREC_SIG)+1);
char *filename;
size_t len_home;
const size_t len_sig=strlen(DOT_PHOTOREC_SIG);
size_t fn_size=len_sig;
#ifndef DISABLED_FOR_FRAMAC
len_home=strlen(home);
fn_size+=len_home;
#endif
filename=(char*)MALLOC(fn_size + 1);
#ifndef DISABLED_FOR_FRAMAC
strcpy(filename, home);
#else
filename[0]='\0';
#endif
strcat(filename, DOT_PHOTOREC_SIG);
handle=fopen(filename,"rb");
if(handle!=NULL)
{
#ifndef DISABLED_FOR_FRAMAC
log_info("Open signature file %s\n", filename);
#endif
free(filename);
return handle;
}
@ -182,241 +247,385 @@ static FILE *open_signature_file(void)
FILE *handle=fopen(PHOTOREC_SIG,"rb");
if(handle!=NULL)
{
#ifndef DISABLED_FOR_FRAMAC
log_info("Open signature file %s\n", PHOTOREC_SIG);
#endif
return handle;
}
}
return NULL;
}
static char *str_uint(char *src, unsigned int *resptr)
/*@
@ requires \valid(ptr);
@ requires valid_read_string(*ptr);
@ ensures \initialized(ptr);
@ ensures valid_read_string(*ptr);
@ assigns *ptr;
@*/
static unsigned int str_uint_hex(char **ptr)
{
char *src=*ptr;
unsigned int res=0;
if(*src=='0' && (*(src+1)=='x' || *(src+1)=='X'))
/*@
@ loop invariant valid_read_string(src);
@ loop invariant res < 0x10000000;
@ loop assigns src, res;
@*/
for(;;src++)
{
for(src+=2;;src++)
const char c=*src;
if(c>='0' && c<='9')
res=res*16+(c-'0');
else if(c>='A' && c<='F')
res=res*16+(c-'A'+10);
else if(c>='a' && c<='f')
res=res*16+(c-'a'+10);
else
{
if(*src>='0' && *src<='9')
res=res*16+(*src)-'0';
else if(*src>='A' && *src<='F')
res=res*16+(*src)-'A'+10;
else if(*src>='a' && *src<='f')
res=res*16+(*src)-'a'+10;
else
{
*resptr=res;
return src;
}
*ptr=src;
return res;
}
if(res >= 0x10000000)
{
*ptr=src;
return res;
}
}
else
{
for(;*src>='0' && *src<='9';src++)
res=res*10+(*src)-'0';
*resptr=res;
return src;
}
}
/*@
@ requires \valid(ptr);
@ requires valid_read_string(*ptr);
@ ensures \initialized(ptr);
@ ensures valid_read_string(*ptr);
@ assigns *ptr;
@*/
static unsigned int str_uint_dec(char **ptr)
{
char *src=*ptr;
unsigned int res=0;
/*@
@ loop invariant valid_read_string(src);
@ loop invariant res < 0x10000000;
@ loop assigns src, res;
@*/
for(;*src>='0' && *src<='9';src++)
{
res=res*10+(*src)-'0';
if(res >= 0x10000000)
{
*ptr=src;
return res;
}
}
*ptr=src;
return res;
}
/*@
@ requires \valid(ptr);
@ requires valid_read_string(*ptr);
@ ensures \initialized(ptr);
@ ensures valid_read_string(*ptr);
@ assigns *ptr;
@*/
static unsigned int str_uint(char **ptr)
{
const char *src=*ptr;
if(*src=='0' && (*(src+1)=='x' || *(src+1)=='X'))
{
(*ptr)+=2;
return str_uint_hex(ptr);
}
return str_uint_dec(ptr);
}
/*@
@ assigns \nothing;
@ */
static unsigned char escaped_char(const unsigned char c)
{
switch(c)
{
case 'b':
return '\b';
case 'n':
return '\n';
case 't':
return '\t';
case 'r':
return '\r';
case '0':
return '\0';
default:
return c;
}
}
/*@
@ ensures 0 <= \result <= 0x10;
@ assigns \nothing;
@*/
static unsigned int load_hex1(const unsigned char c)
{
if(c>='0' && c<='9')
return c-'0';
else if(c>='A' && c<='F')
return c-'A'+10;
else if(c>='a' && c<='f')
return c-'a'+10;
return 0x10;
}
/*@
@ ensures 0 <= \result <= 0x100;
@ assigns \nothing;
@*/
static unsigned int load_hex2(const unsigned char c1, const unsigned char c2)
{
unsigned int val1=load_hex1(c1);
unsigned int val2=load_hex1(c2);
if(val1 >= 0x10 || val2 >=0x10)
return 0x100;
return (val1*16)+val2;
}
/*@
@ requires \valid(*ptr);
@ requires valid_string(*ptr);
@ requires \valid(tmp + (0 .. PHOTOREC_MAX_SIG_SIZE-1));
@ ensures valid_string(*ptr);
@ ensures \initialized(tmp + (0 .. \result-1));
@*/
/* TODO assigns *ptr, tmp[0 .. PHOTOREC_MAX_SIG_SIZE-1]; */
static unsigned int load_signature(char **ptr, unsigned char *tmp)
{
unsigned int signature_size=0;
char *pos=*ptr;
/*@
@ loop invariant \valid(*ptr);
@ loop invariant valid_string(pos);
@ loop invariant signature_size <= PHOTOREC_MAX_SIG_SIZE;
@ loop invariant \valid(tmp + (0 .. PHOTOREC_MAX_SIG_SIZE-1));
@ loop assigns pos, signature_size, tmp[0 .. PHOTOREC_MAX_SIG_SIZE-1];
@*/
while(*pos!='\n' && *pos!='\0')
{
if(signature_size>=PHOTOREC_MAX_SIG_SIZE)
return 0;
/*@ assert signature_size < PHOTOREC_MAX_SIG_SIZE; */
if(*pos ==' ' || *pos=='\t' || *pos=='\r' || *pos==',')
pos++;
else if(*pos== '\'')
{
pos++;
if(*pos=='\0')
return 0;
if(*pos=='\\')
{
pos++;
if(*pos=='\0')
return 0;
tmp[signature_size++]=escaped_char(*(unsigned char *)pos);
}
else
{
tmp[signature_size++]=*(unsigned char *)pos;
}
pos++;
if(*pos!='\'')
return 0;
pos++;
}
else if(*pos=='"')
{
pos++;
/*@
@ loop invariant valid_string(pos);
@ loop invariant signature_size <= PHOTOREC_MAX_SIG_SIZE;
@ loop assigns pos, signature_size, tmp[0 .. PHOTOREC_MAX_SIG_SIZE-1];
@*/
while(*pos!='"')
{
if(*pos=='\0')
return 0;
if(signature_size>=PHOTOREC_MAX_SIG_SIZE)
return 0;
if(*pos=='\\')
{
pos++;
if(*pos=='\0')
return 0;
tmp[signature_size++]=escaped_char(*(unsigned char *)pos);
}
else
tmp[signature_size++]=*(unsigned char *)pos;
pos++;
}
/*@ assert *pos=='"'; */
pos++;
}
else if(*pos=='0' && (*(pos+1)=='x' || *(pos+1)=='X'))
{
pos+=2;
/*@ assert valid_string(pos); */
/*@
@ loop invariant valid_string(pos);
@ loop invariant signature_size <= PHOTOREC_MAX_SIG_SIZE;
@ loop assigns pos, signature_size, tmp[0 .. PHOTOREC_MAX_SIG_SIZE-1];
@*/
while(
#ifdef DISABLED_FOR_FRAMAC
*pos!='\0' && *(pos+1)!='\0'
#else
isxdigit(*pos) && isxdigit(*(pos+1))
#endif
)
{
unsigned int val;
if(signature_size>=PHOTOREC_MAX_SIG_SIZE)
return 0;
/*@ assert valid_string(pos); */
/*@ assert valid_string(pos+1); */
val=load_hex2(*(unsigned char *)pos, *(unsigned char *)(pos+1));
if(val >= 0x100)
break;
pos+=2;
tmp[signature_size++]=val;
}
}
else
{
return 0;
}
/*@ assert valid_string(pos); */
}
*ptr=pos;
return signature_size;
}
/*@
@ requires valid_register_header_check(file_stat);
@ requires valid_file_stat(file_stat);
@ requires valid_string(pos);
@ ensures valid_string(\result);
@*/
static char *parse_signature_line(file_stat_t *file_stat, char *pos)
{
/* each line is composed of "extension sig_offset signature" */
const char *sig_ext=pos;
unsigned char *sig_sig=NULL;
unsigned int sig_offset=0;
unsigned int sig_size;
/* Read the extension */
/*@
@ loop invariant valid_read_string(sig_ext);
@ loop invariant valid_string(pos);
@ loop assigns pos;
@*/
while(*pos!=' ' && *pos!='\t')
{
if(*pos=='\0' || *pos=='\n' || *pos=='\r')
return pos;
pos++;
}
*pos='\0';
pos++;
/*@ assert valid_string(pos); */
#ifndef DISABLED_FOR_FRAMAC
log_info("register a signature for %s\n", sig_ext);
#endif
/* skip spaces */
/*@
@ loop invariant valid_string(pos);
@ loop assigns pos;
@*/
while(*pos=='\t' || *pos==' ')
{
/*@ assert *pos == '\t' || *pos== ' '; */
/*@ assert valid_string(pos); */
pos++;
}
sig_offset=str_uint(&pos);
if(sig_offset > PHOTOREC_MAX_SIG_OFFSET)
{
/* Invalid sig_offset */
return pos;
}
/*@ assert sig_offset <= PHOTOREC_MAX_SIG_OFFSET; */
/* read signature */
sig_sig=(unsigned char *)MALLOC(PHOTOREC_MAX_SIG_SIZE);
/*@ assert valid_string(pos); */
sig_size=load_signature(&pos, sig_sig);
if(sig_size==0)
{
free(sig_sig);
return pos;
}
if(*pos=='\n')
pos++;
/*@ assert sig_offset <= PHOTOREC_MAX_SIG_OFFSET; */
/*@ assert sig_size <= PHOTOREC_MAX_SIG_SIZE; */
if(sig_size>0 && sig_offset + sig_size <= PHOTOREC_MAX_SIG_OFFSET )
{
/* FIXME: memory leak for signature */
void *signature;
/*@ assert sig_size > 0; */
/*@ assert sig_offset + sig_size <= PHOTOREC_MAX_SIG_OFFSET; */
signature=(void *)MALLOC(sig_size);
/*@ assert \valid((char *)signature + (0 .. sig_size - 1)); */
memcpy(signature, sig_sig, sig_size);
#ifndef DISABLED_FOR_FRAMAC
signature_insert(sig_ext, sig_offset, signature, sig_size);
register_header_check(sig_offset, signature, sig_size, &header_check_sig, file_stat);
#endif
}
free(sig_sig);
return pos;
}
/*@
@ requires valid_register_header_check(file_stat);
@ requires valid_file_stat(file_stat);
@ requires valid_string(pos);
@ ensures valid_string(\result);
@*/
static char *parse_signature_file(file_stat_t *file_stat, char *pos)
{
const unsigned int signatures_empty=td_list_empty(&signatures.list);
#ifndef DISABLED_FOR_FRAMAC
/*@
@ loop invariant valid_file_stat(file_stat);
@ loop invariant valid_string(pos);
@*/
while(*pos!='\0')
#endif
{
/* skip comments */
/*@
@ loop invariant valid_string(pos);
@ loop assigns pos;
@*/
while(*pos=='#')
{
/*@
@ loop invariant valid_string(pos);
@ loop assigns pos;
@*/
while(*pos!='\0' && *pos!='\n')
pos++;
if(*pos=='\0')
return pos;
pos++;
}
/* each line is composed of "extension offset signature" */
{
char *extension;
unsigned int offset=0;
unsigned char *tmp=NULL;
unsigned int signature_max_size=512;
unsigned int signature_size=0;
{
const char *extension_start=pos;
while(*pos!='\0' && !isspace(*pos))
pos++;
if(*pos=='\0')
return pos;
*pos='\0';
extension=strdup(extension_start);
pos++;
}
/* skip space */
while(isspace(*pos))
pos++;
/* read offset */
pos=str_uint(pos, &offset);
/* read signature */
tmp=(unsigned char *)MALLOC(signature_max_size);
while(*pos!='\n' && *pos!='\0')
{
if(signature_size==signature_max_size)
{
unsigned char *tmp_old=tmp;
signature_max_size*=2;
tmp=(unsigned char *)realloc(tmp, signature_max_size);
if(tmp==NULL)
{
free(extension);
free(tmp_old);
return pos;
}
}
if(isspace(*pos) || *pos=='\r' || *pos==',')
pos++;
else if(*pos== '\'')
{
pos++;
if(*pos=='\0')
{
free(extension);
free(tmp);
return pos;
}
else if(*pos=='\\')
{
pos++;
if(*pos=='\0')
{
free(extension);
free(tmp);
return pos;
}
else if(*pos=='b')
tmp[signature_size++]='\b';
else if(*pos=='n')
tmp[signature_size++]='\n';
else if(*pos=='t')
tmp[signature_size++]='\t';
else if(*pos=='r')
tmp[signature_size++]='\r';
else if(*pos=='0')
tmp[signature_size++]='\0';
else
tmp[signature_size++]=*pos;
pos++;
}
else
{
tmp[signature_size++]=*pos;
pos++;
}
if(*pos!='\'')
{
free(extension);
free(tmp);
return pos;
}
pos++;
}
else if(*pos=='"')
{
pos++;
for(; *pos!='"' && *pos!='\0'; pos++)
{
if(signature_size==signature_max_size)
{
unsigned char *tmp_old=tmp;
signature_max_size*=2;
tmp=(unsigned char *)realloc(tmp, signature_max_size);
if(tmp==NULL)
{
free(extension);
free(tmp_old);
return pos;
}
}
if(*pos=='\\')
{
pos++;
if(*pos=='\0')
{
free(extension);
free(tmp);
return pos;
}
else if(*pos=='b')
tmp[signature_size++]='\b';
else if(*pos=='n')
tmp[signature_size++]='\n';
else if(*pos=='r')
tmp[signature_size++]='\r';
else if(*pos=='t')
tmp[signature_size++]='\t';
else if(*pos=='0')
tmp[signature_size++]='\0';
else
tmp[signature_size++]=*pos;
}
else
tmp[signature_size++]=*pos;;
}
if(*pos!='"')
{
free(extension);
free(tmp);
return pos;
}
pos++;
}
else if(*pos=='0' && (*(pos+1)=='x' || *(pos+1)=='X'))
{
pos+=2;
while(isxdigit(*pos) && isxdigit(*(pos+1)))
{
unsigned int val=(*pos);
if(*pos>='0' && *pos<='9')
val-='0';
else if(*pos>='A' && *pos<='F')
val=val-'A'+10;
else if(*pos>='a' && *pos<='f')
val=val-'a'+10;
pos++;
val*=16;
val+=(*pos);
if(*pos>='0' && *pos<='9')
val-='0';
else if(*pos>='A' && *pos<='F')
val=val-'A'+10;
else if(*pos>='a' && *pos<='f')
val=val-'a'+10;
pos++;
tmp[signature_size++]=val;
}
}
else
{
free(extension);
free(tmp);
return pos;
}
}
if(*pos=='\n')
pos++;
if(signature_size>0)
{
/* FIXME: Small memory leak */
unsigned char *signature=(unsigned char *)MALLOC(signature_size);
log_info("register a signature for %s\n", extension);
memcpy(signature, tmp, signature_size);
register_header_check(offset, signature, signature_size, &header_check_sig, file_stat);
if(signatures_empty)
signature_insert(extension, offset, signature, signature_size);
}
else
{
free(extension);
}
free(tmp);
}
/* skip empty lines */
/*@
@ loop invariant valid_string(pos);
@ loop assigns pos;
@*/
while(*pos=='\n' || *pos=='\r')
pos++;
pos=parse_signature_line(file_stat, pos);
}
return pos;
}
@ -424,14 +633,17 @@ static char *parse_signature_file(file_stat_t *file_stat, char *pos)
static void register_header_check_sig(file_stat_t *file_stat)
{
char *pos;
char *buffer;
static char *buffer=NULL;
size_t buffer_size;
struct stat stat_rec;
FILE *handle;
// if(!td_list_empty(&signatures.list))
if(buffer!=NULL)
return ;
handle=open_signature_file();
if(!handle)
return;
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
buffer_size=1024*1024;
#else
if(fstat(fileno(handle), &stat_rec)<0 || stat_rec.st_size>100*1024*1024)
@ -457,8 +669,10 @@ static void register_header_check_sig(file_stat_t *file_stat)
pos=parse_signature_file(file_stat, pos);
if(*pos!='\0')
{
#ifndef DISABLED_FOR_FRAMAC
log_warning("Can't parse signature: %s\n", pos);
#endif
}
free(buffer);
// free(buffer);
}
#endif

2
src/file_sp3.c
View file

@ -150,7 +150,7 @@ static void register_header_check_sp3(file_stat_t *file_stat)
static const unsigned char sp31_header[8]= { 0x03, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00};
static const unsigned char sp32_header[8]= { 0x03, 0x02, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00};
register_header_check(0, sp31_header, sizeof(sp31_header), &header_check_sp3, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, sp32_header, sizeof(sp32_header), &header_check_sp3, file_stat);
#endif
}

2
src/file_spe.c
View file

@ -300,7 +300,7 @@ static int header_check_spe(const unsigned char *buffer, const unsigned int buff
file_recovery_new->extension=file_hint_spe.extension;
file_recovery_new->min_filesize=4100;
file_recovery_new->calculated_file_size=tmp;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_debug("spe xdim=%u ydim=%u NumFrames=%u datatype=%u size=%llu\n",
le16(spe->xdim), le16(spe->ydim), (unsigned int)le32(spe->NumFrames), le16(spe->datatype),
(long long unsigned) file_recovery_new->calculated_file_size);

2
src/file_steuer2014.c
View file

@ -33,7 +33,7 @@
#include "filegen.h"
#include "common.h"
#if defined(__FRAMAC__)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_STRPTIME
#endif

2
src/file_swf.c
View file

@ -24,7 +24,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(SINGLE_FORMAT) || defined(MAIN_photorec) || defined(MAIN_fidentify)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_ZLIB_H
#undef HAVE_LIBZ
#endif

4
src/file_tar.c
View file

@ -20,7 +20,7 @@
*/
#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tar) || defined(MAIN_photorec)
#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tar)
#ifdef HAVE_CONFIG_H
#include <config.h>
#endif
@ -134,7 +134,7 @@ static int header_check_tar(const unsigned char *buffer, const unsigned int buff
static void register_header_check_tar(file_stat_t *file_stat)
{
register_header_check(0x101, tar_header_gnu, sizeof(tar_header_gnu), &header_check_tar, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0x101, tar_header_posix, sizeof(tar_header_posix), &header_check_tar, file_stat);
#endif
}

4
src/file_tiff_be.c
View file

@ -217,7 +217,7 @@ static uint64_t parse_strip_be(FILE *handle, const TIFFDirEntry *entry_strip_off
be16(entry_strip_bytecounts->tdir_type)!=4)
return TIFF_ERROR;
/*@ assert 0 < nbr <= 2048; */
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
offsetp=(uint32_t *)MALLOC(2048*sizeof(*offsetp));
#else
offsetp=(uint32_t *)MALLOC(nbr*sizeof(*offsetp));
@ -228,7 +228,7 @@ static uint64_t parse_strip_be(FILE *handle, const TIFFDirEntry *entry_strip_off
free(offsetp);
return TIFF_ERROR;
}
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
sizep=(uint32_t *)MALLOC(2048*sizeof(*sizep));
#else
sizep=(uint32_t *)MALLOC(nbr*sizeof(*sizep));

4
src/file_tiff_le.c
View file

@ -221,7 +221,7 @@ static uint64_t parse_strip_le(FILE *handle, const TIFFDirEntry *entry_strip_off
le16(entry_strip_bytecounts->tdir_type)!=4)
return TIFF_ERROR;
/*@ assert 0 < nbr <= 2048; */
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
offsetp=(uint32_t *)MALLOC(2048*sizeof(*offsetp));
#else
offsetp=(uint32_t *)MALLOC(nbr*sizeof(*offsetp));
@ -232,7 +232,7 @@ static uint64_t parse_strip_le(FILE *handle, const TIFFDirEntry *entry_strip_off
free(offsetp);
return TIFF_ERROR;
}
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
sizep=(uint32_t *)MALLOC(2048*sizeof(*sizep));
#else
sizep=(uint32_t *)MALLOC(nbr*sizeof(*sizep));

12
src/file_txt.c
View file

@ -167,6 +167,7 @@ static const txt_header_t fasttxt_headers[] = {
/* Unix shell */
{ "#!/bin/bash", 11, "sh"},
{ "#!/bin/ksh", 10, "sh"},
#ifndef DISABLED_FOR_FRAMAC
{ "#!/bin/sh", 9, "sh"},
{ "#! /bin/bash", 12, "sh"},
{ "#! /bin/ksh", 11, "sh"},
@ -273,6 +274,7 @@ static const txt_header_t fasttxt_headers[] = {
{ "[.ShellClassInfo]", 17, "Desktop.ini" },
/* Fotobook */
{ "<fotobook ", 10, "mcf"},
#endif
{NULL, 0, NULL}
};
@ -430,7 +432,7 @@ static unsigned int is_fortran(const char *buffer)
if(str==NULL)
return 0;
/*@ assert valid_read_string(str); */
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
if(*str=='\0')
return 0;
#endif
@ -486,7 +488,7 @@ static double is_random(const unsigned char *buffer, const unsigned int buffer_s
double ind;
if(buffer_size < 2)
return 1;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
memset(&stats, 0, sizeof(stats));
#else
/*@
@ -827,7 +829,7 @@ static void file_rename_fods(file_recovery_t *file_recovery)
#endif
fclose(file);
buffer[lu]='\0';
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
/*@
@ loop invariant tmp==\null || valid_read_string(tmp);
@ loop assigns tmp;
@ -882,7 +884,7 @@ static void file_rename_html(file_recovery_t *file_recovery)
#endif
fclose(file);
buffer[lu]='\0';
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
tmp=strchr(buffer,'<');
while(tmp!=NULL)
{
@ -1819,7 +1821,7 @@ static int header_check_txt(const unsigned char *buffer, const unsigned int buff
else if((str=strstr(buffer_lower, "\nimport "))!=NULL)
{
/*@ assert valid_read_string(str); */
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
str+=8;
#endif
/*@ assert valid_read_string(str); */

2
src/file_tz.c
View file

@ -73,7 +73,7 @@ static void register_header_check_tz(file_stat_t *file_stat)
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00
};
register_header_check(0, tz_header, sizeof(tz_header), &header_check_tz, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, tz2_header, sizeof(tz2_header), &header_check_tz, file_stat);
#endif
}

2
src/file_wad.c
View file

@ -75,7 +75,7 @@ static int header_check_wad(const unsigned char *buffer, const unsigned int buff
static void register_header_check_wad(file_stat_t *file_stat)
{
register_header_check(0, "PWAD", 4, &header_check_wad, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, "IWAD", 4, &header_check_wad, file_stat);
#endif
}

2
src/file_xcf.c
View file

@ -79,7 +79,7 @@ static int header_check_xcf(const unsigned char *buffer, const unsigned int buff
static void register_header_check_xcf(file_stat_t *file_stat)
{
register_header_check(0, "gimp xcf file", 13, &header_check_xcf, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, "gimp xcf v001", 13, &header_check_xcf, file_stat);
register_header_check(0, "gimp xcf v002", 13, &header_check_xcf, file_stat);
#endif

16
src/file_xm.c
View file

@ -80,7 +80,7 @@ static int parse_patterns(file_recovery_t *fr, uint16_t patterns)
Frama_C_make_unknown(&buffer, sizeof(uint32_t));
#endif
header_size = le32(*p32);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_debug("xm: pattern header of size %u\n", (unsigned int)header_size);
#endif
/* Never seen any xm having anything but 9 here */
@ -96,7 +96,7 @@ static int parse_patterns(file_recovery_t *fr, uint16_t patterns)
Frama_C_make_unknown(&buffer, sizeof(uint16_t));
#endif
data_size = le16(*p16);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_debug("xm: pattern data of size %u\n", data_size);
#endif
@ -139,7 +139,7 @@ static int parse_instruments(file_recovery_t *fr, uint16_t instrs)
#endif
size = le32(*p32);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_debug("xm: instrument header of size %u\n", (unsigned int)size);
#endif
if(size < 29)
@ -156,7 +156,7 @@ static int parse_instruments(file_recovery_t *fr, uint16_t instrs)
Frama_C_make_unknown(&buffer, sizeof(uint16_t));
#endif
samples = le16(*p16);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_debug("xm: instrument with %u samples\n", samples);
#endif
@ -168,7 +168,7 @@ static int parse_instruments(file_recovery_t *fr, uint16_t instrs)
{
if(size != 263)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_debug("xm: UNEXPECTED HEADER SIZE OF %u, "
" PLEASE REPORT THE FILE!\n",
(unsigned int)size);
@ -189,7 +189,7 @@ static int parse_instruments(file_recovery_t *fr, uint16_t instrs)
Frama_C_make_unknown(&buffer, sizeof(uint32_t));
#endif
size = le32(*p32);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_debug("xm: sample with length of %u\n", (unsigned int)size);
#endif
@ -236,7 +236,7 @@ static void file_check_xm(file_recovery_t *fr)
instrs = le16(hdr->instrs);
patterns = le16(hdr->patterns);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_debug("xm: %u patterns, %u instruments\n", patterns, instrs);
#endif
@ -248,7 +248,7 @@ static void file_check_xm(file_recovery_t *fr)
/* Parse patterns and next instruments */
if(parse_patterns(fr, patterns) < 0 || parse_instruments(fr, instrs) < 0)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_debug("xm: lost sync at pos %li\n", ftell(fr->handle));
#endif
fr->offset_error = fr->file_size;

6
src/file_zip.c
View file

@ -238,7 +238,7 @@ static int64_t file_get_pos(FILE *f, const void* needle, const unsigned int size
{
if(my_fseek(f, (off_t)count-(off_t)read_size, SEEK_CUR)<0)
{
#if !defined(__FRAMAC__)
#if !defined(DISABLED_FOR_FRAMAC)
log_trace("zip: file_get_pos count-read failed\n");
#endif
return -1;
@ -250,7 +250,7 @@ static int64_t file_get_pos(FILE *f, const void* needle, const unsigned int size
}
if(feof(f) || my_fseek(f, (off_t)1-size, SEEK_CUR)<0)
{
#if !defined(__FRAMAC__)
#if !defined(DISABLED_FOR_FRAMAC)
log_trace("zip: file_get_pos 1-size failed\n");
#endif
return -1;
@ -1387,7 +1387,7 @@ static void register_header_check_zip(file_stat_t *file_stat)
{
static const unsigned char zip_header2[8] = { 'P', 'K', '0', '0', 'P', 'K', 0x03, 0x04}; /* WinZIPv8-compressed files. */
register_header_check(0, zip_header,sizeof(zip_header), &header_check_zip, file_stat);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
register_header_check(0, zip_header2,sizeof(zip_header2), &header_check_winzip, file_stat);
#endif
}

28
src/filegen.c
View file

@ -24,7 +24,7 @@
#include <config.h>
#endif
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
#undef HAVE_FTELLO
#undef HAVE_FSEEKO
#endif
@ -63,13 +63,18 @@ file_check_list_t file_check_list={
@ requires \valid_read(b);
@ assigns \nothing;
@*/
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
static
#endif
int file_check_cmp(const struct td_list_head *a, const struct td_list_head *b)
{
#ifdef DISABLED_FOR_FRAMAC
return 1;
#else
const file_check_t *fc_a=td_list_entry_const(a, const file_check_t, list);
const file_check_t *fc_b=td_list_entry_const(b, const file_check_t, list);
/*@ requires valid_file_check_node(fc_a); */
/*@ requires valid_file_check_node(fc_b); */
int res;
unsigned int min_length;
/*@ assert \valid_read(fc_a); */
@ -97,12 +102,14 @@ int file_check_cmp(const struct td_list_head *a, const struct td_list_head *b)
if(res!=0)
return res;
return (int)fc_b->length-(int)fc_a->length;
#endif
}
/*@
@ requires \valid(file_check_new);
@ requires \valid(pos);
@ requires initialization: \initialized(&file_check_new->offset) && \initialized(&file_check_new->length);
@ requires valid_file_check_node(file_check_new);
@*/
static void file_check_add_tail(file_check_t *file_check_new, file_check_list_t *pos)
{
@ -131,7 +138,7 @@ static void file_check_add_tail(file_check_t *file_check_new, file_check_list_t
td_list_add_tail(&newe->list, &pos->list);
}
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
/*@
@ requires separation: \separated(file_stat, &file_check_plist);
@*/
@ -217,6 +224,7 @@ static unsigned int index_header_check(void)
void free_header_check(void)
{
#ifndef DISABLED_FOR_FRAMAC
struct td_list_head *tmpl;
struct td_list_head *nextl;
td_list_for_each_safe(tmpl, nextl, &file_check_list.list)
@ -232,6 +240,7 @@ void free_header_check(void)
{
struct td_list_head *tmp;
struct td_list_head *next;
/* TODO loop invariant \valid(next); */
td_list_for_each_safe(tmp, next, &pos->file_checks[i].list)
{
#ifdef DEBUG_HEADER_CHECK
@ -260,6 +269,7 @@ void free_header_check(void)
td_list_del(tmpl);
free(pos);
}
#endif
}
void file_allow_nl(file_recovery_t *file_recovery, const unsigned int nl_mode)
@ -447,7 +457,7 @@ file_stat_t * init_file_stats(file_enable_t *files_enable)
}
sign_nbr=index_header_check();
file_stats[enable_count-1].file_hint=NULL;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("%u first-level signatures enabled\n", sign_nbr);
#endif
return file_stats;
@ -462,7 +472,7 @@ file_stat_t * init_file_stats(file_enable_t *files_enable)
@*/
static int file_rename_aux(file_recovery_t *file_recovery, const char *new_ext)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
char new_filename[sizeof(file_recovery->filename)];
char *dst;
char *dst_dir_sep;
@ -538,7 +548,7 @@ static int _file_rename(file_recovery_t *file_recovery, const void *buffer, cons
len+=buffer_size-offset+1;
if(new_ext!=NULL)
len+=strlen(new_ext);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
new_filename=(char*)MALLOC(len);
dst=new_filename;
directory_sep=new_filename;
@ -677,7 +687,7 @@ static int _file_rename_unicode(file_recovery_t *file_recovery, const void *buff
len+=buffer_size-offset;
if(new_ext!=NULL)
len+=strlen(new_ext);
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
new_filename=(char*)MALLOC(len);
dst=new_filename;
dst_dir_sep=dst;
@ -790,11 +800,9 @@ void header_ignored_cond_reset(uint64_t start, uint64_t end)
/* 0: file_recovery_new->location.start has been taken into account, offset_skipped_header may have been updated
* 1: file_recovery_new->location.start has been ignored */
/*@
@ requires separation: \separated(file_recovery, file_recovery->handle, file_recovery_new, &errno, &offset_skipped_header);
@*/
int header_ignored_adv(const file_recovery_t *file_recovery, const file_recovery_t *file_recovery_new)
{
/*@ assert \separated(file_recovery, file_recovery->handle, file_recovery_new, &errno, &offset_skipped_header); */
file_recovery_t fr_test;
off_t offset;
assert(file_recovery!=NULL);

111
src/fnctdsk.c
View file

@ -59,6 +59,7 @@ uint64_t CHS2offset(const disk_t *disk_car,const CHS_t*CHS)
{
return (((uint64_t)CHS->cylinder * disk_car->geom.heads_per_cylinder + CHS->head) *
disk_car->geom.sectors_per_head + CHS->sector - 1) * disk_car->sector_size;
// return (uint64_t)C_H_S2LBA(disk_car, CHS->cylinder, CHS->head, CHS->sector) * disk_car->sector_size;
}
unsigned int offset2sector(const disk_t *disk_car, const uint64_t offset)
@ -111,40 +112,72 @@ void dup_partition_t(partition_t *dst, const partition_t *src)
#endif
}
list_disk_t *insert_new_disk_aux(list_disk_t *list_disk, disk_t *disk, disk_t **the_disk)
/*@
@ requires valid_list_disk(list_disk);
@ requires disk!=\null;
@ requires valid_disk(disk);
@ assigns \nothing;
@*/
static disk_t *search_disk(const list_disk_t *list_disk, const disk_t *disk)
{
list_disk_t *tmp;
list_disk_t *prev=NULL;
list_disk_t *new_disk;
if(disk==NULL)
{
if(the_disk!=NULL)
*the_disk=NULL;
return list_disk;
}
/* Add it at the end if it doesn't already exist */
const list_disk_t *tmp;
/*@
@ loop assigns tmp;
@*/
for(tmp=list_disk;tmp!=NULL;tmp=tmp->next)
{
if(tmp->disk->device!=NULL && disk->device!=NULL &&
strcmp(tmp->disk->device, disk->device)==0)
{
disk->clean(disk);
if(the_disk!=NULL)
*the_disk=tmp->disk;
return list_disk;
return tmp->disk;
}
prev=tmp;
}
return NULL;
}
list_disk_t *insert_new_disk_aux(list_disk_t *list_disk, disk_t *disk, disk_t **the_disk)
{
list_disk_t *prev=NULL;
list_disk_t *new_disk;
disk_t *found;
if(disk==NULL)
{
if(the_disk!=NULL)
*the_disk=NULL;
/*@ assert valid_list_disk(list_disk); */
return list_disk;
}
found=search_disk(list_disk, disk);
/* Do not add a disk already known */
if(found!=NULL)
{
disk->clean(disk);
if(the_disk!=NULL)
*the_disk=found;
/*@ assert valid_list_disk(list_disk); */
return list_disk;
}
/* Add the disk at the end */
{
list_disk_t *tmp;
/*@
@ loop assigns tmp,prev;
@*/
for(tmp=list_disk;tmp!=NULL;tmp=tmp->next)
prev=tmp;
}
new_disk=(list_disk_t *)MALLOC(sizeof(*new_disk));
new_disk->disk=disk;
new_disk->prev=prev;
new_disk->next=NULL;
if(prev!=NULL)
{
prev->next=new_disk;
}
new_disk->prev=prev;
new_disk->next=NULL;
if(the_disk!=NULL)
*the_disk=disk;
/*@ assert valid_list_disk(new_disk); */
/*@ assert valid_list_disk(list_disk); */
return (list_disk!=NULL?list_disk:new_disk);
}
@ -222,6 +255,10 @@ list_part_t *sort_partition_list(list_part_t *list_part)
list_part_t *new_list_part=NULL;
list_part_t *element;
list_part_t *next;
/*@ assert valid_list_part(new_list_part); */
/*@
@ loop invariant valid_list_part(new_list_part);
@*/
for(element=list_part;element!=NULL;element=next)
{
int insert_error=0;
@ -231,6 +268,7 @@ list_part_t *sort_partition_list(list_part_t *list_part)
free(element->part);
free(element);
}
/*@ assert valid_list_part(new_list_part); */
return new_list_part;
}
@ -238,12 +276,17 @@ list_part_t *gen_sorted_partition_list(const list_part_t *list_part)
{
list_part_t *new_list_part=NULL;
const list_part_t *element;
/*@ assert valid_list_part(new_list_part); */
/*@
@ loop invariant valid_list_part(new_list_part);
@*/
for(element=list_part;element!=NULL;element=element->next)
{
int insert_error=0;
if(element->part->status!=STATUS_DELETED)
new_list_part=insert_new_partition(new_list_part, element->part, 1, &insert_error);
}
/*@ assert valid_list_part(new_list_part); */
return new_list_part;
}
@ -252,6 +295,7 @@ void part_free_list(list_part_t *list_part)
{
list_part_t *element;
element=list_part;
/*@ loop invariant valid_list_part(element); */
while(element!=NULL)
{
list_part_t *next=element->next;
@ -266,6 +310,7 @@ void part_free_list_only(list_part_t *list_part)
{
list_part_t *element;
element=list_part;
/*@ loop invariant valid_list_part(element); */
while(element!=NULL)
{
list_part_t *next=element->next;
@ -283,6 +328,9 @@ int is_part_overlapping(const list_part_t *list_part)
if(list_part==NULL)
return 0;
element=list_part;
/*@
@ loop assigns element;
@*/
while(1)
{
const list_part_t *next=element->next;
@ -313,7 +361,9 @@ void partition_reset(partition_t *partition, const arch_fnct_t *arch)
partition->part_type_mac=PMAC_UNK;
partition->part_type_xbox=PXBOX_UNK;
partition->part_type_gpt=GPT_ENT_TYPE_UNUSED;
#ifndef DISABLED_FOR_FRAMAC
guid_cpy(&partition->part_uuid, &GPT_ENT_TYPE_UNUSED);
#endif
partition->upart_type=UP_UNK;
partition->status=STATUS_DELETED;
partition->order=NO_ORDER;
@ -357,7 +407,7 @@ static unsigned int get_geometry_from_list_part_aux(const disk_t *disk_car, cons
}
}
}
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
if(nbr>0)
{
log_info("get_geometry_from_list_part_aux head=%u nbr=%u\n",
@ -387,26 +437,29 @@ unsigned int get_geometry_from_list_part(const disk_t *disk_car, const list_part
unsigned int best_score;
unsigned int i;
unsigned int heads_per_cylinder=disk_car->geom.heads_per_cylinder;
disk_t *new_disk_car=(disk_t *)MALLOC(sizeof(*new_disk_car));
memcpy(new_disk_car,disk_car,sizeof(*new_disk_car));
best_score=get_geometry_from_list_part_aux(new_disk_car, list_part, verbose);
disk_t new_disk_car;
memcpy(&new_disk_car,disk_car,sizeof(new_disk_car));
best_score=get_geometry_from_list_part_aux(&new_disk_car, list_part, verbose);
/*@ loop assigns i, best_score, heads_per_cylinder, new_disk_car.geom.heads_per_cylinder; */
for(i=0; head_list[i]!=0; i++)
{
unsigned int score;
new_disk_car->geom.heads_per_cylinder=head_list[i];
score=get_geometry_from_list_part_aux(new_disk_car, list_part, verbose);
new_disk_car.geom.heads_per_cylinder=head_list[i];
score=get_geometry_from_list_part_aux(&new_disk_car, list_part, verbose);
if(score >= best_score)
{
best_score=score;
heads_per_cylinder=new_disk_car->geom.heads_per_cylinder;
heads_per_cylinder=new_disk_car.geom.heads_per_cylinder;
}
}
free(new_disk_car);
return heads_per_cylinder;
}
void size_to_unit(const uint64_t disk_size, char *buffer)
{
#ifdef DISABLED_FOR_FRAMAC
buffer[0]='\0';
#else
if(disk_size<(uint64_t)10*1024)
sprintf(buffer,"%u B", (unsigned)disk_size);
else if(disk_size<(uint64_t)10*1024*1024)
@ -417,13 +470,18 @@ void size_to_unit(const uint64_t disk_size, char *buffer)
sprintf(buffer,"%u GB / %u GiB", (unsigned)(disk_size/1000/1000/1000), (unsigned)(disk_size/1024/1024/1024));
else
sprintf(buffer,"%u TB / %u TiB", (unsigned)(disk_size/1000/1000/1000/1000), (unsigned)(disk_size/1024/1024/1024/1024));
#endif
}
void log_disk_list(list_disk_t *list_disk)
{
#ifndef DISABLED_FOR_FRAMAC
list_disk_t *element_disk;
/* save disk parameters to rapport */
log_info("Hard disk list\n");
/*@
@ loop invariant valid_list_disk(list_disk);
@*/
for(element_disk=list_disk;element_disk!=NULL;element_disk=element_disk->next)
{
disk_t *disk=element_disk->disk;
@ -437,4 +495,5 @@ void log_disk_list(list_disk_t *list_disk)
log_info("\n");
}
log_info("\n");
#endif
}

12
src/geometry.c
View file

@ -79,7 +79,7 @@ int change_geometry_cli(disk_t *disk_car, char ** current_cmd)
int geo_modified=0;
if(*current_cmd==NULL)
return 0;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("Current geometry\n%s sector_size=%u\n", disk_car->description(disk_car), disk_car->sector_size);
#endif
/*@ loop invariant valid_read_string(*current_cmd); */
@ -96,7 +96,7 @@ int change_geometry_cli(disk_t *disk_car, char ** current_cmd)
if(geo_modified==0)
geo_modified=1;
}
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
else
log_error("Illegal cylinders value\n");
#endif
@ -112,7 +112,7 @@ int change_geometry_cli(disk_t *disk_car, char ** current_cmd)
if(cyl_modified==0)
set_cylinders_from_size_up(disk_car);
}
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
else
log_error("Illegal heads value\n");
#endif
@ -128,7 +128,7 @@ int change_geometry_cli(disk_t *disk_car, char ** current_cmd)
if(cyl_modified==0)
set_cylinders_from_size_up(disk_car);
}
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
else
log_error("Illegal sectors value\n");
#endif
@ -138,7 +138,7 @@ int change_geometry_cli(disk_t *disk_car, char ** current_cmd)
tmp_val = get_int_from_command(current_cmd);
if(change_sector_size(disk_car, cyl_modified, tmp_val)==0)
geo_modified=2;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
else
log_error("Illegal sector size\n");
#endif
@ -158,7 +158,7 @@ int change_geometry_cli(disk_t *disk_car, char ** current_cmd)
/* On MacOSX if HD contains some bad sectors, the disk size may not be correctly detected */
disk_car->disk_real_size=disk_car->disk_size;
#endif
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("New geometry\n%s sector_size=%u\n", disk_car->description(disk_car), disk_car->sector_size);
#endif
autoset_unit(disk_car);

2
src/geometryn.c
View file

@ -23,7 +23,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_NCURSES
#endif

413
src/hdaccess.c
View file

@ -23,7 +23,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_FSYNC
#undef HAVE_GLOB_H
#undef HAVE_LIBEWF
@ -169,8 +169,20 @@ struct info_file_struct
int mode;
};
static void autoset_geometry(disk_t * disk_car, const unsigned char *buffer, const int verbose);
static void file_clean(disk_t *disk);
struct dosemu_image_header {
char sig[7]; /* always set to "DOSEMU", null-terminated or to "\x0eDEXE" */
uint32_t heads;
uint32_t sectors;
uint32_t cylinders;
uint32_t header_end; /* distance from beginning of disk to end of header
* i.e. this is the starting byte of the real disk
*/
char dummy[1]; /* someone did define the header unaligned,
* we correct that atleast for the future
*/
uint32_t dexeflags;
} __attribute__((packed)) ;
static int file_pread(disk_t *disk_car, void *buf, const unsigned int count, const uint64_t offset);
static int file_pwrite(disk_t *disk_car, const void *buf, const unsigned int count, const uint64_t offset);
static int file_nopwrite(disk_t *disk_car, const void *buf, const unsigned int count, const uint64_t offset);
@ -199,34 +211,36 @@ void generic_clean(disk_t *disk)
}
#if defined(__CYGWIN__) || defined(__MINGW32__)
list_disk_t *insert_new_disk_nodup(list_disk_t *list_disk, disk_t *disk_car, const char *device_name, const int verbose);
list_disk_t *insert_new_disk_nodup(list_disk_t *list_disk, disk_t *disk_car, const char *device_name, const int verbose)
static list_disk_t *insert_new_disk_nodup(list_disk_t *list_disk, disk_t *disk_car, const char *device_name, const int verbose)
{
if(disk_car==NULL)
return list_disk;
if(disk_car->sector_size==512)
{
int disk_same_size_present=0;
list_disk_t *cur;
for(cur=list_disk;cur!=NULL;cur=cur->next)
{
if(cur->disk->sector_size==disk_car->sector_size &&
((cur->disk->model==NULL && disk_car->model==NULL && cur->disk->disk_size==disk_car->disk_size) ||
(cur->disk->model!=NULL && disk_car->model!=NULL && strcmp(cur->disk->model, disk_car->model)==0)))
disk_same_size_present=1;
{
if(verbose>1)
log_verbose("%s is available but reject it to avoid duplicate disk.\n", device_name);
disk_car->clean(disk_car);
return list_disk;
}
}
if(disk_car->sector_size==512 && disk_same_size_present!=0)
{
if(verbose>1)
log_verbose("%s is available but reject it to avoid duplicate disk.\n", device_name);
disk_car->clean(disk_car);
return list_disk;
}
return insert_new_disk(list_disk,disk_car);
}
return insert_new_disk(list_disk,disk_car);
}
#endif
#ifdef HAVE_GLOB_H
#if defined(HAVE_GLOB_H)
/*@
@ requires valid_read_string(device_pattern);
@ requires \valid(list_disk);
@ ensures \valid(list_disk);
@*/
static list_disk_t *hd_glob_parse(const char *device_pattern, list_disk_t *list_disk, const int verbose, const int testdisk_mode)
{
glob_t globbuf;
@ -309,57 +323,93 @@ list_disk_t *hd_parse(list_disk_t *list_disk, const int verbose, const int testd
char device_i2o_hd[]="/dev/i2o/hda";
char device_mmc[]="/dev/mmcblk0";
/* Disk IDE */
/*@
@ loop invariant valid_list_disk(list_disk);
@ loop invariant 0 <= i <= 8;
@*/
for(i=0;i<8;i++)
{
device_ide[strlen(device_ide)-1]='a'+i;
list_disk=insert_new_disk(list_disk, file_test_availability(device_ide, verbose, testdisk_mode));
}
/* Device RAID Compaq */
/*@
@ loop invariant valid_list_disk(list_disk);
@ loop invariant 0 <= j <= 8;
@*/
for(j=0;j<8;j++)
{
device_ida[strlen(device_ida)-3]='0'+j;
/*@
@ loop invariant valid_list_disk(list_disk);
@ loop invariant 0 <= i <= 8;
@*/
for(i=0;i<8;i++)
{
device_ida[strlen(device_ida)-1]='0'+i;
list_disk=insert_new_disk(list_disk, file_test_availability(device_ida, verbose, testdisk_mode));
}
}
/*@
@ loop invariant valid_list_disk(list_disk);
@ loop invariant 0 <= i <= 8;
@*/
for(i=0;i<8;i++)
{
device_cciss[strlen(device_cciss)-1]='0'+i;
list_disk=insert_new_disk(list_disk, file_test_availability(device_cciss, verbose, testdisk_mode));
}
/* Device RAID */
/*@
@ loop invariant valid_list_disk(list_disk);
@ loop invariant 0 <= i <= 10;
@*/
for(i=0;i<10;i++)
{
snprintf(device,sizeof(device),"/dev/rd/c0d%u",i);
list_disk=insert_new_disk(list_disk, file_test_availability(device, verbose, testdisk_mode));
}
/* Device RAID IDE */
/*@
@ loop invariant valid_list_disk(list_disk);
@ loop invariant 0 <= i <= 15;
@*/
for(i=0;i<15;i++)
{
snprintf(device,sizeof(device),"/dev/ataraid/d%u",i);
list_disk=insert_new_disk(list_disk, file_test_availability(device, verbose, testdisk_mode));
}
/* Parallel port IDE disk */
/*@
@ loop invariant valid_list_disk(list_disk);
@ loop invariant 0 <= i <= 4;
@*/
for(i=0;i<4;i++)
{
device_p_ide[strlen(device_p_ide)-1]='a'+i;
list_disk=insert_new_disk(list_disk, file_test_availability(device_p_ide, verbose, testdisk_mode));
}
/* I2O hard disk */
/*@
@ loop invariant valid_list_disk(list_disk);
@ loop invariant 0 <= i <= 26;
@*/
for(i=0;i<26;i++)
{
device_i2o_hd[strlen(device_i2o_hd)-1]='a'+i;
list_disk=insert_new_disk(list_disk, file_test_availability(device_i2o_hd, verbose, testdisk_mode));
}
/* Memory card */
/*@
@ loop invariant valid_list_disk(list_disk);
@ loop invariant 0 <= i <= 10;
@*/
for(i=0;i<10;i++)
{
device_mmc[strlen(device_mmc)-1]='0'+i;
list_disk=insert_new_disk(list_disk, file_test_availability(device_mmc, verbose, testdisk_mode));
}
#ifdef HAVE_GLOB_H
#if defined(HAVE_GLOB_H)
/* Disk SCSI */
list_disk=hd_glob_parse("/dev/sd[a-z]", list_disk, verbose, testdisk_mode);
list_disk=hd_glob_parse("/dev/sd[a-z][a-z]", list_disk, verbose, testdisk_mode);
@ -474,10 +524,15 @@ list_disk_t *hd_parse(list_disk_t *list_disk, const int verbose, const int testd
}
}
#endif
/*@ assert valid_list_disk(list_disk); */
return list_disk;
}
#ifndef DJGPP
/*@
@ requires valid_read_string(device);
@ ensures \result > 0;
@*/
static unsigned int disk_get_sector_size(const int hd_h, const char *device, const int verbose)
{
unsigned int sector_size=0;
@ -580,7 +635,7 @@ static unsigned int disk_get_sector_size(const int hd_h, const char *device, con
device_geometry g;
int error;
error = ioctl(hd_h, B_GET_GEOMETRY, &g, sizeof(g));
if(error==0)
if(error==0 && g.bytes_per_sector > 0)
{
if(verbose>1)
{
@ -597,12 +652,37 @@ static unsigned int disk_get_sector_size(const int hd_h, const char *device, con
return DEFAULT_SECTOR_SIZE;
}
/*@
@ requires \valid_read(geom);
@ ensures \result==-1 || \result==0;
@ ensures (0 < geom->heads_per_cylinder <= 255 && 0 < geom->sectors_per_head <= 63 && 0 < geom->cylinders < 0x2000000000000) ==> \result == 0;
@ ensures !(0 < geom->heads_per_cylinder <= 255 && 0 < geom->sectors_per_head <= 63 && 0 < geom->cylinders < 0x2000000000000) ==> \result == -1;
@ assigns \nothing;
@*/
static int check_geometry(const CHSgeometry_t *geom)
{
if(geom->heads_per_cylinder==0 || geom->heads_per_cylinder>255)
return -1;
if(geom->sectors_per_head==0 || geom->sectors_per_head>63)
return -1;
if(geom->cylinders==0 || geom->cylinders >= 0x2000000000000)
return -1;
return 0;
}
/*@
@ requires \valid(geom);
@ requires valid_read_string(device);
@ requires \separated(geom, device);
@ ensures 0 < geom->heads_per_cylinder <= 255;
@ ensures 0 < geom->sectors_per_head <= 63;
@*/
static void disk_get_geometry(CHSgeometry_t *geom, const int hd_h, const char *device, const int verbose)
{
if(verbose>1)
log_verbose("disk_get_geometry for %s\n", device);
#ifdef HDIO_GETGEO_BIG
if(geom->sectors_per_head==0)
if(check_geometry(geom)<0)
{
struct hd_big_geometry geometry;
if (ioctl(hd_h, HDIO_GETGEO_BIG, &geometry)>=0)
@ -626,7 +706,7 @@ static void disk_get_geometry(CHSgeometry_t *geom, const int hd_h, const char *d
}
#endif
#ifdef HDIO_GETGEO
if(geom->sectors_per_head==0)
if(check_geometry(geom)<0)
{
struct hd_geometry geometry;
if(ioctl(hd_h, HDIO_GETGEO, &geometry)>=0)
@ -643,7 +723,7 @@ static void disk_get_geometry(CHSgeometry_t *geom, const int hd_h, const char *d
}
#endif
#ifdef DKIOCGGEOM
if(geom->sectors_per_head==0)
if(check_geometry(geom)<0)
{
struct dk_geom dkgeom;
if (ioctl (hd_h, DKIOCGGEOM, &dkgeom)>=0) {
@ -658,7 +738,7 @@ static void disk_get_geometry(CHSgeometry_t *geom, const int hd_h, const char *d
}
#endif
#ifdef DIOCGDINFO
if(geom->sectors_per_head==0)
if(check_geometry(geom)<0)
{
struct disklabel geometry;
if (ioctl(hd_h, DIOCGDINFO, &geometry)==0)
@ -681,7 +761,7 @@ static void disk_get_geometry(CHSgeometry_t *geom, const int hd_h, const char *d
}
#endif
#ifdef DIOCGFWSECTORS
if(geom->sectors_per_head==0)
if(check_geometry(geom)<0)
{
int error;
unsigned int u;
@ -737,8 +817,12 @@ static void disk_get_geometry(CHSgeometry_t *geom, const int hd_h, const char *d
}
}
#endif
if(geom->sectors_per_head>0 && geom->heads_per_cylinder>0)
if(check_geometry(geom)==0)
{
/*@ assert 0 < geom->heads_per_cylinder <= 255; */
/*@ assert 0 < geom->sectors_per_head <= 63; */
return ;
}
geom->cylinders=0;
geom->heads_per_cylinder=1;
geom->sectors_per_head=1;
@ -746,8 +830,13 @@ static void disk_get_geometry(CHSgeometry_t *geom, const int hd_h, const char *d
{
log_error("disk_get_geometry default geometry for %s\n", device);
}
/*@ assert 0 < geom->heads_per_cylinder <= 255; */
/*@ assert 0 < geom->sectors_per_head <= 63; */
}
/*@
@ requires valid_read_string(device);
@*/
static uint64_t disk_get_size(const int hd_h, const char *device, const int verbose, const unsigned int sector_size)
{
if(verbose>1)
@ -850,7 +939,7 @@ void update_disk_car_fields(disk_t *disk_car)
{
if(disk_car->geom.cylinders>0)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_warning("Fix disk size using CHS\n");
#endif
disk_car->disk_real_size=(uint64_t)disk_car->geom.cylinders * disk_car->geom.heads_per_cylinder *
@ -865,7 +954,7 @@ void update_disk_car_fields(disk_t *disk_car)
(uint64_t)disk_car->sector_size;
if(cylinder_num>0 && disk_car->geom.cylinders != cylinder_num)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_debug("Fix cylinder count for %s: number of cylinders %lu != %lu (calculated)\n",
disk_car->device, disk_car->geom.cylinders, cylinder_num);
#endif
@ -878,27 +967,51 @@ void update_disk_car_fields(disk_t *disk_car)
}
#ifdef TARGET_LINUX
/*@
@ requires valid_string(buf);
@ ensures valid_string(buf);
@*/
static void rtrim(char *buf)
{
unsigned int i;
/*@ loop assigns i; */
for(i=strlen(buf); i>0 && buf[i] == ' '; i--);
/*@ assert 0 <= i < strlen(buf); */
buf[i]='\0';
}
/* This function reads the /sys entry named "file" for device "disk_car". */
static char * read_device_sysfs_file (const disk_t *disk_car, const char *file)
/*@
@ requires \valid(buf + (0..255));
@ requires \valid_read(disk_car);
@ requires valid_read_string(file);
@ requires separation: \separated(buf, disk_car, file, &errno);
@ ensures \result==-1 || \result==0;
@ ensures \result==-1 || valid_string(buf);
@*/
static int read_device_sysfs_file (char *buf, const disk_t *disk_car, const char *file)
{
FILE *f;
#ifndef DISABLED_FOR_FRAMAC
char name_buf[128];
char buf[256];
snprintf (name_buf, 127, "/sys/block/%s/device/%s",
basename (disk_car->device), file);
if ((f = fopen (name_buf, "r")) == NULL)
return NULL;
return -1;
#else
if ((f = fopen ("/sys/block/hda/device/vendor", "r")) == NULL)
return -1;
#endif
if (fgets (buf, 255, f) == NULL)
{
fclose (f);
return NULL;
return -1;
}
/*@ assert valid_string(buf); */
fclose (f);
return strip_dup (buf);
/*@ assert valid_string(buf); */
rtrim(buf);
return 0;
}
#endif
@ -938,6 +1051,11 @@ typedef struct _scsi_inquiry_data
#define INQ_CMD_LEN 6
#define INQ_REPLY_LEN sizeof(scsi_inquiry_data_t)
/*@
@ requires \valid(vendor);
@ requires \valid(product);
@ requires \valid(fw_rev);
@*/
static int scsi_query_product_info (const int sg_fd, char **vendor, char **product, char **fw_rev)
{
unsigned char inqCmdBlk[INQ_CMD_LEN] = {INQUIRY, 0, 0, 0, INQ_REPLY_LEN, 0};
@ -993,6 +1111,11 @@ static int scsi_query_product_info (const int sg_fd, char **vendor, char **produ
#endif
#ifndef DJGPP
/*@
@ requires \valid(dev);
@ requires valid_disk(dev);
@ ensures valid_disk(dev);
@*/
static void disk_get_model(const int hd_h, disk_t *dev, const unsigned int verbose)
{
#ifdef HDIO_GET_IDENTITY
@ -1047,17 +1170,20 @@ static void disk_get_model(const int hd_h, disk_t *dev, const unsigned int verbo
return;
{
/* Use modern /sys interface for SCSI device */
char *vendor;
char *product;
vendor = read_device_sysfs_file (dev, "vendor");
product = read_device_sysfs_file (dev, "model");
if (vendor && product)
char vendor[256];
char product[256];
memset(&vendor, 0, sizeof(vendor));
memset(&product, 0, sizeof(product));
if(read_device_sysfs_file (&vendor[0], dev, "vendor")==0)
{
dev->model = (char*) MALLOC(8 + 16 + 2);
sprintf (dev->model, "%.8s %.16s", vendor, product);
/*@ assert valid_string(&vendor[0]); */
if( read_device_sysfs_file (&product[0], dev, "model")==0)
{
/*@ assert valid_string(&product[0]); */
dev->model = (char*) MALLOC(8 + 16 + 2);
sprintf (dev->model, "%.8s %.16s", vendor, product);
}
}
free(vendor);
free(product);
}
#endif
#if defined(__CYGWIN__) || defined(__MINGW32__)
@ -1073,11 +1199,16 @@ static void disk_get_model(const int hd_h, disk_t *dev, const unsigned int verbo
file_win32_disk_get_model(handle, dev, verbose);
}
#endif
/*@ assert valid_disk(dev); */
}
/*@
@ requires sector_size > 0;
@ requires valid_read_string(device);
@*/
static uint64_t compute_device_size(const int hd_h, const char *device, const int verbose, const unsigned int sector_size)
{
#ifdef HAVE_PREAD
#if defined(HAVE_PREAD)
/* This function can failed if there are bad sectors */
uint64_t min_offset;
uint64_t max_offset;
@ -1120,10 +1251,20 @@ static uint64_t compute_device_size(const int hd_h, const char *device, const in
}
#endif
/*@
@ requires \valid(disk);
@ requires \valid_read((const struct info_file_struct *)disk->data);
@ requires valid_disk(disk);
@ ensures valid_disk(disk);
@*/
// ensures valid_read_string(\result);
static const char *file_description(disk_t *disk)
{
const struct info_file_struct *data=(const struct info_file_struct *)disk->data;
char buffer_disk_size[100];
#ifdef DISABLED_FOR_FRAMAC
memset(&buffer_disk_size, 0, sizeof(buffer_disk_size));
#endif
size_to_unit(disk->disk_size, buffer_disk_size);
if(disk->geom.heads_per_cylinder == 1 && disk->geom.sectors_per_head == 1)
snprintf(disk->description_txt, sizeof(disk->description_txt),
@ -1137,13 +1278,25 @@ static const char *file_description(disk_t *disk)
disk->device, buffer_disk_size,
disk->geom.cylinders, disk->geom.heads_per_cylinder, disk->geom.sectors_per_head,
((data->mode&O_RDWR)==O_RDWR?"":" (RO)"));
/*@ assert valid_read_string((char *)&disk->description_txt); */
/*@ assert valid_disk(disk); */
return disk->description_txt;
}
/*@
@ requires \valid(disk_car);
@ requires \valid_read((const struct info_file_struct *)disk_car->data);
@ requires valid_disk(disk_car);
@ ensures valid_disk(disk_car);
@*/
// ensures valid_read_string(\result);
static const char *file_description_short(disk_t *disk_car)
{
const struct info_file_struct *data=(const struct info_file_struct *)disk_car->data;
char buffer_disk_size[100];
#ifdef DISABLED_FOR_FRAMAC
memset(&buffer_disk_size, 0, sizeof(buffer_disk_size));
#endif
size_to_unit(disk_car->disk_size, buffer_disk_size);
if(disk_car->model==NULL)
snprintf(disk_car->description_short_txt, sizeof(disk_car->description_txt),"Disk %s - %s%s",
@ -1154,9 +1307,16 @@ static const char *file_description_short(disk_t *disk_car)
disk_car->device, buffer_disk_size,
((data->mode&O_RDWR)==O_RDWR?"":" (RO)"),
disk_car->model);
/*@ assert valid_read_string((char *)&disk_car->description_short_txt); */
/*@ assert valid_disk(disk_car); */
return disk_car->description_short_txt;
}
/*@
@ requires \valid(disk);
@ requires \freeable(disk);
@ requires valid_disk(disk);
@*/
static void file_clean(disk_t *disk)
{
if(disk->data!=NULL)
@ -1184,6 +1344,11 @@ static void file_clean(disk_t *disk)
generic_clean(disk);
}
/*@
@ requires \valid_read(disk);
@ requires valid_disk(disk);
@ requires \valid((char *)buf + (0 .. count - 1));
@*/
static int file_pread_aux(const disk_t *disk, void *buf, const unsigned int count, const uint64_t offset)
{
long int ret;
@ -1300,11 +1465,29 @@ static int file_pread_aux(const disk_t *disk, void *buf, const unsigned int coun
return ret;
}
/*@
@ requires \valid(disk_car);
@ requires valid_disk(disk_car);
@ requires disk_car->sector_size > 0;
@ requires disk_car->offset < 0x2000000000000;
@ requires 0 < count < 0x2000000000000;
@ requires offset < 0x2000000000000;
@ requires \valid((char *)buf + (0 .. count-1));
@*/
static int file_pread(disk_t *disk_car, void *buf, const unsigned int count, const uint64_t offset)
{
return align_pread(&file_pread_aux, disk_car, buf, count, offset);
}
/*@
@ requires \valid(disk_car);
@ requires valid_disk(disk_car);
@ requires disk_car->sector_size > 0;
@ requires disk_car->offset < 0x2000000000000;
@ requires 0 < count < 0x2000000000000;
@ requires offset < 0x2000000000000;
@ requires \valid_read((char *)buf + (0 .. count-1));
@*/
static int file_pwrite_aux(disk_t *disk_car, const void *buf, const unsigned int count, const uint64_t offset)
{
int fd=((struct info_file_struct *)disk_car->data)->handle;
@ -1343,11 +1526,28 @@ static int file_pwrite_aux(disk_t *disk_car, const void *buf, const unsigned int
return ret;
}
/*@
@ requires \valid(disk_car);
@ requires disk_car->sector_size > 0;
@ requires disk_car->offset < 0x2000000000000;
@ requires 0 < count < 0x2000000000000;
@ requires offset < 0x2000000000000;
@ requires \valid_read((char *)buf + (0 .. count-1));
@*/
static int file_pwrite(disk_t *disk_car, const void *buf, const unsigned int count, const uint64_t offset)
{
return align_pwrite(&file_pread_aux, &file_pwrite_aux, disk_car, buf, count, offset);
}
/*@
@ requires \valid(disk_car);
@ requires valid_disk(disk_car);
@ requires disk_car->sector_size > 0;
@ requires disk_car->offset < 0x2000000000000;
@ requires 0 < count < 0x2000000000000;
@ requires offset < 0x2000000000000;
@ requires \valid_read((char *)buf + (0 .. count-1));
@*/
static int file_nopwrite(disk_t *disk_car, const void *buf, const unsigned int count, const uint64_t offset)
{
struct info_file_struct *data=(struct info_file_struct *)disk_car->data;
@ -1357,9 +1557,13 @@ static int file_nopwrite(disk_t *disk_car, const void *buf, const unsigned int c
return -1;
}
/*@
@ requires \valid(disk_car);
@ requires valid_disk(disk_car);
@*/
static int file_sync(disk_t *disk_car)
{
#ifdef HAVE_FSYNC
#if defined(HAVE_FSYNC)
struct info_file_struct *data=(struct info_file_struct *)disk_car->data;
return fsync(data->handle);
#else
@ -1368,10 +1572,28 @@ static int file_sync(disk_t *disk_car)
#endif
}
/*@
@ requires \valid(disk);
@ requires valid_disk(disk);
@ requires 0 < disk->geom.heads_per_cylinder <= 255;
@ requires 0 < disk->geom.sectors_per_head <= 63;
@ requires \valid_read(buffer + (0 .. DEFAULT_SECTOR_SIZE-1));
@ requires separation: \separated(disk, buffer + (0 .. DEFAULT_SECTOR_SIZE-1));
@ decreases 0;
@ ensures valid_disk(disk);
@*/
// assigns disk->geom.cylinders;
// assigns disk->geom.heads_per_cylinder;
// assigns disk->geom.sectors_per_head;
// assigns disk->geom.bytes_per_sector;
// ensures 0 < disk->geom.heads_per_cylinder <= 255;
// ensures 0 < disk->geom.sectors_per_head <= 63;
static void autoset_geometry(disk_t *disk, const unsigned char *buffer, const int verbose)
{
if(disk->arch->get_geometry_from_mbr!=NULL)
/*@ assert 0 < disk->sector_size; */
if((disk->arch)->get_geometry_from_mbr!=NULL)
{
/*@ assert \valid_function(disk->arch->get_geometry_from_mbr); */
CHSgeometry_t geometry;
geometry.cylinders=0;
geometry.heads_per_cylinder=0;
@ -1379,15 +1601,25 @@ static void autoset_geometry(disk_t *disk, const unsigned char *buffer, const in
geometry.bytes_per_sector=0;
disk->arch->get_geometry_from_mbr(buffer, verbose, &geometry);
disk->autodetect=1;
if(geometry.sectors_per_head > 0 && geometry.heads_per_cylinder > 0)
if( geometry.heads_per_cylinder > 0 &&
geometry.heads_per_cylinder <= 255 &&
geometry.sectors_per_head > 0 &&
geometry.sectors_per_head <= 63
)
{
/*@ assert 0 < geometry.heads_per_cylinder <= 255; */
/*@ assert 0 < geometry.sectors_per_head <= 63; */
disk->geom.heads_per_cylinder=geometry.heads_per_cylinder;
disk->geom.sectors_per_head=geometry.sectors_per_head;
/*@ assert 0 < disk->geom.heads_per_cylinder <= 255; */
/*@ assert 0 < disk->geom.sectors_per_head <= 63; */
if(geometry.bytes_per_sector!=0)
{
disk->geom.bytes_per_sector=geometry.bytes_per_sector;
disk->sector_size=geometry.bytes_per_sector;
/*@ assert 0 < disk->sector_size; */
}
/*@ assert 0 < disk->sector_size; */
}
else
{
@ -1395,14 +1627,33 @@ static void autoset_geometry(disk_t *disk, const unsigned char *buffer, const in
disk->geom.sectors_per_head=63;
}
}
/*@ assert 0 < disk->sector_size; */
/*@ assert 0 < disk->geom.heads_per_cylinder <= 255; */
/*@ assert 0 < disk->geom.sectors_per_head <= 63; */
/* Round up because file is often truncated. */
disk->geom.cylinders=(disk->disk_size / disk->sector_size +
(uint64_t)disk->geom.sectors_per_head * disk->geom.heads_per_cylinder - 1) /
disk->geom.sectors_per_head / disk->geom.heads_per_cylinder;
}
/*@
@ requires \valid_read(hdr);
@ assigns \nothing;
@*/
static int is_dosemu_image(const struct dosemu_image_header *hdr)
{
if(memcmp(&hdr->sig,"DOSEMU",6)==0 &&
0 < le32(hdr->sectors) && le32(hdr->sectors) <= 63 &&
0 < le32(hdr->heads) && le32(hdr->heads) <= 255 &&
0 < le32(hdr->cylinders) &&
0 < le32(hdr->header_end))
return 1;
return 0;
}
disk_t *file_test_availability(const char *device, const int verbose, int testdisk_mode)
{
/*@ assert valid_read_string(device); */
disk_t *disk_car=NULL;
struct stat stat_rec;
int device_is_a_file=0;
@ -1525,10 +1776,29 @@ disk_t *file_test_availability(const char *device, const int verbose, int testdi
}
return NULL;
}
/*@ assert 0 <= hd_h; */
#ifdef DISABLED_FOR_FRAMAC
if(hd_h >= 1024)
return NULL;
/*@ assert 0 <= hd_h < 1024; */
#endif
disk_car=(disk_t *)MALLOC(sizeof(*disk_car));
disk_car->arch=&arch_none;
init_disk(disk_car);
#ifdef DISABLED_FOR_FRAMAC
disk_car->device=(char *)MALLOC(2048);
strncpy(disk_car->device, device, 2048);
disk_car->device[2048-1]='\0';
#else
disk_car->device=strdup(device);
#endif
if(disk_car->device==NULL)
{
free(disk_car);
close(hd_h);
return NULL;
}
/*@ assert valid_read_string(disk_car->device); */
data=(struct info_file_struct *)MALLOC(sizeof(*data));
data->handle=hd_h;
data->mode=mode;
@ -1539,22 +1809,27 @@ disk_t *file_test_availability(const char *device, const int verbose, int testdi
disk_car->pwrite=((mode&O_RDWR)==O_RDWR?&file_pwrite:&file_nopwrite);
disk_car->sync=&file_sync;
disk_car->access_mode=((mode&O_RDWR)==O_RDWR?TESTDISK_O_RDWR:TESTDISK_O_RDONLY);
disk_car->model=NULL;
#ifdef O_DIRECT
if((mode&O_DIRECT)==O_DIRECT)
disk_car->access_mode|=TESTDISK_O_DIRECT;
#endif
disk_car->clean=&file_clean;
#if !defined(DISABLED_FOR_FRAMAC)
if(fstat(hd_h,&stat_rec)>=0 &&
S_ISREG(stat_rec.st_mode) &&
stat_rec.st_size > 0)
#endif
{
device_is_a_file=1;
}
#ifndef DJGPP
if(device_is_a_file==0)
{
#ifndef DISABLED_FOR_FRAMAC
if(verbose>1)
log_info("file_test_availability %s is a device\n", device);
#endif
disk_car->sector_size=disk_get_sector_size(hd_h, device, verbose);
disk_get_geometry(&disk_car->geom, hd_h, device, verbose);
disk_car->disk_real_size=disk_get_size(hd_h, device, verbose, disk_car->sector_size);
@ -1576,8 +1851,11 @@ disk_t *file_test_availability(const char *device, const int verbose, int testdi
unsigned char *buffer;
const struct tdewf_file_header *ewf;
const uint8_t evf_file_signature[8] = { 'E', 'V', 'F', 0x09, 0x0D, 0x0A, 0xFF, 0x00 };
const struct dosemu_image_header *hdr;
#ifndef DISABLED_FOR_FRAMAC
if(verbose>1)
log_verbose("file_test_availability %s is a file\n", device);
#endif
disk_car->sector_size=DEFAULT_SECTOR_SIZE;
buffer=(unsigned char*)MALLOC(DEFAULT_SECTOR_SIZE);
ewf=(const struct tdewf_file_header *)buffer;
@ -1585,14 +1863,22 @@ disk_t *file_test_availability(const char *device, const int verbose, int testdi
{
memset(buffer,0,DEFAULT_SECTOR_SIZE);
}
if(memcmp(buffer,"DOSEMU",6)==0 && *(unsigned long*)(buffer+11)>0)
#ifdef __FRAMAC__
Frama_C_make_unknown((char *)buffer, DEFAULT_SECTOR_SIZE);
#endif
#ifndef DISABLED_FOR_FRAMAC
hdr=(const struct dosemu_image_header *)buffer;
if(is_dosemu_image(hdr))
{
log_info("%s DOSEMU\n",device);
disk_car->geom.cylinders=*(unsigned long*)(buffer+15);
disk_car->geom.heads_per_cylinder=*(unsigned long*)(buffer+7);
disk_car->geom.sectors_per_head=*(unsigned long*)(buffer+11);
disk_car->geom.cylinders=le32(hdr->cylinders);
/*@ assert 0 < disk_car->geom.cylinders < 4294967296; */
disk_car->geom.heads_per_cylinder=le32(hdr->heads);
/*@ assert 0 < disk_car->geom.heads_per_cylinder <= 255; */
disk_car->geom.sectors_per_head=le32(hdr->sectors);
/*@ assert 0 < disk_car->geom.sectors_per_head <= 63; */
disk_car->disk_real_size=(uint64_t)disk_car->geom.cylinders * disk_car->geom.heads_per_cylinder * disk_car->geom.sectors_per_head * disk_car->sector_size;
disk_car->offset=*(unsigned long*)(buffer+19);
disk_car->offset=le32(hdr->header_end);
}
else if(memcmp(buffer, evf_file_signature, 8)==0 && le16(ewf->fields_segment)==1)
{
@ -1611,6 +1897,7 @@ disk_t *file_test_availability(const char *device, const int verbose, int testdi
#endif
}
else
#endif
{
disk_car->geom.cylinders=0;
disk_car->geom.heads_per_cylinder=255;
@ -1626,18 +1913,20 @@ disk_t *file_test_availability(const char *device, const int verbose, int testdi
off_t pos;
pos=lseek(hd_h,0,SEEK_END);
if(pos>0 && (uint64_t)pos > disk_car->offset)
{
/*@ assert pos > disk_car->offset; */
disk_car->disk_real_size=(uint64_t)pos-disk_car->offset;
}
else
disk_car->disk_real_size=0;
}
#ifndef DISABLED_FOR_FRAMAC
autoset_geometry(disk_car,buffer,verbose);
#endif
}
free(buffer);
}
update_disk_car_fields(disk_car);
#if defined(POSIX_FADV_SEQUENTIAL) && defined(HAVE_POSIX_FADVISE)
// posix_fadvise(hd_h,0,0,POSIX_FADV_SEQUENTIAL);
#endif
if(disk_car->disk_real_size!=0)
{
#ifdef HDCLONE
@ -1653,14 +1942,22 @@ disk_t *file_test_availability(const char *device, const int verbose, int testdi
free(new_file);
}
#endif
/*@ assert 0 < disk_car->geom.cylinders < 0x2000000000000; */
/*@ assert 0 < disk_car->geom.heads_per_cylinder <= 255; */
/*@ assert 0 < disk_car->geom.sectors_per_head <= 63; */
/*@ assert valid_read_string(disk_car->device); */
/*@ assert valid_disk(disk_car); */
return disk_car;
}
/*@ assert disk_car->description == &file_description; */
#ifndef DISABLED_FOR_FRAMAC
if(disk_car->model==NULL)
log_warning("Warning: can't get size for %s, sector size=%u\n",
disk_car->description(disk_car), disk_car->sector_size);
file_description(disk_car), disk_car->sector_size);
else
log_warning("Warning: can't get size for %s, sector size=%u - %s\n",
disk_car->description(disk_car), disk_car->sector_size, disk_car->model);
file_description(disk_car), disk_car->sector_size, disk_car->model);
#endif
free(data);
free(disk_car->device);
free(disk_car->model);

7
src/hdcache.c
View file

@ -19,6 +19,7 @@
Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*/
#if !defined(DISABLED_FOR_FRAMAC)
#ifdef HAVE_CONFIG_H
#include <config.h>
#endif
@ -193,6 +194,7 @@ static int cache_pread(disk_t *disk_car, void *buffer, const unsigned int count,
@ requires valid_disk(disk_car);
@ requires \valid_read((char *)buffer + (0 .. count-1));
@ requires separation: \separated(disk_car, (const char *)buffer + (0 .. count-1));
@ decreases 0;
@*/
static int cache_pwrite(disk_t *disk_car, const void *buffer, const unsigned int count, const uint64_t offset)
{
@ -214,6 +216,7 @@ static int cache_pwrite(disk_t *disk_car, const void *buffer, const unsigned int
/*@
@ requires \valid(disk_car);
@ requires valid_disk(disk_car);
@ decreases 0;
@*/
static void cache_clean(disk_t *disk_car)
{
@ -241,6 +244,7 @@ static void cache_clean(disk_t *disk_car)
/*@
@ requires \valid(disk_car);
@ decreases 0;
@*/
static int cache_sync(disk_t *disk_car)
{
@ -267,6 +271,7 @@ static void dup_geometry(CHSgeometry_t * CHS_dst, const CHSgeometry_t * CHS_sour
/*@
@ requires \valid(disk_car);
@ requires valid_disk(disk_car);
@ decreases 0;
@ ensures valid_read_string(\result);
@*/
static const char *cache_description(disk_t *disk_car)
@ -283,6 +288,7 @@ static const char *cache_description(disk_t *disk_car)
/*@
@ requires \valid(disk_car);
@ requires valid_disk(disk_car);
@ decreases 0;
@ ensures valid_read_string(\result);
@*/
static const char *cache_description_short(disk_t *disk_car)
@ -339,3 +345,4 @@ disk_t *new_diskcache(disk_t *disk_car, const unsigned int testdisk_mode)
}
return new_disk_car;
}
#endif

2
src/hdcache.h
View file

@ -24,6 +24,7 @@
#ifdef __cplusplus
extern "C" {
#endif
#if !defined(DISABLED_FOR_FRAMAC)
/*@
@ requires \valid(disk_car);
@ -32,6 +33,7 @@ extern "C" {
@*/
disk_t *new_diskcache(disk_t *disk_car, const unsigned int cache_size_min);
#endif
#ifdef __cplusplus
} /* closing brace for extern "C" */
#endif

4
src/hidden.c
View file

@ -40,14 +40,14 @@ int is_hpa_or_dco(const disk_t *disk)
}
else if(disk->dco > 0 && disk->user_max < disk->dco+1)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("user_max=%llu dco=%llu\n",
(long long unsigned) disk->user_max,
(long long unsigned) disk->dco);
#endif
res|=2;
}
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
if(res>0)
{
if(res&1)

2
src/hiddenn.c
View file

@ -23,7 +23,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_NCURSES
#endif

2
src/hpa_dco.c
View file

@ -23,7 +23,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_LINUX_TYPES_H
#undef HAVE_LINUX_HDREG_H
#undef HAVE_SCSI_SG_H

12
src/intrf.c
View file

@ -102,6 +102,11 @@ int screen_buffer_add(const char *_format, ...)
return 0;
}
/*@
@ ensures intr_nbr_line == 0;
@ assigns intr_nbr_line;
@ assigns intr_buffer_screen[0 .. MAX_LINES-1][ 0 .. BUFFER_LINE_LENGTH];
@*/
void screen_buffer_reset(void)
{
intr_nbr_line=0;
@ -145,6 +150,10 @@ const char *aff_part_aux(const unsigned int newline, const disk_t *disk_car, con
return msg;
}
msg[sizeof(msg)-1]=0;
#ifdef DISABLED_FOR_FRAMAC
msg[0]='T';
msg[1]='\0';
#else
if((newline&AFF_PART_ORDER)==AFF_PART_ORDER)
{
if(partition->status!=STATUS_EXT_IN_EXT && partition->order!=NO_ORDER)
@ -189,6 +198,7 @@ const char *aff_part_aux(const unsigned int newline, const disk_t *disk_car, con
pos+=snprintf(&msg[pos],sizeof(msg)-pos-1, " [%s]",partition->partname);
if(partition->fsname[0]!='\0')
snprintf(&msg[pos],sizeof(msg)-pos-1, " [%s]",partition->fsname);
#endif
return msg;
}
@ -221,7 +231,7 @@ uint64_t ask_number_cli(char **current_cmd, const uint64_t val_cur, const uint64
/*@ assert valid_read_string(*current_cmd); */
if (val_min==val_max || (tmp_val >= val_min && tmp_val <= val_max))
return tmp_val;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
else
{
char res[200];

2
src/intrfn.c
View file

@ -23,7 +23,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_NCURSES
#endif

2
src/intrfn.h
View file

@ -26,7 +26,7 @@
extern "C" {
#endif
#if defined(HAVE_NCURSES) && !defined(MAIN_photorec)
#if defined(HAVE_NCURSES)
#ifdef HAVE_NCURSES_H
#include <ncurses.h>
#elif defined(HAVE_NCURSESW_NCURSES_H)

4
src/log.c
View file

@ -47,7 +47,7 @@
#include "common.h"
#include "log.h"
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
#undef HAVE_DUP2
#endif
@ -130,7 +130,7 @@ int log_open_default(const char*default_filename, const int mode, int *errsv)
#else
int log_open_default(const char*default_filename, const int mode, int *errsv)
{
#ifdef __FRAMAC__
#ifdef DISABLED_FOR_FRAMAC
return log_open(default_filename, mode, errsv);
#else
char*filename;

40
src/md.c
View file

@ -36,12 +36,12 @@
#include "fnctdsk.h"
#include "log.h"
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
static int test_MD(const disk_t *disk_car, const struct mdp_superblock_s *sb, const partition_t *partition, const int dump_ind)
{
if(le32(sb->md_magic)!=(unsigned int)MD_SB_MAGIC)
return 1;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("\nRaid magic value at %u/%u/%u\n",
offset2cylinder(disk_car,partition->part_offset),
offset2head(disk_car,partition->part_offset),
@ -67,7 +67,7 @@ static int test_MD_be(const disk_t *disk_car, const struct mdp_superblock_s *sb,
{
if(be32(sb->md_magic)!=(unsigned int)MD_SB_MAGIC)
return 1;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("\nRaid magic value at %u/%u/%u\n",
offset2cylinder(disk_car,partition->part_offset),
offset2head(disk_car,partition->part_offset),
@ -127,7 +127,7 @@ static void set_MD_info(const struct mdp_superblock_s *sb, partition_t *partitio
(unsigned int)le32(sb1->major_version),
(unsigned int)le32(sb1->level),
(long unsigned)le32(sb1->dev_number));
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
if(le32(sb1->max_dev) <= 384)
{
unsigned int i,d;
@ -151,7 +151,7 @@ static void set_MD_info(const struct mdp_superblock_s *sb, partition_t *partitio
}
#endif
}
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
if(verbose>0)
log_info("%s %s\n", partition->fsname, partition->info);
#endif
@ -195,7 +195,7 @@ static void set_MD_info_be(const struct mdp_superblock_s *sb, partition_t *parti
(unsigned int)be32(sb1->major_version),
(unsigned int)be32(sb1->level),
(long unsigned)be32(sb1->dev_number));
#if !defined(__FRAMAC__)
#if !defined(DISABLED_FOR_FRAMAC)
if(be32(sb1->max_dev) <= 384)
{
unsigned int i,d;
@ -219,7 +219,7 @@ static void set_MD_info_be(const struct mdp_superblock_s *sb, partition_t *parti
}
#endif
}
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
if(verbose>0)
log_info("%s %s\n", partition->fsname, partition->info);
#endif
@ -228,7 +228,7 @@ static void set_MD_info_be(const struct mdp_superblock_s *sb, partition_t *parti
int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
unsigned char *buffer=(unsigned char*)MALLOC(MD_SB_BYTES);
/* MD version 1.1 */
if(disk_car->pread(disk_car, buffer, MD_SB_BYTES, partition->part_offset) == MD_SB_BYTES)
@ -239,7 +239,7 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
le64(sb1->super_offset)==0 &&
test_MD(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("check_MD 1.1\n");
#endif
set_MD_info((struct mdp_superblock_s*)buffer, partition, verbose);
@ -251,7 +251,7 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
be64(sb1->super_offset)==0 &&
test_MD_be(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("check_MD 1.1 (BigEndian)\n");
#endif
set_MD_info_be((struct mdp_superblock_s*)buffer, partition, verbose);
@ -268,7 +268,7 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
le64(sb1->super_offset)==8 &&
test_MD(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("check_MD 1.2\n");
#endif
set_MD_info((struct mdp_superblock_s*)buffer, partition, verbose);
@ -280,7 +280,7 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
be64(sb1->super_offset)==8 &&
test_MD_be(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("check_MD 1.2 (BigEndian)\n");
#endif
set_MD_info_be((struct mdp_superblock_s*)buffer, partition, verbose);
@ -292,7 +292,7 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
{
const struct mdp_superblock_s *sb=(const struct mdp_superblock_s *)buffer;
const uint64_t offset=MD_NEW_SIZE_SECTORS(partition->part_size/512)*512;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
if(verbose>1)
{
log_verbose("Raid md 0.90 offset %llu\n", (long long unsigned)offset/512);
@ -304,7 +304,7 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
le32(sb->major_version)==0 &&
test_MD(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("check_MD 0.90\n");
#endif
set_MD_info((struct mdp_superblock_s*)buffer, partition, verbose);
@ -315,7 +315,7 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
be32(sb->major_version)==0 &&
test_MD_be(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("check_MD 0.90 (BigEndian)\n");
#endif
set_MD_info_be((struct mdp_superblock_s*)buffer, partition, verbose);
@ -328,7 +328,7 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
if(partition->part_size > 8*2*512)
{
const uint64_t offset=(uint64_t)(((partition->part_size/512)-8*2) & ~(4*2-1))*512;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
if(verbose>1)
{
log_verbose("Raid md 1.0 offset %llu\n", (long long unsigned)offset/512);
@ -342,7 +342,7 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
le64(sb1->super_offset)==(offset/512) &&
test_MD(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("check_MD 1.0\n");
#endif
set_MD_info((struct mdp_superblock_s*)buffer, partition, verbose);
@ -354,7 +354,7 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
be64(sb1->super_offset)==(offset/512) &&
test_MD_be(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("check_MD 1.0 (BigEndian)\n");
#endif
set_MD_info_be((struct mdp_superblock_s*)buffer, partition, verbose);
@ -370,7 +370,7 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
int recover_MD_from_partition(disk_t *disk_car, partition_t *partition, const int verbose)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
unsigned char *buffer=(unsigned char*)MALLOC(MD_SB_BYTES);
/* MD version 0.90 */
{
@ -408,7 +408,7 @@ int recover_MD_from_partition(disk_t *disk_car, partition_t *partition, const in
int recover_MD(const disk_t *disk_car, const struct mdp_superblock_s *sb, partition_t *partition, const int verbose, const int dump_ind)
{
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
if(test_MD(disk_car, sb, partition, dump_ind)==0)
{
set_MD_info(sb, partition, verbose);

8
src/misc.c
View file

@ -24,7 +24,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_STRPTIME
#undef HAVE_SYS_UTSNAME_H
#undef HAVE_UNAME
@ -233,6 +233,10 @@ https://msdn.microsoft.com/en-us/library/windows/desktop/ms724834%28v=vs.85%29.a
return "Apple";
#elif defined(__OS2__)
return "OS2";
#elif defined(DISABLED_FOR_FRAMAC)
const char *res="Frama-C";
/*@ assert valid_read_string(res); */
return res;
#else
return "unknown";
#endif
@ -286,6 +290,8 @@ const char *get_compiler(void)
#else
return "unknown compiler";
#endif
buffer[99]='\0';
/*@ assert valid_read_string(&buffer[0]); */
return buffer;
}

2
src/nodisk.c
View file

@ -23,7 +23,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_NCURSES
#endif

2
src/ntfs_dir.c
View file

@ -27,7 +27,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_LIBNTFS
#undef HAVE_LIBNTFS3G
#undef HAVE_SYS_PARAM_H

2
src/ntfs_io.c
View file

@ -26,7 +26,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_LIBNTFS
#undef HAVE_LIBNTFS3G
#endif

2
src/ntfs_udl.c
View file

@ -28,7 +28,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_LIBNTFS
#undef HAVE_LIBNTFS3G
#endif

2
src/ntfs_utl.c
View file

@ -27,7 +27,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_LIBNTFS
#undef HAVE_LIBNTFS3G
#endif

2
src/ntfsp.c
View file

@ -24,7 +24,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__) || defined(MAIN_photorec)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_LIBNTFS
#undef HAVE_LIBNTFS3G
#endif

53
src/partauto.c
View file

@ -34,13 +34,25 @@
#include "partauto.h"
#include "log.h"
extern const arch_fnct_t arch_gpt;
extern const arch_fnct_t arch_humax;
extern const arch_fnct_t arch_i386;
extern const arch_fnct_t arch_mac;
extern const arch_fnct_t arch_none;
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_GPT)
extern const arch_fnct_t arch_gpt;
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_HUMAX)
extern const arch_fnct_t arch_humax;
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_I386)
extern const arch_fnct_t arch_i386;
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_MAC)
extern const arch_fnct_t arch_mac;
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_SUN)
extern const arch_fnct_t arch_sun;
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_XBOX)
extern const arch_fnct_t arch_xbox;
#endif
void autodetect_arch(disk_t *disk, const arch_fnct_t *arch)
{
@ -55,42 +67,61 @@ void autodetect_arch(disk_t *disk, const arch_fnct_t *arch)
{
disk->arch=&arch_none;
list_part=arch_none.read_part(disk,verbose,0);
/*@ assert valid_list_part(list_part); */
if(list_part!=NULL && list_part->part!=NULL && list_part->part->upart_type==UP_UNK)
{
part_free_list(list_part);
list_part=NULL;
}
}
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_XBOX)
if(list_part==NULL)
{
disk->arch=&arch_xbox;
list_part=arch_xbox.read_part(disk,verbose,0);
/*@ assert valid_list_part(list_part); */
}
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_GPT)
if(list_part==NULL)
{
disk->arch=&arch_gpt;
list_part=arch_gpt.read_part(disk,verbose,0);
/*@ assert valid_list_part(list_part); */
}
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_HUMAX)
if(list_part==NULL)
{
disk->arch=&arch_humax;
list_part=arch_humax.read_part(disk,verbose,0);
/*@ assert valid_list_part(list_part); */
}
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_I386)
if(list_part==NULL)
{
disk->arch=&arch_i386;
list_part=arch_i386.read_part(disk,verbose,0);
/*@ assert valid_list_part(list_part); */
}
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_SUN)
if(list_part==NULL)
{
disk->arch=&arch_sun;
list_part=arch_sun.read_part(disk,verbose,0);
/*@ assert valid_list_part(list_part); */
}
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_MAC)
if(list_part==NULL)
{
disk->arch=&arch_mac;
list_part=arch_mac.read_part(disk,verbose,0);
/*@ assert valid_list_part(list_part); */
}
#endif
#ifndef DEBUG_PARTAUTO
log_set_levels(old_levels);
#endif
@ -108,25 +139,29 @@ void autodetect_arch(disk_t *disk, const arch_fnct_t *arch)
}
else
{
#ifdef TARGET_SOLARIS
#ifdef DISABLED_FOR_FRAMAC
disk->arch=&arch_none;
#elif defined(TARGET_SOLARIS) && (!defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_SUN))
disk->arch=&arch_sun;
#elif defined __APPLE__
#ifdef TESTDISK_LSB
#elif defined(__APPLE__) && defined(TESTDISK_LSB) && (!defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_GPT))
disk->arch=&arch_gpt;
#else
#elif defined(__APPLE__) && !defined(TESTDISK_LSB) && (!defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_MAC))
disk->arch=&arch_mac;
#endif
#else
#if defined(__CYGWIN__) || defined(__MINGW32__)
if(disk->device[0]=='\\' && disk->device[1]=='\\' && disk->device[2]=='.' && disk->device[3]=='\\' && disk->device[5]==':')
disk->arch=&arch_none;
else
#endif
#if !defined(SINGLE_PARTITION_TYPE) || (defined(SINGLE_PARTITION_I386) && defined(SINGLE_PARTITION_GPT))
/* PC/Intel partition table is limited to 2 TB, 2^32 512-bytes sectors */
if(disk->disk_size < ((uint64_t)1<<(32+9)))
disk->arch=&arch_i386;
else
disk->arch=&arch_gpt;
#else
disk->arch=&arch_none;
#endif
#endif
}
log_info("Partition table type defaults to %s\n", disk->arch->part_name);

4
src/partgpt.c
View file

@ -25,7 +25,7 @@
#include <config.h>
#endif
#if defined(__FRAMAC__)
#if defined(DISABLED_FOR_FRAMAC)
#undef HAVE_SYS_UUID_H
#undef HAVE_UUID_H
#undef HAVE_UUID_UUID_H
@ -595,7 +595,7 @@ static const char *get_gpt_typename(const efi_guid_t part_type_gpt)
for(i=0; gpt_sys_types[i].name!=NULL; i++)
if(guid_cmp(gpt_sys_types[i].part_type, part_type_gpt)==0)
return gpt_sys_types[i].name;
#ifndef __FRAMAC__
#ifndef DISABLED_FOR_FRAMAC
log_info("%8x %04x %04x %02x %02x %02x %02x %02x %02x %02x %02x\n",
part_type_gpt.time_low,
part_type_gpt.time_mid,

Some files were not shown because too many files have changed in this diff Show more