summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-09-21 10:08:14 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2019-09-21 10:08:14 +0200
commit5e48555814c93598b109eccf8cdf2b2b69621c88 (patch)
tree87dc4f2d36316071ea2761089e96da9941fde1a8
parent153269e044bef851b706f2306a936331c3a5e94c (diff)
PhotoRec: add frama-c tests for mp3 and id3
-rw-r--r--Makefile.am32
-rw-r--r--src/file_mp3.c437
2 files changed, 413 insertions, 56 deletions
diff --git a/Makefile.am b/Makefile.am
index a41d194..225db54 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -1,3 +1,24 @@
+.PRECIOUS: session_%.framac
+FRAMA_C_FLAGS=-machdep x86_64 \
+ -warn-left-shift-negative \
+ -warn-right-shift-negative \
+ -warn-signed-downcast \
+ -warn-signed-overflow \
+ -warn-unsigned-downcast \
+ -warn-unsigned-overflow \
+ -rte \
+ -eva \
+ -eva-slevel 1 \
+ -eva-warn-undefined-pointer-comparison none \
+ -eva-ignore-recursive-calls \
+ -then \
+ -wp \
+ -wp-dynamic \
+ -wp-steps 100000 -wp-depth 100000 \
+ -wp-split -wp-literals \
+ -wp-timeout 20 -pp-annot \
+ -kernel-msg-key pp
+
SUBDIRS = icons man src
docdir ?= $(datadir)/doc/$(PACKAGE)
@@ -59,4 +80,15 @@ extras:
extrasstatic:
$(MAKE) LDFLAGS="$(LDFLAGS) -static" LIBS="$(PTHREAD_LIBS) $(LIBS)" CFLAGS="$(PTHREAD_CFLAGS) $(CFLAGS)" CXXFLAGS="$(PTHREAD_CFLAGS) $(CXXFLAGS)" extras
+session_id3.framac: src/file_mp3.c src/common.c src/filegen.c src/log.c
+ gcc -W -Wall -DMAIN_id3 -DHAVE_CONFIG_H -O -o demo -I. $^
+ frama-c $^ -cpp-extra-args="-DMAIN_id3 -DHAVE_CONFIG_H -D__x86_64__" $(FRAMA_C_FLAGS) -save $@
+
+session_%.framac: src/file_%.c src/common.c src/filegen.c src/log.c
+ gcc -W -Wall -DMAIN_$* -DHAVE_CONFIG_H -O -o demo -I. $^
+ frama-c $^ -cpp-extra-args="-DMAIN_$* -DHAVE_CONFIG_H -D__x86_64__" $(FRAMA_C_FLAGS) -save $@
+
+frama-c-%: session_%.framac
+ frama-c-gui -load $^
+
DISTCLEANFILES = *~ core
diff --git a/src/file_mp3.c b/src/file_mp3.c
index 9cde947..93f3aa3 100644
--- a/src/file_mp3.c
+++ b/src/file_mp3.c
@@ -31,9 +31,14 @@
#include "common.h"
#include "filegen.h"
#include "log.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
+#if !defined(MAIN_mp3) && !defined(MAIN_id3)
extern const file_hint_t file_hint_mkv;
extern const file_hint_t file_hint_tiff;
+#endif
static void register_header_check_mp3(file_stat_t *file_stat);
static data_check_t data_check_id3(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
@@ -112,6 +117,21 @@ static const unsigned int bit_rate_table[4][4][16]=
},
};
+#ifndef MAIN_mp3
+/*@
+ @ requires buffer_size >= 10;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ requires \valid_read(file_recovery);
+ @ requires \valid(file_recovery_new);
+ @ requires file_recovery_new->blocksize > 0;
+ @ ensures \result == 0 || \result == 1;
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_mp3.extension);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size > 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 287);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_id3);
+ @*/
static int header_check_id3(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)
{
if(buffer[0]=='I' && buffer[1]=='D' && buffer[2]=='3' && (buffer[3]==2 || buffer[3]==3 || buffer[3]==4) && buffer[4]==0)
@@ -133,6 +153,7 @@ static int header_check_id3(const unsigned char *buffer, const unsigned int buff
*/
reset_file_recovery(file_recovery_new);
file_recovery_new->calculated_file_size=potential_frame_offset;
+ /*@ assert file_recovery_new->calculated_file_size > 0; */
file_recovery_new->min_filesize=287;
file_recovery_new->data_check=&data_check_id3;
file_recovery_new->extension=file_hint_mp3.extension;
@@ -141,7 +162,25 @@ static int header_check_id3(const unsigned char *buffer, const unsigned int buff
}
return 0;
}
+#endif
+#ifndef MAIN_id3
+/*@
+ @ requires buffer_size >= 6;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ requires \valid_read(file_recovery);
+ @ requires \valid(file_recovery_new);
+ @ requires file_recovery_new->blocksize > 0;
+ @ ensures \result == 0 || \result == 1;
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_mp3.extension);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size > 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 287);
+ @ ensures (\result == 1 && file_recovery_new->blocksize >= 16) ==> (file_recovery_new->file_check == &file_check_size);
+ @ ensures (\result == 1 && file_recovery_new->blocksize >= 16) ==> (file_recovery_new->data_check == &data_check_mp3);
+ @ ensures (\result == 1 && file_recovery_new->blocksize < 16) ==> (file_recovery_new->file_check == \null);
+ @ ensures (\result == 1 && file_recovery_new->blocksize < 16) ==> (file_recovery_new->data_check == \null);
+ @*/
static int header_check_mp3(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)
{
unsigned int potential_frame_offset=0;
@@ -165,12 +204,16 @@ static int header_check_mp3(const unsigned char *buffer, const unsigned int buff
return 0;
if(file_recovery->file_stat!=NULL)
{
- if(file_recovery->file_stat->file_hint==&file_hint_mp3 ||
- file_recovery->file_stat->file_hint==&file_hint_mkv)
+ if(file_recovery->file_stat->file_hint==&file_hint_mp3
+#if !defined(MAIN_mp3) && !defined(MAIN_id3)
+ || file_recovery->file_stat->file_hint==&file_hint_mkv
+#endif
+ )
{
header_ignored(file_recovery_new);
return 0;
}
+#if !defined(MAIN_mp3) && !defined(MAIN_id3)
/* RGV values from TIFF may be similar to the beginning of an mp3 */
if(file_recovery->file_stat->file_hint==&file_hint_tiff &&
buffer[0]==buffer[3] && buffer[1]==buffer[4] && buffer[2]==buffer[5])
@@ -178,7 +221,12 @@ static int header_check_mp3(const unsigned char *buffer, const unsigned int buff
if(header_ignored_adv(file_recovery, file_recovery_new)==0)
return 0;
}
+#endif
}
+ /*@ assert nbr == 0; */
+ /*@
+ @ loop invariant 0 <= nbr <= potential_frame_offset <= 2048 + 8065;
+ @*/
while(potential_frame_offset+1 < buffer_size &&
potential_frame_offset+1 < 2048)
{
@@ -195,6 +243,8 @@ static int header_check_mp3(const unsigned char *buffer, const unsigned int buff
unsigned int frameLengthInBytes=0;
if(sample_rate==0 || bit_rate==0 || mpeg_layer==MPEG_L1)
return 0;
+ /*@ assert 8 <= bit_rate <= 448; */
+ /*@ assert 8000 <= sample_rate <= 48000; */
if(mpeg_layer==MPEG_L3)
{
if(mpeg_version==MPEG_V1)
@@ -212,17 +262,24 @@ static int header_check_mp3(const unsigned char *buffer, const unsigned int buff
#endif
if(frameLengthInBytes==0)
return 0;
+ /*@ assert 0 < frameLengthInBytes <= 8065; */
potential_frame_offset+=frameLengthInBytes;
+ /*@ assert potential_frame_offset > 0; */
nbr++;
}
}
if(nbr>1)
{
+ /*@ assert nbr > 1; */
+ /*@ assert potential_frame_offset > 0; */
#ifdef DEBUG_MP3
log_info("header_check_mp3 mp3 found\n");
#endif
reset_file_recovery(file_recovery_new);
+ /*@ assert file_recovery_new->file_check == \null; */
+ /*@ assert file_recovery_new->data_check == \null; */
file_recovery_new->calculated_file_size=potential_frame_offset;
+ /*@ assert file_recovery_new->calculated_file_size > 0; */
file_recovery_new->min_filesize=287;
file_recovery_new->extension=file_hint_mp3.extension;
if(file_recovery_new->blocksize >= 16)
@@ -234,13 +291,25 @@ static int header_check_mp3(const unsigned char *buffer, const unsigned int buff
}
return 0;
}
+#endif
+#ifndef MAIN_mp3
+/*@
+ @ requires buffer_size >= 32;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ requires \valid(file_recovery);
+ @ requires file_recovery->data_check==&data_check_id3;
+ @ ensures \result == DC_CONTINUE || \result == DC_STOP;
+ @ ensures \result == DC_CONTINUE && file_recovery->data_check==&data_check_id3 ==> (file_recovery->calculated_file_size >= file_recovery->file_size + buffer_size/2 - 1);
+ @ ensures \result == DC_CONTINUE ==> (file_recovery->calculated_file_size >= file_recovery->file_size + buffer_size/2 - 16);
+ @*/
static data_check_t data_check_id3(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{
while(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size &&
file_recovery->calculated_file_size + 1 < file_recovery->file_size + buffer_size/2)
{
- const unsigned int i=file_recovery->calculated_file_size - 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 - 1 ; */
if(buffer[i]==0)
{ /* Padding is present */
file_recovery->calculated_file_size++;
@@ -249,12 +318,29 @@ static data_check_t data_check_id3(const unsigned char *buffer, const unsigned i
{ /* no more padding or no padding */
file_recovery->data_check=&data_check_mp3;
file_recovery->file_check=&file_check_size;
- return data_check_mp3(buffer, buffer_size, file_recovery);
+ if(data_check_mp3(buffer, buffer_size, file_recovery)!=DC_CONTINUE)
+ return DC_STOP;
+ /*@ assert file_recovery->data_check==&data_check_mp3; */
+ /*@ assert file_recovery->calculated_file_size >= file_recovery->file_size + buffer_size/2 - 16; */
+ return DC_CONTINUE;
}
}
+ /*@ 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 - 1; */
+ /*@ assert file_recovery->calculated_file_size >= file_recovery->file_size + buffer_size/2 - 1; */
return DC_CONTINUE;
}
+#endif
+/*@
+ @ requires buffer_size >= 32;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ requires \valid(file_recovery);
+ @ requires file_recovery->data_check==&data_check_mp3;
+ @ 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);
+ @*/
+ /* TODO: assigns file_recovery->calculated_file_size; */
static data_check_t data_check_mp3(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{
#ifdef DEBUG_MP3
@@ -265,7 +351,8 @@ static data_check_t data_check_mp3(const unsigned char *buffer, const unsigned i
while(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size &&
file_recovery->calculated_file_size + 16 < file_recovery->file_size + buffer_size/2)
{
- const unsigned int i=file_recovery->calculated_file_size - 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 - 16 ; */
#ifdef DEBUG_MP3
log_info("data_check_mp3 start i=0x%x buffer_size=0x%x calculated_file_size=%lu file_size=%lu\n",
i, buffer_size,
@@ -290,6 +377,8 @@ static data_check_t data_check_mp3(const unsigned char *buffer, const unsigned i
*/
if(sample_rate==0 || bit_rate==0 || mpeg_layer==MPEG_L1)
return DC_STOP;
+ /*@ assert 8 <= bit_rate <= 448; */
+ /*@ assert 8000 <= sample_rate <= 48000; */
if(mpeg_layer==MPEG_L3)
{
if(mpeg_version==MPEG_V1)
@@ -303,7 +392,9 @@ static data_check_t data_check_mp3(const unsigned char *buffer, const unsigned i
frameLengthInBytes = (12000 * bit_rate / sample_rate + padding)*4;
if(frameLengthInBytes<3)
return DC_STOP;
+ /*@ assert 3 < frameLengthInBytes <= 8065; */
file_recovery->calculated_file_size+=frameLengthInBytes;
+ /*@ assert file_recovery->calculated_file_size > 0; */
}
else if(buffer[i]=='L' && buffer[i+1]=='Y' && buffer[i+2]=='R' && buffer[i+3]=='I' && buffer[i+4]=='C' && buffer[i+5]=='S' && buffer[i+6]=='B' && buffer[i+7]=='E' && buffer[i+8]=='G' && buffer[i+9]=='I' && buffer[i+10]=='N')
{
@@ -318,16 +409,20 @@ static data_check_t data_check_mp3(const unsigned char *buffer, const unsigned i
The maximum length of the lyrics is 5100 bytes for Lyrics3 and 4096 bytes for Lyrics3 v2.
*/
unsigned int pos_lyrics=0;
- /* FIXME */
- if(file_recovery->calculated_file_size + 5100 >= file_recovery->file_size + buffer_size/2)
- return DC_CONTINUE;
+ if(i + 5100 > buffer_size)
+ return DC_STOP;
+ /*@ assert i + 5100 <= buffer_size; */
if((pos_lyrics=pos_in_mem(&buffer[i], 4096, (const unsigned char*)"LYRICS200", 9)) != 0)
{
+ /*@ assert pos_lyrics > 0; */
file_recovery->calculated_file_size+=pos_lyrics;
+ /*@ assert file_recovery->calculated_file_size > 0; */
}
else if((pos_lyrics=pos_in_mem(&buffer[i], 5100, (const unsigned char*)"LYRICSEND", 9)) != 0)
{
+ /*@ assert pos_lyrics > 0; */
file_recovery->calculated_file_size+=pos_lyrics;
+ /*@ assert file_recovery->calculated_file_size > 0; */
}
else
{
@@ -339,42 +434,64 @@ static data_check_t data_check_mp3(const unsigned char *buffer, const unsigned i
}
else if(buffer[i]=='A' && buffer[i+1]=='P' && buffer[i+2]=='E' && buffer[i+3]=='T' && buffer[i+4]=='A' && buffer[i+5]=='G' && buffer[i+6]=='E' && buffer[i+7]=='X')
{ /* APE Tagv2 (APE Tagv1 has no header) http://wiki.hydrogenaudio.org/index.php?title=APE_Tags_Header */
- const unsigned int ape_tag_size = (buffer[i+12] + (buffer[i+13]<<8) + (buffer[i+14]<<16) + (buffer[i+15]<<24))+32;
+ const uint64_t ape_tag_size = (buffer[i+12] | (buffer[i+13]<<8) | (buffer[i+14]<<16) | ((uint64_t)buffer[i+15]<<24))+(uint64_t)32;
file_recovery->calculated_file_size+=ape_tag_size;
+ /*@ assert file_recovery->calculated_file_size > 0; */
}
else if(buffer[i]=='T' && buffer[i+1]=='A' && buffer[i+2]=='G')
{ /* http://www.id3.org/ID3v1 TAGv1 size = 128 bytes with header "TAG" */
file_recovery->calculated_file_size+=128;
- }
- else if(file_recovery->calculated_file_size > file_recovery->file_size)
- {
- return DC_CONTINUE;
+ /*@ assert file_recovery->calculated_file_size > 0; */
}
else
{
const unsigned int MMT_size=search_MMT(buffer,i,buffer_size);
if(MMT_size==0)
return DC_STOP;
+ /*@ assert MMT_size > 0; */
/*
log_info("MusicMatch Tag found at offset 0x%x with size 0x%x \n", file_recovery->calculated_file_size, MMT_size);
*/
file_recovery->calculated_file_size+=MMT_size;
+ /*@ assert file_recovery->calculated_file_size > 0; */
}
}
+ /*@ 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 - 16; */
+ /*@ assert file_recovery->calculated_file_size >= file_recovery->file_size + buffer_size/2 - 16; */
return DC_CONTINUE;
}
+/*@
+ @ requires needle_size > 0;
+ @ requires haystack_size > 0;
+ @ requires \valid_read(needle+(0..needle_size-1));
+ @ requires \valid_read(haystack+(0..haystack_size-1));
+ @ ensures \result == 0 || needle_size <= \result <= haystack_size;
+ @ assigns \nothing;
+ @*/
static unsigned int pos_in_mem(const unsigned char *haystack, const unsigned int haystack_size, const unsigned char *needle, const unsigned int needle_size)
{
unsigned int i;
if(haystack_size < needle_size)
return 0;
+ /*@ assert haystack_size >= needle_size; */
+ /*@
+ @ loop assigns i;
+ @ loop invariant 0 <= i <= haystack_size - needle_size + 1;
+ @ loop variant haystack_size - needle_size - i;
+ @*/
for(i=0; i <= haystack_size - needle_size; i++)
if(memcmp(&haystack[i],needle,needle_size)==0)
return (i+needle_size);
return 0;
}
+/*@
+ @ requires buffer_size > 0;
+ @ requires i <= buffer_size;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ assigns \nothing;
+ @*/
static unsigned int search_MMT(const unsigned char *buffer, const unsigned int i, const unsigned int buffer_size)
{
/*
@@ -397,12 +514,12 @@ static unsigned int search_MMT(const unsigned char *buffer, const unsigned int i
*/
const unsigned char mm_header[10]= {'1','8','2','7','3','6','4','5',0x00, 0x00};
const unsigned char mm_pad_version_info[14] = {0x00,0x00,0x00,0x00,'1','8','2','7','3','6','4','5',0x00,0x00};
- const char *mm_footer="Brava Software Inc.";
- const char *mm_footer_tag="TAG";
+ const char mm_footer[]="Brava Software Inc.";
+ const char mm_footer_tag[]="TAG";
unsigned int size=0;
- unsigned int image_size;
if(i+sizeof(mm_header)>buffer_size)
return 0;
+ /*@ assert i + sizeof(mm_header) <= buffer_size; */
if(memcmp(&buffer[i],mm_header,sizeof(mm_header))==0) // Optional Header
{
size=256;
@@ -412,57 +529,83 @@ static unsigned int search_MMT(const unsigned char *buffer, const unsigned int i
else
{
/* Check image extension */
- if( memcmp(&buffer[i+size]," ",4)!=0 &&
- memcmp(&buffer[i+size],"bmp ",4)!=0 &&
- memcmp(&buffer[i+size],"jpg ",4)!=0)
+ if( memcmp(&buffer[i]," ",4)!=0 &&
+ memcmp(&buffer[i],"bmp ",4)!=0 &&
+ memcmp(&buffer[i],"jpg ",4)!=0)
return 0;
/* log_info("search_MMT: image extension present\n"); */
}
-/* dump_log(&buffer[i+size], buffer_size-(i+size)); */
- /* Image binary */
- image_size = buffer[i+size+4]+(buffer[i+size+5]<<8)+(buffer[i+size+6]<<16)+(buffer[i+size+7]<<24);
- size+=8+image_size;
- /* check null padding + version_info */
- if(i+size+sizeof(mm_pad_version_info)>buffer_size)
- { /* FIXME: Is it better to have a partial MusicMatch Tag or none ? */
- /* log_trace("search_MMT: partial MusicMatch Tag 1\n"); */
- return 0;
+ {
+ const unsigned int tmp=i+size;
+ const uint32_t *image_size_ptr;
+ uint32_t image_size;
+ if(tmp+8>buffer_size)
+ return 0;
+ /*@ assert tmp + 8 <= buffer_size; */
+ image_size_ptr = (const uint32_t *)&buffer[tmp+4];
+ image_size = le32(*image_size_ptr);
+ /* Check if the image size */
+ if(image_size > 10 * 1024 * 1024)
+ return 0;
+ /*@ assert image_size <= 10 * 1024 * 1024; */
+ /* Image binary */
+ size+=8+image_size;
}
- if(memcmp(&buffer[i+size], mm_pad_version_info, sizeof(mm_pad_version_info))!=0)
{
- /* log_trace("search_MMT: mm_pad_version_info not present\n"); */
- return 0;
+ const unsigned int tmp=i+size;
+ /* check null padding + version_info */
+ if(tmp+sizeof(mm_pad_version_info)>buffer_size)
+ { /* FIXME: Is it better to have a partial MusicMatch Tag or none ? */
+ /* log_trace("search_MMT: partial MusicMatch Tag 1\n"); */
+ return 0;
+ }
+ /*@ assert tmp + sizeof(mm_pad_version_info) <= buffer_size; */
+ if(memcmp(&buffer[tmp], mm_pad_version_info, sizeof(mm_pad_version_info))!=0)
+ {
+ /* log_trace("search_MMT: mm_pad_version_info not present\n"); */
+ return 0;
+ }
}
size+=4+256; /* padding + version_info */
size+=20; /* data offset */
- /* check footer for various audio meta-data size: 7868, 7936, 8004, 8132 */
- if(i+size+8132+sizeof(*mm_footer)>buffer_size)
- { /* FIXME: Is it better to have a partial MusicMatch Tag or none ? */
- /* log_trace("search_MMT: partial MusicMatch 2\n"); */
- return 0;
+ {
+ const unsigned int tmp=i+size;
+ /* check footer for various audio meta-data size: 7868, 7936, 8004, 8132 */
+ if(tmp+8132+sizeof(mm_footer) > buffer_size)
+ { /* FIXME: Is it better to have a partial MusicMatch Tag or none ? */
+ /* log_trace("search_MMT: partial MusicMatch 2\n"); */
+ return 0;
+ }
+ /*@ assert tmp + 8132 + sizeof(mm_footer) <= buffer_size; */
+ if( memcmp(&buffer[tmp+7868], mm_footer, sizeof(mm_footer)-1)==0 ||
+ memcmp(&buffer[tmp+7868], mm_footer_tag, sizeof(mm_footer_tag) - 1)==0)
+ size+=7868;
+ else if(memcmp(&buffer[tmp+7936], mm_footer, sizeof(mm_footer)-1)==0 ||
+ memcmp(&buffer[tmp+7936], mm_footer_tag, sizeof(mm_footer_tag) - 1)==0)
+ size+=7936;
+ else if(memcmp(&buffer[tmp+8004], mm_footer, sizeof(mm_footer)-1)==0 ||
+ memcmp(&buffer[tmp+8004], mm_footer_tag, sizeof(mm_footer_tag) - 1)==0)
+ size+=8004;
+ else if(memcmp(&buffer[tmp+8132], mm_footer, sizeof(mm_footer)-1)==0 ||
+ memcmp(&buffer[tmp+8132], mm_footer_tag, sizeof(mm_footer_tag)-1)==0)
+ size+=8132;
+ else
+ {
+ /* log_trace("search_MMT: no mm_footer present\n"); */
+ return 0;
+ }
}
- if(memcmp(&buffer[i+size+7868],mm_footer,strlen(mm_footer))==0 ||
- memcmp(&buffer[i+size+7868],mm_footer_tag,strlen(mm_footer_tag))==0)
- size+=7868;
- else if(memcmp(&buffer[i+size+7936],mm_footer,strlen(mm_footer))==0 ||
- memcmp(&buffer[i+size+7936],mm_footer_tag,strlen(mm_footer_tag))==0)
- size+=7936;
- else if(memcmp(&buffer[i+size+8004],mm_footer,strlen(mm_footer))==0 ||
- memcmp(&buffer[i+size+8004],mm_footer_tag,strlen(mm_footer_tag))==0)
- size+=8004;
- else if(memcmp(&buffer[i+size+8132],mm_footer,strlen(mm_footer))==0 ||
- memcmp(&buffer[i+size+8132],mm_footer_tag,strlen(mm_footer_tag))==0)
- size+=8132;
- else
{
- /* log_trace("search_MMT: no mm_footer present\n"); */
- return 0;
+ const unsigned int tmp=i+size;
+ if(tmp + sizeof(mm_footer) > buffer_size)
+ return 0;
+ /*@ assert tmp + sizeof(mm_footer) <= buffer_size; */
+ /* dump_log(&buffer[tmp], 16); */
+ if(memcmp(&buffer[tmp],mm_footer, sizeof(mm_footer)-1)==0)
+ size+=48; /* footer */
+ else
+ size+=0x80; /* TAG footer */
}
- /* dump_log(&buffer[i+size], 16); */
- if(memcmp(&buffer[i+size],mm_footer,strlen(mm_footer))==0)
- size+=48; /* footer */
- else
- size+=0x80; /* TAG footer */
/* log_trace("search_MMT: MMT found size=%u (0x%x)\n", size, size); */
return(size);
}
@@ -475,11 +618,193 @@ static void register_header_check_mp3(file_stat_t *file_stat)
static const unsigned char mpeg2_L3_header2[2]= {0xFF, 0xF3};
static const unsigned char mpeg25_L3_header1[2]={0xFF, 0xE2};
static const unsigned char mpeg25_L3_header2[2]={0xFF, 0xE3};
+#ifndef MAIN_mp3
register_header_check(0, "ID3", 3, &header_check_id3, file_stat);
+#endif
+#ifndef MAIN_id3
register_header_check(0, mpeg1_L3_header1, sizeof(mpeg1_L3_header1), &header_check_mp3, file_stat);
register_header_check(0, mpeg1_L3_header2, sizeof(mpeg1_L3_header2), &header_check_mp3, file_stat);
register_header_check(0, mpeg2_L3_header1, sizeof(mpeg2_L3_header1), &header_check_mp3, file_stat);
register_header_check(0, mpeg2_L3_header2, sizeof(mpeg2_L3_header2), &header_check_mp3, file_stat);
register_header_check(0, mpeg25_L3_header1, sizeof(mpeg25_L3_header1), &header_check_mp3, file_stat);
register_header_check(0, mpeg25_L3_header2, sizeof(mpeg25_L3_header2), &header_check_mp3, file_stat);
+#endif
+}
+
+#ifdef MAIN_id3
+#define BLOCKSIZE 65536u
+int main()
+{
+ 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
+
+ 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.location.start=0;
+
+ file_stats.file_hint=&file_hint_mp3;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+ file_hint_mp3.register_header_check(&file_stats);
+ if(header_check_id3(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new) != 1)
+ return 0;
+ memcpy(file_recovery_new.filename, "demo", 5);
+ /*@ assert file_recovery_new.extension == file_hint_mp3.extension; */
+ /*@ assert file_recovery_new.calculated_file_size > 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.min_filesize == 287; */
+ /*@ assert file_recovery_new.data_check == &data_check_id3; */
+ file_recovery_new.file_stat=&file_stats;
+ if(file_recovery_new.file_stat!=NULL && file_recovery_new.file_stat->file_hint!=NULL &&
+ file_recovery_new.data_check!=NULL)
+ {
+ 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 <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_id3(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ /*@ assert file_recovery_new.data_check == &data_check_id3 || file_recovery_new.data_check == &data_check_mp3; */
+ /*@ assert res_data_check == DC_CONTINUE && file_recovery_new.data_check == &data_check_mp3 ==> (file_recovery_new.calculated_file_size >= file_recovery_new.file_size + BLOCKSIZE - 16); */
+ /*@ assert res_data_check == DC_CONTINUE && file_recovery_new.data_check == &data_check_id3 ==> (file_recovery_new.calculated_file_size >= file_recovery_new.file_size + BLOCKSIZE - 1); */
+ /*@ assert res_data_check == DC_CONTINUE ==> (file_recovery_new.calculated_file_size >= file_recovery_new.file_size + BLOCKSIZE - 16); */
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ 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
+ file_recovery_new.data_check(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ if(file_recovery_new.file_stat!=NULL)
+ {
+ 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_id3(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ if(file_recovery_new.file_check!=NULL)
+ {
+ file_recovery_new.handle=fopen("demo", "rb");
+ if(file_recovery_new.handle!=NULL)
+ {
+ (file_recovery_new.file_check)(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ }
+ if(file_recovery_new.file_rename!=NULL)
+ {
+ /*@ assert valid_read_string((char *)&file_recovery_new.filename); */
+ (file_recovery_new.file_rename)(&file_recovery_new);
+ }
+ return 0;
}
+#elif defined(MAIN_mp3)
+#define BLOCKSIZE 65536u
+int main()
+{
+ 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
+
+ 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.location.start=0;
+
+ file_stats.file_hint=&file_hint_mp3;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+ file_hint_mp3.register_header_check(&file_stats);
+ if(header_check_mp3(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ memcpy(file_recovery_new.filename, "demo", 5);
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.min_filesize == 287; */
+ /*@ assert file_recovery_new.extension == file_hint_mp3.extension; */
+ /*@ assert file_recovery_new.calculated_file_size > 0; */
+ file_recovery_new.file_stat=&file_stats;
+ if(file_recovery_new.file_stat!=NULL && file_recovery_new.file_stat->file_hint!=NULL &&
+ file_recovery_new.data_check!=NULL)
+ {
+ 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.data_check == &data_check_mp3; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_mp3(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ /*@ assert res_data_check == DC_CONTINUE ==> (file_recovery_new.calculated_file_size >= file_recovery_new.file_size + BLOCKSIZE - 16); */
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ 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
+ file_recovery_new.data_check(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ if(file_recovery_new.file_stat!=NULL)
+ {
+ 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_mp3(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ if(file_recovery_new.file_check!=NULL)
+ {
+ file_recovery_new.handle=fopen("demo", "rb");
+ if(file_recovery_new.handle!=NULL)
+ {
+ (file_recovery_new.file_check)(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ }
+ if(file_recovery_new.file_rename!=NULL)
+ {
+ /*@ assert valid_read_string((char *)&file_recovery_new.filename); */
+ (file_recovery_new.file_rename)(&file_recovery_new);
+ }
+ return 0;
+}
+#endif