summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/fidentify.c32
-rw-r--r--src/file_bmp.c4
-rw-r--r--src/file_list.c4
-rw-r--r--src/filegen.c5
-rw-r--r--src/list.h21
-rw-r--r--src/misc.c4
6 files changed, 62 insertions, 8 deletions
diff --git a/src/fidentify.c b/src/fidentify.c
index be44e6b..149487f 100644
--- a/src/fidentify.c
+++ b/src/fidentify.c
@@ -60,6 +60,9 @@ extern file_check_list_t file_check_list;
#define OPT_CHECK 1
#define OPT_TIME 2
+/*@
+ @ requires valid_read_string(filename);
+ @*/
static int file_identify(const char *filename, const unsigned int options)
{
const unsigned int blocksize=65536;
@@ -96,6 +99,7 @@ static int file_identify(const char *filename, const unsigned int options)
td_list_for_each(tmp, &pos->file_checks[buffer[pos->offset]].list)
{
const file_check_t *file_check=td_list_entry_const(tmp, const file_check_t, list);
+ /*@ assert &file_check->header_check != \null; */
if((file_check->length==0 || memcmp(buffer + file_check->offset, file_check->value, file_check->length)==0) &&
file_check->header_check(buffer, blocksize, 0, &file_recovery, &file_recovery_new)!=0)
{
@@ -112,13 +116,15 @@ static int file_identify(const char *filename, const unsigned int options)
((options&OPT_CHECK)!=0 || ((options&OPT_TIME)!=0 && file_recovery_new.time==0))
)
{
+ off_t file_size;
file_recovery_new.handle=file;
my_fseek(file_recovery_new.handle, 0, SEEK_END);
-#ifdef HAVE_FTELLO
- file_recovery_new.file_size=ftello(file_recovery_new.handle);
+#if defined(HAVE_FTELLO) && !defined(__FRAMAC__)
+ file_size=ftello(file_recovery_new.handle);
#else
- file_recovery_new.file_size=ftell(file_recovery_new.handle);
+ file_size=ftell(file_recovery_new.handle);
#endif
+ file_recovery_new.file_size=(file_size==-1?0:file_size);
file_recovery_new.calculated_file_size=file_recovery_new.file_size;
(file_recovery_new.file_check)(&file_recovery_new);
if(file_recovery_new.file_size < file_recovery_new.min_filesize)
@@ -148,7 +154,7 @@ static int file_identify(const char *filename, const unsigned int options)
return 0;
}
-#ifndef __AFL_COMPILER
+#if !defined(__AFL_COMPILER) && !defined(MAIN_fidentify)
static void file_identify_dir(const char *current_dir, const unsigned int options)
{
DIR *dir;
@@ -201,20 +207,27 @@ static void display_version(void)
#ifdef RECORD_COMPILATION_DATE
printf("Compilation date: %s\n", get_compilation_date());
#endif
+#ifndef MAIN_fidentify
printf("libjpeg: %s, zlib: %s\n", td_jpeg_version(), td_zlib_version());
printf("OS: %s\n" , get_os());
+#endif
}
int main(int argc, char **argv)
{
int i;
+#ifdef MAIN_fidentify
+ unsigned int options=OPT_CHECK|OPT_TIME;
+#else
unsigned int options=0;
+#endif
FILE *log_handle=NULL;
int log_errno=0;
int enable_all_formats=1;
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
for(i=1; i<argc; i++)
{
if( strcmp(argv[i], "/check")==0 || strcmp(argv[i], "-check")==0 || strcmp(argv[i], "--check")==0)
@@ -239,24 +252,28 @@ int main(int argc, char **argv)
return 0;
}
}
+#endif
#ifndef __AFL_COMPILER
log_handle=log_open("fidentify.log", TD_LOG_CREATE, &log_errno);
if(log_handle!=NULL)
{
time_t my_time;
-#ifdef HAVE_DUP2
+#if defined(HAVE_DUP2) && !defined(__FRAMAC__)
dup2(fileno(log_handle),2);
#endif
my_time=time(NULL);
log_info("\n\n%s",ctime(&my_time));
log_info("Command line: fidentify");
+#ifndef MAIN_fidentify
for(i=1;i<argc;i++)
log_info(" %s", argv[i]);
+#endif
log_info("\n\n");
log_flush();
}
log_info("fidentify %s, Data Recovery Utility, %s\nChristophe GRENIER <grenier@cgsecurity.org>\nhttps://www.cgsecurity.org\n", VERSION, TESTDISKDATE);
#endif
+#ifndef MAIN_fidentify
for(i=1; i<argc; i++)
{
file_enable_t *file_enable;
@@ -269,6 +286,7 @@ int main(int argc, char **argv)
enable_all_formats=0;
}
}
+#endif
if(enable_all_formats)
{
/* Enable all file formats */
@@ -277,6 +295,7 @@ int main(int argc, char **argv)
file_enable->enable=1;
}
file_stats=init_file_stats(list_file_enable);
+#ifndef MAIN_fidentify
for(i=1; i<argc; i++)
{
if(strcmp(argv[i], "/check")==0 || strcmp(argv[i], "-check")==0 || strcmp(argv[i], "--check")==0 ||
@@ -307,6 +326,9 @@ int main(int argc, char **argv)
if(scan_dir)
file_identify_dir(".", options);
#endif
+#else
+ file_identify("demo", options);
+#endif
free_header_check();
free(file_stats);
log_close();
diff --git a/src/file_bmp.c b/src/file_bmp.c
index 090f538..afef52b 100644
--- a/src/file_bmp.c
+++ b/src/file_bmp.c
@@ -130,6 +130,8 @@ static int header_check_bmp(const unsigned char *buffer, const unsigned int buff
/*@ assert file_recovery_new->min_filesize == 65; */
/*@ assert file_recovery_new->data_check == &data_check_size; */
/*@ assert file_recovery_new->file_check == &file_check_size; */
+ /*@ assert valid_read_string(file_recovery_new->extension); */
+ /*@ assert \initialized(&file_recovery_new->time); */
return 1;
}
return 0;
@@ -145,7 +147,7 @@ static void register_header_check_bmp(file_stat_t *file_stat)
#if defined(MAIN_bmp)
#define BLOCKSIZE 65536u
-int main()
+int main(void)
{
const char fn[] = "recup_dir.1/f0000000.bmp";
unsigned char buffer[BLOCKSIZE];
diff --git a/src/file_list.c b/src/file_list.c
index 5e8867e..0c6b183 100644
--- a/src/file_list.c
+++ b/src/file_list.c
@@ -366,6 +366,7 @@ extern const file_hint_t file_hint_zpr;
file_enable_t list_file_enable[]=
{
+#ifndef MAIN_fidentify
{ .enable=0, .file_hint=&file_hint_sig },
{ .enable=0, .file_hint=&file_hint_1cd },
{ .enable=0, .file_hint=&file_hint_3dm },
@@ -405,7 +406,9 @@ file_enable_t list_file_enable[]=
{ .enable=0, .file_hint=&file_hint_binvox },
{ .enable=0, .file_hint=&file_hint_bkf },
{ .enable=0, .file_hint=&file_hint_blend },
+#endif
{ .enable=0, .file_hint=&file_hint_bmp },
+#ifndef MAIN_fidentify
{ .enable=0, .file_hint=&file_hint_bpg },
{ .enable=0, .file_hint=&file_hint_bvr },
{ .enable=0, .file_hint=&file_hint_bz2 },
@@ -702,6 +705,7 @@ file_enable_t list_file_enable[]=
{ .enable=0, .file_hint=&file_hint_zcode },
{ .enable=0, .file_hint=&file_hint_zip },
{ .enable=0, .file_hint=&file_hint_zpr },
+#endif
{ .enable=0, .file_hint=NULL }
};
diff --git a/src/filegen.c b/src/filegen.c
index e76010c..70b6913 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -182,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;
diff --git a/src/list.h b/src/list.h
index 265e7fe..c4fbe67 100644
--- a/src/list.h
+++ b/src/list.h
@@ -124,10 +124,19 @@ static inline void td_list_add_tail(struct td_list_head *newe, struct td_list_he
* This is only for internal list manipulation where we know
* the prev/next entries already!
*/
+/*@
+ @ requires \valid(prev);
+ @ requires \valid(next);
+ @ ensures next->prev == prev;
+ @ ensures prev->next == next;
+ @ assigns next->prev,prev->next;
+ @*/
static inline void __td_list_del(struct td_list_head * prev, struct td_list_head * next)
{
next->prev = prev;
prev->next = next;
+ /*@ assert next->prev == prev; */
+ /*@ assert prev->next == next; */
}
/**
@@ -136,11 +145,23 @@ static inline void __td_list_del(struct td_list_head * prev, struct td_list_head
* Note: td_list_empty on entry does not return true after this, the entry is
* in an undefined state.
*/
+/*@
+ @ requires \valid(entry);
+ @ requires \valid(entry->prev);
+ @ requires \valid(entry->next);
+ @ ensures \old(entry->prev)->next == \old(entry->next);
+ @ ensures \old(entry->next)->prev == \old(entry->prev);
+ @ assigns \old(entry->prev)->next, \old(entry->next)->prev, entry->next, entry->prev;
+ @*/
static inline void td_list_del(struct td_list_head *entry)
{
__td_list_del(entry->prev, entry->next);
+ /*@ assert entry->prev->next == entry->next; */
+ /*@ assert entry->next->prev == entry->prev; */
entry->next = (struct td_list_head*)LIST_POISON1;
entry->prev = (struct td_list_head*)LIST_POISON2;
+ /*@ assert \at(entry->prev,Pre)->next == \at(entry->next,Pre); */
+ /*@ assert \at(entry->next,Pre)->prev == \at(entry->prev,Pre); */
}
/**
diff --git a/src/misc.c b/src/misc.c
index 8ac00d6..fb89ce8 100644
--- a/src/misc.c
+++ b/src/misc.c
@@ -172,7 +172,7 @@ https://msdn.microsoft.com/en-us/library/windows/desktop/ms724834%28v=vs.85%29.a
}
#elif defined(DJGPP)
return "DOS";
-#elif defined(HAVE_SYS_UTSNAME_H) && defined(HAVE_UNAME)
+#elif defined(HAVE_SYS_UTSNAME_H) && defined(HAVE_UNAME) && !defined(__FRAMAC__)
{
struct utsname Ver;
if(uname(&Ver)==0)
@@ -281,7 +281,7 @@ const char *get_compilation_date(void)
{
static char buffer[100] = {0x00};
#ifdef __DATE__
-#ifdef HAVE_STRPTIME
+#if defined(HAVE_STRPTIME) && !defined(__FRAMAC__)
struct tm tm;
memset(&tm,0,sizeof(tm));
if(strptime(__DATE__, "%b %d %Y", &tm)!=NULL)