summaryrefslogtreecommitdiffstats
path: root/src/filegen.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/filegen.c')
-rw-r--r--src/filegen.c309
1 files changed, 234 insertions, 75 deletions
diff --git a/src/filegen.c b/src/filegen.c
index f48f21d..70b6913 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -38,8 +38,10 @@
#include "types.h"
#include "common.h"
#include "filegen.h"
-#include "photorec.h"
#include "log.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
static file_check_t file_check_plist={
.list = TD_LIST_HEAD_INIT(file_check_plist.list)
@@ -51,11 +53,18 @@ file_check_list_t file_check_list={
static unsigned int index_header_check(void);
+/*@
+ @ requires \valid_read(a);
+ @ requires \valid_read(b);
+ @*/
static int file_check_cmp(const struct td_list_head *a, const struct td_list_head *b)
{
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);
int res;
+ unsigned int min_length;
+ /*@ assert \valid_read(fc_a); */
+ /*@ assert \valid_read(fc_b); */
if(fc_a->length==0 && fc_b->length!=0)
return -1;
if(fc_a->length!=0 && fc_b->length==0)
@@ -63,23 +72,44 @@ static int file_check_cmp(const struct td_list_head *a, const struct td_list_hea
res=fc_a->offset-fc_b->offset;
if(res!=0)
return res;
- res=memcmp(fc_a->value,fc_b->value, (fc_a->length<=fc_b->length?fc_a->length:fc_b->length));
+ /*@ assert \valid_read((char *)fc_a->value + (0 .. fc_a->length - 1)); */
+ /*@ assert \initialized((char *)fc_a->value + (0 .. fc_a->length - 1)); */
+#if 0
+ /*@ assert \valid_read((char *)fc_b->value + (0 .. fc_b->length - 1)); */
+ /*@ assert \initialized((char *)fc_b->value + (0 .. fc_b->length - 1)); */
+#endif
+ min_length=fc_a->length<=fc_b->length?fc_a->length:fc_b->length;
+ res=memcmp(fc_a->value,fc_b->value, min_length);
if(res!=0)
return res;
- return fc_b->length-fc_a->length;
+ return (int)fc_b->length-(int)fc_a->length;
}
+/*@
+ @ requires \valid(file_check_new);
+ @ requires \valid(pos);
+ @*/
static void file_check_add_tail(file_check_t *file_check_new, file_check_list_t *pos)
{
unsigned int i;
+ const unsigned int tmp=(file_check_new->length==0?0:((const unsigned char *)file_check_new->value)[0]);
file_check_list_t *newe=(file_check_list_t *)MALLOC(sizeof(*newe));
newe->offset=file_check_new->offset;
+ /*@
+ @ loop unroll 256;
+ @ loop invariant 0 <= i <= 256;
+ @ loop assigns i, newe->file_checks[0 .. 255].list.prev, newe->file_checks[0 .. 255].list.next;
+ @ loop variant 255-i;
+ @*/
for(i=0;i<256;i++)
{
newe->file_checks[i].list.prev=&newe->file_checks[i].list;
newe->file_checks[i].list.next=&newe->file_checks[i].list;
+ /*@ assert newe->file_checks[i].list.prev == &newe->file_checks[i].list; */
+ /*@ assert newe->file_checks[i].list.next == &newe->file_checks[i].list; */
}
- td_list_add_tail(&file_check_new->list, &newe->file_checks[file_check_new->length==0?0:((const unsigned char *)file_check_new->value)[0]].list);
+ /*@ assert newe->file_checks[tmp].list.prev == &newe->file_checks[tmp].list; */
+ td_list_add_tail(&file_check_new->list, &newe->file_checks[tmp].list);
td_list_add_tail(&newe->list, &pos->list);
}
@@ -96,14 +126,19 @@ void register_header_check(const unsigned int offset, const void *value, const u
td_list_add_sorted(&file_check_new->list, &file_check_plist.list, file_check_cmp);
}
+/*@
+ @ requires \valid(file_check_new);
+ @*/
static void index_header_check_aux(file_check_t *file_check_new)
{
- struct td_list_head *tmp;
- td_list_for_each(tmp, &file_check_list.list)
+ if(file_check_new->length>0)
{
- file_check_list_t *pos=td_list_entry(tmp, file_check_list_t, list);
- if(file_check_new->length>0)
+ /*@ assert file_check_new->offset < 0x80000000; */
+ /*@ assert 0 < file_check_new->length <= 4096; */
+ struct td_list_head *tmp;
+ td_list_for_each(tmp, &file_check_list.list)
{
+ file_check_list_t *pos=td_list_entry(tmp, file_check_list_t, list);
if(pos->offset >= file_check_new->offset &&
pos->offset < file_check_new->offset+file_check_new->length)
{
@@ -147,6 +182,11 @@ void free_header_check(void)
{
unsigned int i;
file_check_list_t *pos=td_list_entry(tmpl, file_check_list_t, list);
+ /*@
+ @ loop unroll 256;
+ @ loop invariant 0 <= i <= 256;
+ @*/
+ /* TODO loop variant 255-i; */
for(i=0;i<256;i++)
{
struct td_list_head *tmp;
@@ -187,6 +227,9 @@ void file_allow_nl(file_recovery_t *file_recovery, const unsigned int nl_mode)
if(my_fseek(file_recovery->handle, file_recovery->file_size,SEEK_SET)<0)
return;
taille=fread(buffer,1, 4096,file_recovery->handle);
+#ifdef __FRAMAC__
+ Frama_C_make_unknown((char *)&buffer, 4096);
+#endif
if(taille > 0 && buffer[0]=='\n' && (nl_mode&NL_BARENL)==NL_BARENL)
file_recovery->file_size++;
else if(taille > 1 && buffer[0]=='\r' && buffer[1]=='\n' && (nl_mode&NL_CRLF)==NL_CRLF)
@@ -199,20 +242,35 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
{
unsigned char*buffer;
assert(footer_length < 4096);
- buffer=(unsigned char*)MALLOC(4096+footer_length-1);
+ /*@ assert 0 < footer_length < 4096; */
+ /*
+ * 4096+footer_length-1: required size
+ * 4096+footer_length: to avoid a Frama-C warning when footer_length==1
+ * 8192: maximum size
+ * */
+ buffer=(unsigned char*)MALLOC(4096+footer_length);
memset(buffer+4096,0,footer_length-1);
do
{
int i;
int taille;
- const unsigned int read_size=(offset%4096!=0 ? offset%4096 : 4096);
- offset-=read_size;
+ if(offset <= 4096)
+ offset=0;
+ else if(offset%4096==0)
+ offset-=4096;
+ else
+ offset=offset-(offset%4096);
if(my_fseek(handle,offset,SEEK_SET)<0)
{
free(buffer);
return 0;
}
- taille=fread(buffer, 1, read_size, handle);
+ taille=fread(buffer, 1, 4096, handle);
+ if(taille <= 0)
+ {
+ free(buffer);
+ return 0;
+ }
for(i=taille-1;i>=0;i--)
{
if(buffer[i]==*(const unsigned char *)footer && memcmp(buffer+i,footer,footer_length)==0)
@@ -234,10 +292,16 @@ void file_search_footer(file_recovery_t *file_recovery, const void*footer, const
file_recovery->file_size=file_rsearch(file_recovery->handle, file_recovery->file_size-extra_length, footer, footer_length);
if(file_recovery->file_size > 0)
file_recovery->file_size+= footer_length + extra_length;
+ /*@ assert \valid(file_recovery->handle); */
}
#if 0
-void file_search_lc_footer(file_recovery_t *file_recovery, const unsigned char*footer, const unsigned int footer_length)
+/*@
+ @ requires \valid(file_recovery);
+ @ requires footer_length > 0;
+ @ requires \valid_read((char *)footer+(0..footer_length-1));
+ @*/
+static void file_search_lc_footer(file_recovery_t *file_recovery, const unsigned char*footer, const unsigned int footer_length)
{
const unsigned int read_size=4096;
unsigned char*buffer;
@@ -317,7 +381,6 @@ void reset_file_recovery(file_recovery_t *file_recovery)
file_recovery->file_size=0;
file_recovery->location.list.prev=&file_recovery->location.list;
file_recovery->location.list.next=&file_recovery->location.list;
- file_recovery->location.start=0;
file_recovery->location.end=0;
file_recovery->location.data=0;
file_recovery->extension=NULL;
@@ -330,7 +393,6 @@ void reset_file_recovery(file_recovery_t *file_recovery)
file_recovery->offset_ok=0;
file_recovery->checkpoint_status=0;
file_recovery->checkpoint_offset=0;
-// file_recovery->blocksize=512;
file_recovery->flags=0;
file_recovery->extra=0;
}
@@ -368,23 +430,84 @@ file_stat_t * init_file_stats(file_enable_t *files_enable)
return file_stats;
}
-/* The original filename begins at offset in buffer and is null terminated */
-int file_rename(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int append_original_ext)
+/*@
+ @ requires \valid(file_recovery);
+ @ requires valid_read_string((const char*)&file_recovery->filename);
+ @ requires valid_read_string(new_ext);
+ @ ensures valid_read_string((char*)&file_recovery->filename);
+ @*/
+static int file_rename_aux(file_recovery_t *file_recovery, const char *new_ext)
+{
+ char new_filename[sizeof(file_recovery->filename)];
+ char *dst;
+ char *dst_dir_sep;
+ unsigned int len=strlen(file_recovery->filename)+1;
+ len+=strlen(new_ext);
+ /*@ assert valid_read_string(&file_recovery->filename[0]); */
+ if(len > sizeof(file_recovery->filename))
+ {
+ return -1;
+ }
+ /*@ assert len <= sizeof(file_recovery->filename); */
+ /*@ assert valid_read_string((char*)&file_recovery->filename); */
+ strcpy(new_filename, (char *)&file_recovery->filename);
+ dst_dir_sep=strrchr(new_filename, '/');
+#ifndef __FRAMAC__
+ /*@ assert valid_read_string(dst_dir_sep); */
+ dst=dst_dir_sep;
+ while(*dst!='.' && *dst!='\0')
+ dst++;
+ /* Add extension */
+ {
+ const char *src;
+ src=new_ext;
+ *dst++ = '.';
+ while(*src!='\0')
+ *dst++ = *src++;
+ *dst='\0';
+ }
+#endif
+ /*@ assert valid_read_string(&new_filename[0]); */
+ if(strlen(new_filename) >= sizeof(file_recovery->filename))
+ {
+ /*@ assert valid_read_string(&file_recovery->filename[0]); */
+ return -1;
+ }
+ /*@ assert valid_read_string(&new_filename[0]); */
+ if(rename(&file_recovery->filename[0], new_filename)<0)
+ {
+ /* Rename has failed */
+ /*@ assert valid_read_string(&file_recovery->filename[0]); */
+ return -1;
+ }
+ /*@ assert valid_read_string(&new_filename[0]); */
+ strcpy(file_recovery->filename, new_filename);
+ /*@ assert valid_read_string(&file_recovery->filename[0]); */
+ return 0;
+}
+
+/*@
+ @ requires \valid(file_recovery);
+ @ requires valid_read_string((char*)&file_recovery->filename);
+ @ requires 0 <= offset < buffer_size;
+ @ requires \valid_read((char *)buffer+(0..buffer_size-1));
+ @ requires new_ext==\null || valid_read_string(new_ext);
+ @ ensures valid_read_string((char*)&file_recovery->filename);
+ @*/
+static int _file_rename(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int append_original_ext)
{
- /* new_filename is large enough to avoid a buffer overflow */
char *new_filename;
const char *src=file_recovery->filename;
const char *ext=NULL;
char *dst;
char *directory_sep;
int len;
- if(buffer_size<0)
- return -1;
len=strlen(src)+1;
- if(offset < buffer_size && buffer!=NULL)
- len+=buffer_size-offset+1;
+ /*@ assert offset < buffer_size; */
+ len+=buffer_size-offset+1;
if(new_ext!=NULL)
len+=strlen(new_ext);
+#ifndef __FRAMAC__
new_filename=(char*)MALLOC(len);
dst=new_filename;
directory_sep=new_filename;
@@ -404,7 +527,6 @@ int file_rename(file_recovery_t *file_recovery, const void *buffer, const int bu
while(*dst!='.' && *dst!='\0')
dst++;
/* Add original filename */
- if(offset < buffer_size && buffer!=NULL)
{
char *dst_old=dst;
int off;
@@ -468,56 +590,72 @@ int file_rename(file_recovery_t *file_recovery, const void *buffer, const int bu
}
}
*dst='\0';
- if(rename(file_recovery->filename, new_filename)<0)
- {
- /* Rename has failed */
- free(new_filename);
- if(buffer==NULL)
- return -1;
- /* Try without the original filename */
- return file_rename(file_recovery, NULL, 0, 0, new_ext, append_original_ext);
- }
- if(strlen(new_filename)<sizeof(file_recovery->filename))
+ /*@ assert valid_read_string(new_filename); */
+ /*@ assert valid_read_string(&file_recovery->filename[0]); */
+ if(strlen(new_filename)<sizeof(file_recovery->filename) && rename(file_recovery->filename, new_filename)==0)
{
strcpy(file_recovery->filename, new_filename);
+ free(new_filename);
+ /*@ assert valid_read_string(&file_recovery->filename[0]); */
+ return 0;
+
}
free(new_filename);
- return 0;
+#endif
+ /*@ assert valid_read_string(&file_recovery->filename[0]); */
+ return -1;
}
/* The original filename begins at offset in buffer and is null terminated */
-int file_rename_unicode(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int append_original_ext)
+int file_rename(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int append_original_ext)
+{
+ if(buffer!=NULL && 0 <= offset && offset < buffer_size &&
+ _file_rename(file_recovery, buffer, buffer_size, offset, new_ext, append_original_ext)==0)
+ return 0;
+ if(new_ext==NULL)
+ return 0;
+ /* Try without the original filename */
+ return file_rename_aux(file_recovery, new_ext);
+}
+
+/* The original filename begins at offset in buffer and is null terminated */
+/*@
+ @ requires \valid(file_recovery);
+ @ requires valid_read_string((char*)&file_recovery->filename);
+ @ requires 0 <= offset < buffer_size;
+ @ requires \valid_read((char *)buffer+(0..buffer_size-1));
+ @ requires new_ext==\null || valid_read_string(new_ext);
+ @ ensures valid_read_string((char*)&file_recovery->filename);
+ @*/
+static int _file_rename_unicode(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int append_original_ext)
{
- /* new_filename is large enough to avoid a buffer overflow */
char *new_filename;
const char *src=file_recovery->filename;
- const char *ext=src;
+ const char *src_ext=src;
char *dst;
- char *directory_sep;
+ char *dst_dir_sep;
int len=strlen(src)+1;
- if(buffer_size<0)
- return -1;
- if(offset < buffer_size && buffer!=NULL)
- len+=buffer_size-offset;
+ /*@ assert offset < buffer_size; */
+ len+=buffer_size-offset;
if(new_ext!=NULL)
len+=strlen(new_ext);
+#ifndef __FRAMAC__
new_filename=(char*)MALLOC(len);
dst=new_filename;
- directory_sep=dst;
+ dst_dir_sep=dst;
while(*src!='\0')
{
if(*src=='/')
- directory_sep=dst;
+ dst_dir_sep=dst;
if(*src=='.')
- ext=src;
+ src_ext=src;
*dst++ = *src++;
}
*dst='\0';
- dst=directory_sep;
+ dst=dst_dir_sep;
while(*dst!='.' && *dst!='\0')
dst++;
/* Add original filename */
- if(offset < buffer_size && buffer!=NULL)
{
char *dst_old=dst;
int off;
@@ -572,31 +710,46 @@ int file_rename_unicode(file_recovery_t *file_recovery, const void *buffer, cons
while(*src!='\0')
*dst++ = *src++;
}
- else if(append_original_ext>0)
+ else if(append_original_ext>0 && src_ext!=NULL)
{
- while(*ext!='\0')
- *dst++ = *ext++;
+ while(*src_ext!='\0')
+ *dst++ = *src_ext++;
}
*dst='\0';
- if(rename(file_recovery->filename, new_filename)<0)
- {
- /* Rename has failed */
- free(new_filename);
- if(buffer==NULL)
- return -1;
- /* Try without the original filename */
- return file_rename_unicode(file_recovery, NULL, 0, 0, new_ext, append_original_ext);
- }
- if(strlen(new_filename)<sizeof(file_recovery->filename))
+ if(strlen(new_filename)<sizeof(file_recovery->filename) && rename(file_recovery->filename, new_filename)==0)
{
strcpy(file_recovery->filename, new_filename);
+ free(new_filename);
+ /*@ assert valid_read_string(&file_recovery->filename[0]); */
+ return 0;
}
free(new_filename);
- return 0;
+#endif
+ /*@ assert valid_read_string(&file_recovery->filename[0]); */
+ return -1;
+}
+
+int file_rename_unicode(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int append_original_ext)
+{
+ if(buffer!=NULL && 0 <= offset && offset < buffer_size &&
+ _file_rename_unicode(file_recovery, buffer, buffer_size, offset, new_ext, append_original_ext)==0)
+ return 0;
+ if(new_ext==NULL)
+ return 0;
+ return file_rename_aux(file_recovery, new_ext);
}
static uint64_t offset_skipped_header=0;
+/*@
+ @ assigns offset_skipped_header;
+ @*/
+void header_ignored_cond_reset(uint64_t start, uint64_t end)
+{
+ if(start <= offset_skipped_header && offset_skipped_header <= end)
+ offset_skipped_header=0;
+}
+
/* 0: file_recovery is bad *
* 1: file_recovery is ok */
int header_ignored_adv(const file_recovery_t *file_recovery, const file_recovery_t *file_recovery_new)
@@ -612,13 +765,15 @@ int header_ignored_adv(const file_recovery_t *file_recovery, const file_recovery
}
if(file_recovery->handle==NULL)
{
- if(file_recovery_new->location.start==0 || offset_skipped_header==0)
+ if(file_recovery_new->location.start < offset_skipped_header || offset_skipped_header==0)
+ {
offset_skipped_header=file_recovery_new->location.start;
+ }
return 0;
}
memcpy(&fr_test, file_recovery, sizeof(fr_test));
-#ifdef HAVE_FTELLO
+#if defined(HAVE_FTELLO) && !defined(__FRAMAC__)
if((offset=ftello(file_recovery->handle)) < 0)
offset=ftell(file_recovery->handle);
#else
@@ -626,15 +781,17 @@ int header_ignored_adv(const file_recovery_t *file_recovery, const file_recovery
#endif
assert(offset >= 0);
file_recovery->file_check(&fr_test);
- if(fr_test.file_size>0)
- return 1;
if(my_fseek(file_recovery->handle, offset, SEEK_SET) < 0)
{
log_error("BUG in header_ignored_adv: my_fseek() failed\n");
return 1;
}
- if(file_recovery_new->location.start==0 || offset_skipped_header==0)
+ if(fr_test.file_size>0)
+ return 1;
+ if(file_recovery_new->location.start < offset_skipped_header || offset_skipped_header==0)
+ {
offset_skipped_header=file_recovery_new->location.start;
+ }
return 0;
}
@@ -645,7 +802,7 @@ void header_ignored(const file_recovery_t *file_recovery_new)
offset_skipped_header=0;
return ;
}
- if(file_recovery_new->location.start==0 || offset_skipped_header==0)
+ if(file_recovery_new->location.start < offset_skipped_header || offset_skipped_header==0)
offset_skipped_header=file_recovery_new->location.start;
}
@@ -669,7 +826,7 @@ void get_prev_location_smart(alloc_data_t *list_search_space, alloc_data_t **cur
if(file_space->start < prev_location)
break;
}
-#ifdef DEBUG_HEADER_CHECK
+#ifdef DEBUG_PREV_LOCATION
log_info("get_prev_location_smart: reset offset_skipped_header=%llu, offset=%llu\n",
(long long unsigned)(offset_skipped_header/512),
(long long unsigned)(*offset/512));
@@ -682,24 +839,26 @@ void get_prev_location_smart(alloc_data_t *list_search_space, alloc_data_t **cur
offset_skipped_header=0;
return;
}
- if(file_space->start < prev_location || file_space->start < offset_skipped_header)
+ *current_search_space=file_space;
+ if(file_space->start < offset_skipped_header)
{
-#ifdef DEBUG_HEADER_CHECK
- log_info("get_prev_location_smart: file_space->start < prev_location=%llu (in 512-bytes sectors), offset=%llu\n",
+#ifdef DEBUG_PREV_LOCATION
+ log_info("get_prev_location_smart: file_space->start < offset_skipped_header, prev_location=%llu (in 512-bytes sectors), offset=%llu => %llu\n",
(long long unsigned)(prev_location/512),
- (long long unsigned)(*offset/512));
+ (long long unsigned)(*offset/512),
+ (long long unsigned)(offset_skipped_header/512));
#endif
+ *offset=offset_skipped_header;
offset_skipped_header=0;
return ;
}
- *current_search_space=file_space;
*offset=file_space->start;
}
}
int my_fseek(FILE *stream, off_t offset, int whence)
{
-#if defined(HAVE_FSEEKO) && !defined(__MINGW32__) && !defined(__ARM_EABI__)
+#if defined(HAVE_FSEEKO) && !defined(__MINGW32__) && !defined(__ARM_EABI__) && !defined(__FRAMAC__)
{
int res;
if((res=fseeko(stream, offset, whence))>=0)
@@ -725,7 +884,7 @@ time_t get_time_from_YYMMDDHHMMSS(const char *date_asc)
return mktime(&tm_time);
}
-time_t get_time_from_YYYY_MM_DD_HH_MM_SS(const char *date_asc)
+time_t get_time_from_YYYY_MM_DD_HH_MM_SS(const unsigned char *date_asc)
{
struct tm tm_time;
if(memcmp(date_asc, "0000", 4)==0)