luisgulo/testdisk
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

frama-c: add annotations for fidentify, checks reduced to file_bmp.c and

Browse source 
lot of code has been commented.
This commit is contained in:
Christophe Grenier 2020-01-26 20:52:47 +01:00
parent cf84e644b5
commit 5cb2dccf0d
6 changed files with 62 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/fidentify.c
View file

@ -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 ||
@ -306,6 +325,9 @@ int main(int argc, char **argv)
#ifndef __AFL_COMPILER
if(scan_dir)
file_identify_dir(".", options);
#endif
#else
file_identify("demo", options);
#endif
free_header_check();
free(file_stats);

4
src/file_bmp.c
View file

@ -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];

4
src/file_list.c
View file

@ -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 }
};

5
src/filegen.c
View file

@ -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;

21
src/list.h
View file

@ -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); */
}
/**

4
src/misc.c
View file

@ -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)