From 5cb2dccf0ddff068c76928d79428ffca4d859f8a Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Sun, 26 Jan 2020 20:52:47 +0100 Subject: [PATCH] frama-c: add annotations for fidentify, checks reduced to file_bmp.c and lot of code has been commented. --- src/fidentify.c | 32 +++++++++++++++++++++++++++----- src/file_bmp.c | 4 +++- src/file_list.c | 4 ++++ src/filegen.c | 5 +++++ src/list.h | 21 +++++++++++++++++++++ src/misc.c | 4 ++-- 6 files changed, 62 insertions(+), 8 deletions(-) diff --git a/src/fidentify.c b/src/fidentify.c index be44e6be..149487f2 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\nhttps://www.cgsecurity.org\n", VERSION, TESTDISKDATE); #endif +#ifndef MAIN_fidentify for(i=1; ienable=1; } file_stats=init_file_stats(list_file_enable); +#ifndef MAIN_fidentify for(i=1; imin_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 5e8867ee..0c6b1835 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 e76010c1..70b69136 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 265e7fe3..c4fbe67c 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 8ac00d66..fb89ce81 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)