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

src/fidentify.c: make file_identify() more frama-c friendly

Browse source
This commit is contained in:
Christophe Grenier 2020-06-18 18:59:02 +02:00
parent 04374e9c52
commit fa497bec61
1 changed files with 13 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/fidentify.c
View file

@ -92,9 +92,12 @@ static int file_identify(const char *filename, const unsigned int options)
} }
if(fread(buffer, 1, READ_SIZE, file) >0) if(fread(buffer, 1, READ_SIZE, file) >0)
{ {
struct td_list_head *tmpl; const struct td_list_head *tmpl;
file_recovery_t file_recovery_new; file_recovery_t file_recovery_new;
file_recovery_t file_recovery; file_recovery_t file_recovery;
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)buffer, READ_SIZE);
#endif
reset_file_recovery(&file_recovery); reset_file_recovery(&file_recovery);
reset_file_recovery(&file_recovery_new); reset_file_recovery(&file_recovery_new);
file_recovery.blocksize=blocksize; file_recovery.blocksize=blocksize;
@ -102,13 +105,18 @@ static int file_identify(const char *filename, const unsigned int options)
/*@ assert file_recovery_new.file_stat==NULL; */ /*@ assert file_recovery_new.file_stat==NULL; */
td_list_for_each(tmpl, &file_check_list.list) td_list_for_each(tmpl, &file_check_list.list)
{ {
struct td_list_head *tmp; const struct td_list_head *tmp;
const file_check_list_t *pos=td_list_entry_const(tmpl, const file_check_list_t, list); const file_check_list_t *pos=td_list_entry_const(tmpl, const file_check_list_t, list);
td_list_for_each(tmp, &pos->file_checks[buffer[pos->offset]].list) const struct td_list_head *tmp_list=&pos->file_checks[buffer[pos->offset]].list;
td_list_for_each(tmp, tmp_list)
{ {
/*TODO assert tmp!=tmp_list; */
const file_check_t *file_check=td_list_entry_const(tmp, const file_check_t, list); const file_check_t *file_check=td_list_entry_const(tmp, const file_check_t, list);
/*@ assert &file_check->header_check != \null; */ if(
if((file_check->length==0 || memcmp(buffer + file_check->offset, file_check->value, file_check->length)==0) && #ifdef __FRAMAC__
file_check->header_check!=NULL &&
#endif
(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) file_check->header_check(buffer, blocksize, 0, &file_recovery, &file_recovery_new)!=0)
{ {
file_recovery_new.file_stat=file_check->file_stat; file_recovery_new.file_stat=file_check->file_stat;