summaryrefslogtreecommitdiffstats
path: root/src/file_mov.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/file_mov.c')
-rw-r--r--src/file_mov.c484
1 files changed, 358 insertions, 126 deletions
diff --git a/src/file_mov.c b/src/file_mov.c
index dc9c138..6e71676 100644
--- a/src/file_mov.c
+++ b/src/file_mov.c
@@ -32,12 +32,12 @@
#include "filegen.h"
#include "common.h"
#include "log.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
static void register_header_check_mov(file_stat_t *file_stat);
static void register_header_check_mov_mdat(file_stat_t *file_stat);
-static int header_check_mov(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);
-static int header_check_mov_aux(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);
-static data_check_t data_check_mov(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
const file_hint_t file_hint_mov= {
.extension="mov",
@@ -57,30 +57,13 @@ const file_hint_t file_hint_mov_mdat= {
.register_header_check=&register_header_check_mov_mdat
};
-static void register_header_check_mov_mdat(file_stat_t *file_stat)
-{
- register_header_check(4, (const unsigned char*)"mdat",4, &header_check_mov_aux, 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);
- 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);
- register_header_check(4, (const unsigned char*)"ftyp",4, &header_check_mov_aux, file_stat);
- register_header_check(4, (const unsigned char*)"jp2h",4, &header_check_mov, file_stat);
- register_header_check(4, (const unsigned char*)"mdat",4, &header_check_mov, file_stat);
- register_header_check(4, (const unsigned char*)"mdia",4, &header_check_mov, file_stat);
- register_header_check(4, (const unsigned char*)"moov",4, &header_check_mov, file_stat);
- register_header_check(4, (const unsigned char*)"PICT",4, &header_check_mov, file_stat);
- register_header_check(4, (const unsigned char*)"pnot",4, &header_check_mov, file_stat);
- register_header_check(4, (const unsigned char*)"skip",4, &header_check_mov, file_stat);
- register_header_check(4, (const unsigned char*)"stbl",4, &header_check_mov, file_stat);
- register_header_check(4, (const unsigned char*)"trak",4, &header_check_mov, file_stat);
- register_header_check(4, (const unsigned char*)"wide",4, &header_check_mov, file_stat);
- register_header_check(4, (const unsigned char*)"jP ",4, &header_check_mov, file_stat);
-}
+static const char *extension_mp4="mp4";
+static const char *extension_m4p="m4p";
+static const char *extension_3gp="3gp";
+static const char *extension_3g2="3g2";
+static const char *extension_heic="heic";
+static const char *extension_jp2="jp2";
+static const char *extension_cr3="cr3";
struct atom_struct
{
@@ -95,6 +78,10 @@ struct atom64_struct
uint64_t size;
} __attribute__ ((gcc_struct, __packed__));
+/*@
+ @ requires \valid(file_recovery);
+ @ requires valid_read_string((char*)file_recovery->filename);
+ @*/
static void file_rename_mov(file_recovery_t *file_recovery)
{
FILE *file;
@@ -107,29 +94,138 @@ static void file_rename_mov(file_recovery_t *file_recovery)
return ;
}
fclose(file);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, sizeof(buffer));
+#endif
buffer[8]='\0';
file_rename(file_recovery, buffer, sizeof(buffer), 4, NULL, 1);
}
-static int header_check_mov(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)
+/*@
+ @ requires buffer_size >= 16;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ requires \valid(file_recovery);
+ @ requires file_recovery->data_check==&data_check_mov;
+ @ requires file_recovery->file_size == 0 || file_recovery->calculated_file_size > file_recovery->file_size - 16;
+ @ ensures \result == DC_CONTINUE || \result == DC_STOP;
+ @ ensures \result == DC_CONTINUE ==> (file_recovery->calculated_file_size > file_recovery->file_size + buffer_size/2 - 16);
+ @*/
+static data_check_t data_check_mov(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{
- if(file_recovery->file_stat!=NULL &&
- file_recovery->file_stat->file_hint==&file_hint_mov &&
- (file_recovery->calculated_file_size == file_recovery->file_size ||
- file_recovery->blocksize < 16))
- { /* PhotoRec is already trying to recover this mov file */
- header_ignored(file_recovery_new);
- return 0;
+ while(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size &&
+ file_recovery->calculated_file_size + 8 <= file_recovery->file_size + buffer_size/2)
+ {
+ const unsigned int i=file_recovery->calculated_file_size + buffer_size/2 - file_recovery->file_size;
+ /*@ assert 0 <= i <= buffer_size - 8 ; */
+ const struct atom_struct *atom=(const struct atom_struct*)&buffer[i];
+ uint64_t atom_size=be32(atom->size);
+ if(atom_size==1)
+ {
+ const struct atom64_struct *atom64;
+ if(i + 16 > buffer_size)
+ {
+ /*@ assert file_recovery->calculated_file_size + buffer_size/2 - file_recovery->file_size + 16 > buffer_size; */
+ /*@ assert file_recovery->calculated_file_size > file_recovery->file_size + buffer_size/2 - 16; */
+ return DC_CONTINUE;
+ }
+ /*@ assert i + 16 <= buffer_size; */
+ atom64=(const struct atom64_struct*)&buffer[i];
+ atom_size=be64(atom64->size);
+ if(atom_size<16)
+ return DC_STOP;
+ }
+ else if(atom_size<8)
+ return DC_STOP;
+ if(atom_size >= 0x80000000)
+ return DC_STOP;
+#ifdef DEBUG_MOV
+ log_trace("file_mov.c: %s atom %c%c%c%c (0x%02x%02x%02x%02x) size %llu, calculated_file_size %llu\n",
+ file_recovery->filename,
+ buffer[i+4],buffer[i+5],buffer[i+6],buffer[i+7],
+ buffer[i+4],buffer[i+5],buffer[i+6],buffer[i+7],
+ (long long unsigned)atom_size,
+ (long long unsigned)file_recovery->calculated_file_size);
+#endif
+ if(buffer[i+4]=='m' && buffer[i+5]=='d' && buffer[i+6]=='a' && buffer[i+7]=='t')
+ {
+ file_recovery->calculated_file_size+=atom_size;
+#if 0
+ if(i+8 == buffer_size)
+ {
+ return -((atom_size + buffer_size/2 - 1)/ (buffer_size/2));
+ }
+#endif
+ }
+ else if( (buffer[i+4]=='c' && buffer[i+5]=='m' && buffer[i+6]=='o' && buffer[i+7]=='v') ||
+ (buffer[i+4]=='c' && buffer[i+5]=='m' && buffer[i+6]=='v' && buffer[i+7]=='d') ||
+ (buffer[i+4]=='d' && buffer[i+5]=='c' && buffer[i+6]=='o' && buffer[i+7]=='m') ||
+ (buffer[i+4]=='f' && buffer[i+5]=='r' && buffer[i+6]=='e' && buffer[i+7]=='a') ||
+ (buffer[i+4]=='f' && buffer[i+5]=='r' && buffer[i+6]=='e' && buffer[i+7]=='e') ||
+ (buffer[i+4]=='f' && buffer[i+5]=='t' && buffer[i+6]=='y' && buffer[i+7]=='p') ||
+ (buffer[i+4]=='j' && buffer[i+5]=='p' && buffer[i+6]=='2' && buffer[i+7]=='h') ||
+ (buffer[i+4]=='m' && buffer[i+5]=='d' && buffer[i+6]=='i' && buffer[i+7]=='a') ||
+ (buffer[i+4]=='m' && buffer[i+5]=='e' && buffer[i+6]=='t' && buffer[i+7]=='a') ||
+ (buffer[i+4]=='m' && buffer[i+5]=='o' && buffer[i+6]=='o' && buffer[i+7]=='v') ||
+ (buffer[i+4]=='P' && buffer[i+5]=='I' && buffer[i+6]=='C' && buffer[i+7]=='T') ||
+ (buffer[i+4]=='p' && buffer[i+5]=='n' && buffer[i+6]=='o' && buffer[i+7]=='t') ||
+ (buffer[i+4]=='s' && buffer[i+5]=='k' && buffer[i+6]=='i' && buffer[i+7]=='p') ||
+ (buffer[i+4]=='s' && buffer[i+5]=='t' && buffer[i+6]=='b' && buffer[i+7]=='l') ||
+ (buffer[i+4]=='t' && buffer[i+5]=='h' && buffer[i+6]=='u' && buffer[i+7]=='m') ||
+ (buffer[i+4]=='t' && buffer[i+5]=='r' && buffer[i+6]=='a' && buffer[i+7]=='k') ||
+ (buffer[i+4]=='u' && buffer[i+5]=='u' && buffer[i+6]=='i' && buffer[i+7]=='d') ||
+ (buffer[i+4]=='w' && buffer[i+5]=='i' && buffer[i+6]=='d' && buffer[i+7]=='e') )
+ {
+ file_recovery->calculated_file_size+=atom_size;
+ }
+ else
+ {
+ 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],
+ (long long unsigned)file_recovery->calculated_file_size);
+ return DC_STOP;
+ }
}
- return header_check_mov_aux(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+ /*@ assert file_recovery->calculated_file_size < file_recovery->file_size - buffer_size/2 || file_recovery->calculated_file_size > file_recovery->file_size + buffer_size/2 - 8; */
+ /*@ assert file_recovery->calculated_file_size > file_recovery->file_size + buffer_size/2 - 8; */
+#ifdef DEBUG_MOV
+ log_trace("file_mov.c: new calculated_file_size %llu\n",
+ (long long unsigned)file_recovery->calculated_file_size);
+#endif
+ return DC_CONTINUE;
}
+/*@
+ @ requires buffer_size >= 16;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ requires \valid_read(file_recovery);
+ @ requires \valid(file_recovery_new);
+ @ requires file_recovery_new->blocksize > 0;
+ @ requires separation: \separated(file_recovery, file_recovery_new);
+ @ ensures \result == 0 || \result == 1;
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_mov.extension ||
+ file_recovery_new->extension == extension_3g2 ||
+ file_recovery_new->extension == extension_3gp ||
+ file_recovery_new->extension == extension_cr3 ||
+ file_recovery_new->extension == extension_heic ||
+ file_recovery_new->extension == extension_jp2 ||
+ file_recovery_new->extension == extension_m4p ||
+ file_recovery_new->extension == extension_mp4);
+ @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == &file_rename_mov || file_recovery_new->file_rename == \null);
+ @ ensures (\result == 1 && file_recovery_new->extension == file_hint_mov.extension) ==> (file_recovery_new->file_rename == file_rename_mov);
+ @ ensures (\result == 1 && file_recovery_new->extension != file_hint_mov.extension) ==> (file_recovery_new->file_rename == \null);
+ @ ensures (\result == 1 && (file_recovery_new->extension == extension_jp2 || file_recovery_new->blocksize < 16)) ==> (file_recovery_new->data_check == \null && file_recovery_new->file_check == \null && file_recovery_new->file_rename == \null && file_recovery_new->min_filesize > 0);
+ @ ensures (\result == 1 && file_recovery_new->extension != extension_jp2 && file_recovery_new->blocksize >= 16) ==> (file_recovery_new->calculated_file_size > 0 && file_recovery_new->file_check == &file_check_size && file_recovery_new->data_check == &data_check_mov);
+ @*/
static int header_check_mov_aux(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)
{
uint64_t i=0;
- while(i<buffer_size-16)
+ while(i <= buffer_size-16)
{
+ /*@ assert i <= buffer_size - 16; */
const struct atom_struct *atom=(const struct atom_struct*)&buffer[i];
+ uint64_t calculated_file_size;
uint64_t atom_size=be32(atom->size);
if(atom_size==1)
{
@@ -137,47 +233,65 @@ static int header_check_mov_aux(const unsigned char *buffer, const unsigned int
atom_size=be64(atom64->size);
if(atom_size<16)
return 0;
+ /*@ assert atom_size >= 16; */
}
else if(atom_size<8)
return 0;
+ /*@ assert 8 <= atom_size; */
+ if(atom_size >= 0x80000000)
+ return 0;
+ /*@ assert 8 <= atom_size < 0x80000000; */
+ calculated_file_size=atom_size+i;
/* check for commun atom type */
if(buffer[i+4]=='p' && buffer[i+5]=='n' && buffer[i+6]=='o' && buffer[i+7]=='t')
{
if(atom_size != 20)
return 0;
+ /*@ assert atom_size == 20; */
reset_file_recovery(file_recovery_new);
file_recovery_new->extension=file_hint_mov.extension;
file_recovery_new->file_rename=&file_rename_mov;
- if(file_recovery->blocksize < 16)
+ if(file_recovery_new->blocksize < 16)
+ {
+ file_recovery_new->min_filesize=calculated_file_size;
return 1;
+ }
file_recovery_new->data_check=&data_check_mov;
file_recovery_new->file_check=&file_check_size;
- file_recovery_new->calculated_file_size=i+atom_size;
+ file_recovery_new->calculated_file_size=calculated_file_size;
return 1;
}
if(buffer[i+4]=='w' && buffer[i+5]=='i' && buffer[i+6]=='d' && buffer[i+7]=='e')
{
if(atom_size != 8)
return 0;
+ /*@ assert atom_size == 8; */
reset_file_recovery(file_recovery_new);
file_recovery_new->extension=file_hint_mov.extension;
file_recovery_new->file_rename=&file_rename_mov;
- if(file_recovery->blocksize < 16)
+ if(file_recovery_new->blocksize < 16)
+ {
+ file_recovery_new->min_filesize=calculated_file_size;
return 1;
+ }
file_recovery_new->data_check=&data_check_mov;
file_recovery_new->file_check=&file_check_size;
- file_recovery_new->calculated_file_size=i+atom_size;
+ file_recovery_new->calculated_file_size=calculated_file_size;
return 1;
}
if(buffer[i+4]=='m' && buffer[i+5]=='o' && buffer[i+6]=='o' && buffer[i+7]=='v')
{
if(atom_size > 256*256*256)
return 0;
+ /*@ assert atom_size <= 256*256*256; */
reset_file_recovery(file_recovery_new);
file_recovery_new->extension=file_hint_mov.extension;
file_recovery_new->file_rename=&file_rename_mov;
- if(file_recovery->blocksize < 16)
+ if(file_recovery_new->blocksize < 16)
+ {
+ file_recovery_new->min_filesize=calculated_file_size;
return 1;
+ }
/*
if(i==0 && buffer[12]=='m' && buffer[13]=='v' && buffer[14]=='h' && buffer[15]=='d')
{
@@ -188,13 +302,14 @@ static int header_check_mov_aux(const unsigned char *buffer, const unsigned int
*/
file_recovery_new->data_check=&data_check_mov;
file_recovery_new->file_check=&file_check_size;
- file_recovery_new->calculated_file_size=i+atom_size;
+ file_recovery_new->calculated_file_size=calculated_file_size;
return 1;
}
if(buffer[i+4]=='f' && buffer[i+5]=='t' && buffer[i+6]=='y' && buffer[i+7]=='p')
{
if(atom_size < 20 || (atom_size&3)!=0 || atom_size>256)
return 0;
+ /*@ assert 20 <= atom_size <= 256; */
if(memcmp(&buffer[i+8], "isom", 4)==0 ||
memcmp(&buffer[i+8], "mp41", 4)==0 ||
memcmp(&buffer[i+8], "mp42", 4)==0 ||
@@ -203,92 +318,117 @@ static int header_check_mov_aux(const unsigned char *buffer, const unsigned int
memcmp(&buffer[i+8], "M4P", 3)==0)
{
reset_file_recovery(file_recovery_new);
- file_recovery_new->extension="mp4";
+ file_recovery_new->extension=extension_mp4;
if(file_recovery->blocksize < 16)
+ {
+ file_recovery_new->min_filesize=calculated_file_size;
return 1;
+ }
file_recovery_new->data_check=&data_check_mov;
file_recovery_new->file_check=&file_check_size;
- file_recovery_new->calculated_file_size=i+atom_size;
+ file_recovery_new->calculated_file_size=calculated_file_size;
return 1;
}
else if(memcmp(&buffer[i+8], "M4A ", 4)==0)
{
reset_file_recovery(file_recovery_new);
/* acc ? */
- file_recovery_new->extension="m4p";
+ file_recovery_new->extension=extension_m4p;
if(file_recovery->blocksize < 16)
+ {
+ file_recovery_new->min_filesize=calculated_file_size;
return 1;
+ }
file_recovery_new->data_check=&data_check_mov;
file_recovery_new->file_check=&file_check_size;
- file_recovery_new->calculated_file_size=i+atom_size;
+ file_recovery_new->calculated_file_size=calculated_file_size;
return 1;
}
else if(memcmp(&buffer[i+8], "3gp", 3)==0)
{
/* Video for 3G mobile phone (GSM) */
reset_file_recovery(file_recovery_new);
- file_recovery_new->extension="3gp";
+ file_recovery_new->extension=extension_3gp;
if(file_recovery->blocksize < 16)
+ {
+ file_recovery_new->min_filesize=calculated_file_size;
return 1;
+ }
file_recovery_new->data_check=&data_check_mov;
file_recovery_new->file_check=&file_check_size;
- file_recovery_new->calculated_file_size=i+atom_size;
+ file_recovery_new->calculated_file_size=calculated_file_size;
return 1;
}
else if(memcmp(&buffer[i+8], "3g2", 3)==0)
{
/* Video for 3G mobile phone (CDMA) */
reset_file_recovery(file_recovery_new);
- file_recovery_new->extension="3g2";
+ file_recovery_new->extension=extension_3g2;
+ if(file_recovery->blocksize < 16)
+ {
+ file_recovery_new->min_filesize=calculated_file_size;
+ return 1;
+ }
file_recovery_new->data_check=&data_check_mov;
file_recovery_new->file_check=&file_check_size;
- file_recovery_new->calculated_file_size=i+atom_size;
+ file_recovery_new->calculated_file_size=calculated_file_size;
return 1;
}
else if(memcmp(&buffer[i+8], "heic", 4)==0)
{
reset_file_recovery(file_recovery_new);
- file_recovery_new->extension="heic";
+ file_recovery_new->extension=extension_heic;
+ if(file_recovery->blocksize < 16)
+ {
+ file_recovery_new->min_filesize=calculated_file_size;
+ return 1;
+ }
file_recovery_new->data_check=&data_check_mov;
file_recovery_new->file_check=&file_check_size;
- file_recovery_new->calculated_file_size=i+atom_size;
+ file_recovery_new->calculated_file_size=calculated_file_size;
return 1;
}
else if(memcmp(&buffer[i+8], "jp2 ", 4)==0)
{
reset_file_recovery(file_recovery_new);
- file_recovery_new->extension="jp2";
+ file_recovery_new->extension=extension_jp2;
+ file_recovery_new->min_filesize=calculated_file_size;
/* jP + ftyp "jp2 " + jp2h + jp2c (atom_size=0) => no data check */
return 1;
}
else if(memcmp(&buffer[i+8], "qt ", 4)==0)
{
reset_file_recovery(file_recovery_new);
- file_recovery_new->extension="mov";
+ file_recovery_new->extension=file_hint_mov.extension;
file_recovery_new->file_rename=&file_rename_mov;
if(file_recovery->blocksize < 16)
+ {
+ file_recovery_new->min_filesize=calculated_file_size;
return 1;
+ }
file_recovery_new->data_check=&data_check_mov;
file_recovery_new->file_check=&file_check_size;
- file_recovery_new->calculated_file_size=i+atom_size;
+ file_recovery_new->calculated_file_size=calculated_file_size;
return 1;
}
else if(memcmp(&buffer[i+8], "crx ", 4)==0)
{
reset_file_recovery(file_recovery_new);
- file_recovery_new->extension="cr3";
- file_recovery_new->file_rename=&file_rename_mov;
+ file_recovery_new->extension=extension_cr3;
if(file_recovery->blocksize < 16)
+ {
+ file_recovery_new->min_filesize=calculated_file_size;
return 1;
+ }
file_recovery_new->data_check=&data_check_mov;
file_recovery_new->file_check=&file_check_size;
- file_recovery_new->calculated_file_size=i+atom_size;
+ file_recovery_new->calculated_file_size=calculated_file_size;
return 1;
}
}
if(buffer[i+4]=='m' && buffer[i+5]=='d' && buffer[i+6]=='a' && buffer[i+7]=='t')
{
- if(memcmp(buffer, "der.mdat\" anim=\"", 16)==0)
+ if(memcmp(&buffer[i], "der.mdat\" anim=\"", 16)==0)
return 0;
if(file_recovery->file_stat!=NULL &&
buffer[8]=='a' && isprint(buffer[0]) && isprint(buffer[1]) && isprint(buffer[2]) && isprint(buffer[3]))
@@ -299,88 +439,180 @@ static int header_check_mov_aux(const unsigned char *buffer, const unsigned int
reset_file_recovery(file_recovery_new);
file_recovery_new->extension=file_hint_mov.extension;
file_recovery_new->file_rename=&file_rename_mov;
- if(file_recovery->blocksize < 16)
+ if(file_recovery_new->blocksize < 16)
+ {
+ file_recovery_new->min_filesize=calculated_file_size;
return 1;
+ }
file_recovery_new->data_check=&data_check_mov;
file_recovery_new->file_check=&file_check_size;
- file_recovery_new->calculated_file_size=i+atom_size;
+ file_recovery_new->calculated_file_size=calculated_file_size;
return 1;
}
+ if(atom_size > buffer_size)
+ return 0;
i+=atom_size;
}
return 0;
}
-static data_check_t data_check_mov(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
+/*@
+ @ requires buffer_size >= 16;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ requires \valid_read(file_recovery);
+ @ requires \valid(file_recovery_new);
+ @ requires file_recovery_new->blocksize > 0;
+ @ requires separation: \separated(file_recovery, file_recovery_new);
+ @ ensures \result == 0 || \result == 1;
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_mov.extension ||
+ file_recovery_new->extension == extension_3g2 ||
+ file_recovery_new->extension == extension_3gp ||
+ file_recovery_new->extension == extension_cr3 ||
+ file_recovery_new->extension == extension_heic ||
+ file_recovery_new->extension == extension_jp2 ||
+ file_recovery_new->extension == extension_m4p ||
+ file_recovery_new->extension == extension_mp4);
+ @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == &file_rename_mov || file_recovery_new->file_rename == \null);
+ @ ensures (\result == 1 && file_recovery_new->extension == file_hint_mov.extension) ==> (file_recovery_new->file_rename == file_rename_mov);
+ @ ensures (\result == 1 && file_recovery_new->extension != file_hint_mov.extension) ==> (file_recovery_new->file_rename == \null);
+ @ ensures (\result == 1 && (file_recovery_new->extension == extension_jp2 || file_recovery_new->blocksize < 16)) ==> (file_recovery_new->data_check == \null && file_recovery_new->file_check == \null && file_recovery_new->file_rename == \null && file_recovery_new->min_filesize > 0);
+ @ ensures (\result == 1 && file_recovery_new->extension != extension_jp2 && file_recovery_new->blocksize >= 16) ==> (file_recovery_new->calculated_file_size > 0 && file_recovery_new->file_check == &file_check_size && file_recovery_new->data_check == &data_check_mov);
+ @*/
+static int header_check_mov(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)
{
- while(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size &&
- file_recovery->calculated_file_size + 8 <= file_recovery->file_size + buffer_size/2)
- {
- const unsigned int i=file_recovery->calculated_file_size - file_recovery->file_size + buffer_size/2;
- const struct atom_struct *atom=(const struct atom_struct*)&buffer[i];
- uint64_t atom_size=be32(atom->size);
- if(atom_size==1)
- {
- const struct atom64_struct *atom64=(const struct atom64_struct*)&buffer[i];
- if(file_recovery->calculated_file_size + 16 > file_recovery->file_size + buffer_size/2)
- return DC_CONTINUE;
- atom_size=be64(atom64->size);
- if(atom_size<16)
- return DC_STOP;
- }
- else if(atom_size<8)
- return DC_STOP;
-#ifdef DEBUG_MOV
- log_trace("file_mov.c: %s atom %c%c%c%c (0x%02x%02x%02x%02x) size %llu, calculated_file_size %llu\n",
- file_recovery->filename,
- buffer[i+4],buffer[i+5],buffer[i+6],buffer[i+7],
- buffer[i+4],buffer[i+5],buffer[i+6],buffer[i+7],
- (long long unsigned)atom_size,
- (long long unsigned)file_recovery->calculated_file_size);
+ if(file_recovery->file_stat!=NULL &&
+ file_recovery->file_stat->file_hint==&file_hint_mov &&
+ (file_recovery->calculated_file_size == file_recovery->file_size ||
+ file_recovery_new->blocksize < 16))
+ { /* PhotoRec is already trying to recover this mov file */
+ header_ignored(file_recovery_new);
+ return 0;
+ }
+ return header_check_mov_aux(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+}
+
+/*@
+ @ requires \valid(file_stat);
+ @*/
+static void register_header_check_mov_mdat(file_stat_t *file_stat)
+{
+ register_header_check(4, (const unsigned char*)"mdat",4, &header_check_mov_aux, file_stat);
+}
+
+/*@
+ @ requires \valid(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);
+ 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);
+ register_header_check(4, (const unsigned char*)"ftyp",4, &header_check_mov_aux, file_stat);
+ register_header_check(4, (const unsigned char*)"jp2h",4, &header_check_mov, file_stat);
+ register_header_check(4, (const unsigned char*)"mdat",4, &header_check_mov, file_stat);
+ register_header_check(4, (const unsigned char*)"mdia",4, &header_check_mov, file_stat);
+ register_header_check(4, (const unsigned char*)"moov",4, &header_check_mov, file_stat);
+ register_header_check(4, (const unsigned char*)"PICT",4, &header_check_mov, file_stat);
+ register_header_check(4, (const unsigned char*)"pnot",4, &header_check_mov, file_stat);
+ register_header_check(4, (const unsigned char*)"skip",4, &header_check_mov, file_stat);
+ register_header_check(4, (const unsigned char*)"stbl",4, &header_check_mov, file_stat);
+ register_header_check(4, (const unsigned char*)"trak",4, &header_check_mov, file_stat);
+ register_header_check(4, (const unsigned char*)"wide",4, &header_check_mov, file_stat);
+ register_header_check(4, (const unsigned char*)"jP ",4, &header_check_mov, file_stat);
+}
+
+#if defined(MAIN_mov)
+#define BLOCKSIZE 65536u
+int main()
+{
+ const char fn[] = "recup_dir.1/f0000000.mov";
+ unsigned char buffer[BLOCKSIZE];
+ file_recovery_t file_recovery_new;
+ file_recovery_t file_recovery;
+ file_stat_t file_stats;
+
+ /*@ assert \valid(buffer + (0 .. (BLOCKSIZE - 1))); */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
#endif
- if(buffer[i+4]=='m' && buffer[i+5]=='d' && buffer[i+6]=='a' && buffer[i+7]=='t')
+
+ reset_file_recovery(&file_recovery);
+ file_recovery.blocksize=BLOCKSIZE;
+ file_recovery_new.blocksize=BLOCKSIZE;
+ file_recovery_new.data_check=NULL;
+ file_recovery_new.file_stat=NULL;
+ file_recovery_new.file_check=NULL;
+ file_recovery_new.file_rename=NULL;
+ file_recovery_new.calculated_file_size=0;
+ file_recovery_new.file_size=0;
+ file_recovery_new.offset_ok=0;
+ file_recovery_new.checkpoint_status=0;
+ file_recovery_new.location.start=0;
+ file_recovery_new.offset_error=0;
+
+ file_stats.file_hint=&file_hint_mov;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+ register_header_check_mov(&file_stats);
+ /*@ assert file_recovery_new.blocksize >= 16; */
+ if(header_check_mov(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ assert file_recovery_new.blocksize >= 16; */
+ /*@ assert valid_read_string(file_recovery_new.extension); */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.offset_ok == 0; */
+ /*@ assert valid_read_string((char *)&fn); */
+ memcpy(file_recovery_new.filename, fn, sizeof(fn));
+ /*@ assert valid_read_string((char *)&file_recovery_new.filename); */
+ /*@ assert file_recovery_new.offset_ok == 0; */
+ file_recovery_new.file_stat=&file_stats;
+ if(file_recovery_new.data_check != NULL)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_mov; */
+ /*@ assert file_recovery_new.file_check == file_check_size; */
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.file_size == 0; */;
+ res_data_check=data_check_mov(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
{
- file_recovery->calculated_file_size+=atom_size;
-#if 0
- if(i+8 == buffer_size)
- {
- return -((atom_size + buffer_size/2 - 1)/ (buffer_size/2));
- }
+ /*@ assert file_recovery_new.calculated_file_size > file_recovery_new.file_size - 16; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
#endif
+ data_check_mov(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
}
- else if( (buffer[i+4]=='c' && buffer[i+5]=='m' && buffer[i+6]=='o' && buffer[i+7]=='v') ||
- (buffer[i+4]=='c' && buffer[i+5]=='m' && buffer[i+6]=='v' && buffer[i+7]=='d') ||
- (buffer[i+4]=='d' && buffer[i+5]=='c' && buffer[i+6]=='o' && buffer[i+7]=='m') ||
- (buffer[i+4]=='f' && buffer[i+5]=='r' && buffer[i+6]=='e' && buffer[i+7]=='a') ||
- (buffer[i+4]=='f' && buffer[i+5]=='r' && buffer[i+6]=='e' && buffer[i+7]=='e') ||
- (buffer[i+4]=='f' && buffer[i+5]=='t' && buffer[i+6]=='y' && buffer[i+7]=='p') ||
- (buffer[i+4]=='j' && buffer[i+5]=='p' && buffer[i+6]=='2' && buffer[i+7]=='h') ||
- (buffer[i+4]=='m' && buffer[i+5]=='d' && buffer[i+6]=='i' && buffer[i+7]=='a') ||
- (buffer[i+4]=='m' && buffer[i+5]=='e' && buffer[i+6]=='t' && buffer[i+7]=='a') ||
- (buffer[i+4]=='m' && buffer[i+5]=='o' && buffer[i+6]=='o' && buffer[i+7]=='v') ||
- (buffer[i+4]=='P' && buffer[i+5]=='I' && buffer[i+6]=='C' && buffer[i+7]=='T') ||
- (buffer[i+4]=='p' && buffer[i+5]=='n' && buffer[i+6]=='o' && buffer[i+7]=='t') ||
- (buffer[i+4]=='s' && buffer[i+5]=='k' && buffer[i+6]=='i' && buffer[i+7]=='p') ||
- (buffer[i+4]=='s' && buffer[i+5]=='t' && buffer[i+6]=='b' && buffer[i+7]=='l') ||
- (buffer[i+4]=='t' && buffer[i+5]=='h' && buffer[i+6]=='u' && buffer[i+7]=='m') ||
- (buffer[i+4]=='t' && buffer[i+5]=='r' && buffer[i+6]=='a' && buffer[i+7]=='k') ||
- (buffer[i+4]=='u' && buffer[i+5]=='u' && buffer[i+6]=='i' && buffer[i+7]=='d') ||
- (buffer[i+4]=='w' && buffer[i+5]=='i' && buffer[i+6]=='d' && buffer[i+7]=='e') )
- {
- file_recovery->calculated_file_size+=atom_size;
- }
- else
+ }
+ /*@ assert file_recovery_new.offset_ok == 0; */
+ {
+ file_recovery_t file_recovery_new2;
+ /* Test when another file of the same is detected in the next block */
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+ header_check_mov(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert file_recovery_new.offset_ok == 0; */
+ if(file_recovery_new.file_check != NULL)
+ {
+ /*@ assert file_recovery_new.file_check == file_check_size; */
+ file_recovery_new.handle=fopen(fn, "rb");
+ if(file_recovery_new.handle!=NULL)
{
- 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],
- (long long unsigned)file_recovery->calculated_file_size);
- return DC_STOP;
+ file_check_size(&file_recovery_new);
+ fclose(file_recovery_new.handle);
}
}
-#ifdef DEBUG_MOV
- log_trace("file_mov.c: new calculated_file_size %llu\n",
- (long long unsigned)file_recovery->calculated_file_size);
-#endif
- return DC_CONTINUE;
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_rename_mov(&file_recovery_new);
+ return 0;
}
+#endif