diff options
| -rw-r--r-- | src/fidentify.c | 32 | ||||
| -rw-r--r-- | src/file_bmp.c | 4 | ||||
| -rw-r--r-- | src/file_list.c | 4 | ||||
| -rw-r--r-- | src/filegen.c | 5 | ||||
| -rw-r--r-- | src/list.h | 21 | ||||
| -rw-r--r-- | src/misc.c | 4 |
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; @@ -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); */ } /** @@ -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) |