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

add a few frama-c annotations

Browse source
This commit is contained in:
Christophe Grenier 2020-01-01 16:34:38 +01:00
parent f5f3120cfa
commit 611da961b3
3 changed files with 17 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/file_mov.c
View file

@ -103,6 +103,7 @@ static void file_rename_mov(file_recovery_t *file_recovery)
/*@
@ requires buffer_size >= 16;
@ requires (buffer_size&1)==0;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires \valid(file_recovery);
@ requires file_recovery->data_check==&data_check_mov;

14
src/file_zip.c
View file

@ -852,22 +852,29 @@ static void file_check_zip(file_recovery_t *fr)
@ requires valid_read_string((char*)file_recovery->filename);
@ requires file_recovery->file_rename==&file_rename_zip;
@*/
/* TODO ensures valid_read_string((char*)file_recovery->filename); */
static void file_rename_zip(file_recovery_t *file_recovery)
{
const char *ext=NULL;
unsigned int file_nbr=0;
file_recovery_t fr;
reset_file_recovery(&fr);
/*@ assert valid_read_string((char*)file_recovery->filename); */
if((fr.handle=fopen(file_recovery->filename, "rb"))==NULL)
{
/*@ assert valid_read_string((char*)file_recovery->filename); */
return;
}
fr.file_size = 0;
fr.offset_error=0;
first_filename[0]='\0';
if(my_fseek(fr.handle, 0, SEEK_SET) < 0)
{
fclose(fr.handle);
/*@ assert valid_read_string((char*)file_recovery->filename); */
return ;
}
/*@ loop invariant valid_read_string((char*)file_recovery->filename); */
while (1)
{
uint32_t header;
@ -875,6 +882,7 @@ static void file_rename_zip(file_recovery_t *file_recovery)
if(file_nbr>=0xffffffff || fr.file_size >= 0x8000000000000000 - 4)
{
fclose(fr.handle);
/*@ assert valid_read_string((char*)file_recovery->filename); */
return;
}
/*@ assert fr.file_size < 0x8000000000000000 - 4; */
@ -885,6 +893,7 @@ static void file_rename_zip(file_recovery_t *file_recovery)
log_trace("Failed to read block header\n");
#endif
fclose(fr.handle);
/*@ assert valid_read_string((char*)file_recovery->filename); */
return;
}
#if defined(__FRAMAC__)
@ -921,7 +930,9 @@ static void file_rename_zip(file_recovery_t *file_recovery)
if(ext!=NULL)
{
fclose(fr.handle);
/*@ assert valid_read_string((char*)file_recovery->filename); */
file_rename(file_recovery, NULL, 0, 0, ext, 1);
/*@ assert valid_read_string((char*)file_recovery->filename); */
return;
}
break;
@ -943,6 +954,7 @@ static void file_rename_zip(file_recovery_t *file_recovery)
if (status<0)
{
fclose(fr.handle);
/*@ assert valid_read_string((char*)file_recovery->filename); */
return;
}
/* Only end of central dir is end of archive, 64b version of it is before */
@ -956,7 +968,9 @@ static void file_rename_zip(file_recovery_t *file_recovery)
first_filename[len]!='/' &&
first_filename[len]!='\\';
len++);
/*@ assert valid_read_string((char*)file_recovery->filename); */
file_rename(file_recovery, first_filename, len, 0, "zip", 0);
/*@ assert valid_read_string((char*)file_recovery->filename); */
return;
}
}

3
src/filegen.h
View file

@ -144,7 +144,8 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
void file_search_footer(file_recovery_t *file_recovery, const void*footer, const unsigned int footer_length, const unsigned int extra_length);
/*@
@ requires buffer_size > 0;
@ requires buffer_size >= 2;
@ requires (buffer_size&1)==0;
@ requires \valid_read((char *)buffer+(0..buffer_size-1));
@ requires \valid(file_recovery);
@ requires file_recovery->data_check == &data_check_size;