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

src/file_zip.c: improve Frama-C annotations

Browse source
This commit is contained in:
Christophe Grenier 2023-09-01 07:58:38 +02:00
parent 2457531d2b
commit 14210bd402
1 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/file_zip.c
View file

@ -315,6 +315,7 @@ static const char *zip_parse_parse_entry_mimetype(const char *mime, const unsign
@ requires \valid(fr->handle); @ requires \valid(fr->handle);
@ requires \valid(ext); @ requires \valid(ext);
@ requires fr->file_size < 0x8000000000000000 - 65535; @ requires fr->file_size < 0x8000000000000000 - 65535;
@ requires \valid_read(file);
@ requires 0 < len <= 65535; @ requires 0 < len <= 65535;
@ requires \separated(fr, fr->handle, ext, file, &first_filename[0 .. 256], &errno, &Frama_C_entropy_source); @ requires \separated(fr, fr->handle, ext, file, &first_filename[0 .. 256], &errno, &Frama_C_entropy_source);
@ requires *ext == \null || @ requires *ext == \null ||
@ -431,6 +432,7 @@ static int zip_parse_file_entry_fn(file_recovery_t *fr, const char **ext, const
if(len==8 && memcmp(filename, "mimetype", 8)==0) if(len==8 && memcmp(filename, "mimetype", 8)==0)
{ {
char buffer[128]; char buffer[128];
/*@ assert \valid_read(file); */
const unsigned int compressed_size=le32(file->compressed_size); const unsigned int compressed_size=le32(file->compressed_size);
const int to_read=(compressed_size < 128 ? compressed_size: 128); const int to_read=(compressed_size < 128 ? compressed_size: 128);
const int extra_length=le16(file->extra_length); const int extra_length=le16(file->extra_length);
@ -598,6 +600,8 @@ static int zip_parse_file_entry(file_recovery_t *fr, const char **ext, const uns
char b_extra[sizeof(zip64_extra_entry_t)]; char b_extra[sizeof(zip64_extra_entry_t)];
const zip_file_entry_t *file=(const zip_file_entry_t *)&b_file; const zip_file_entry_t *file=(const zip_file_entry_t *)&b_file;
const zip64_extra_entry_t *extra=(const zip64_extra_entry_t *)&b_extra; const zip64_extra_entry_t *extra=(const zip64_extra_entry_t *)&b_extra;
/*@ assert \valid_read(file); */
/*@ assert \valid_read(extra); */
uint64_t len; uint64_t len;
if (fread(b_file, sizeof(b_file), 1, fr->handle) != 1) if (fread(b_file, sizeof(b_file), 1, fr->handle) != 1)
{ {
@ -746,6 +750,7 @@ static int zip_parse_file_entry(file_recovery_t *fr, const char **ext, const uns
/*@ /*@
@ requires \valid(fr); @ requires \valid(fr);
@ requires \valid(fr->handle); @ requires \valid(fr->handle);
@ requires fr->file_size < 0x8000000000000000;
@ requires \separated(fr, fr->handle, &errno, &Frama_C_entropy_source); @ requires \separated(fr, fr->handle, &errno, &Frama_C_entropy_source);
@ ensures \result == -1 || \result == 0; @ ensures \result == -1 || \result == 0;
@ assigns Frama_C_entropy_source, errno; @ assigns Frama_C_entropy_source, errno;
@ -756,7 +761,9 @@ static int zip_parse_central_dir(file_recovery_t *fr)
char buf_file[sizeof(zip_file_entry_t)]; char buf_file[sizeof(zip_file_entry_t)];
char buf_dir[sizeof(struct zip_central_dir)]; char buf_dir[sizeof(struct zip_central_dir)];
const struct zip_central_dir *dir=(const struct zip_central_dir *)&buf_dir; const struct zip_central_dir *dir=(const struct zip_central_dir *)&buf_dir;
/*@ assert \valid_read(dir); */
const zip_file_entry_t *file=(const zip_file_entry_t *)&buf_file; const zip_file_entry_t *file=(const zip_file_entry_t *)&buf_file;
/*@ assert \valid_read(file); */
uint32_t len; uint32_t len;
if (my_fseek(fr->handle, 2, SEEK_CUR) == -1) if (my_fseek(fr->handle, 2, SEEK_CUR) == -1)
{ {
@ -823,7 +830,7 @@ static int zip64_parse_end_central_dir(file_recovery_t *fr)
{ {
char buffer[sizeof(struct zip64_end_central_dir)]; char buffer[sizeof(struct zip64_end_central_dir)];
const struct zip64_end_central_dir *dir=(const struct zip64_end_central_dir *)&buffer; const struct zip64_end_central_dir *dir=(const struct zip64_end_central_dir *)&buffer;
/*@ assert \valid_read(dir); */
if (fread(&buffer, sizeof(buffer), 1, fr->handle) != 1) if (fread(&buffer, sizeof(buffer), 1, fr->handle) != 1)
{ {
#ifdef DEBUG_ZIP #ifdef DEBUG_ZIP
@ -863,6 +870,7 @@ static int zip64_parse_end_central_dir(file_recovery_t *fr)
/*@ /*@
@ requires \valid(fr); @ requires \valid(fr);
@ requires \valid(fr->handle); @ requires \valid(fr->handle);
@ requires fr->file_size < 0x8000000000000000;
@ requires \separated(fr, fr->handle, &errno, &Frama_C_entropy_source); @ requires \separated(fr, fr->handle, &errno, &Frama_C_entropy_source);
@ ensures \result == -1 || \result == 0; @ ensures \result == -1 || \result == 0;
@ assigns *fr->handle, fr->file_size, errno, Frama_C_entropy_source; @ assigns *fr->handle, fr->file_size, errno, Frama_C_entropy_source;
@ -905,6 +913,7 @@ static int zip_parse_end_central_dir(file_recovery_t *fr)
/*@ /*@
@ requires \valid(fr); @ requires \valid(fr);
@ requires \valid(fr->handle); @ requires \valid(fr->handle);
@ requires fr->file_size < 0x8000000000000000;
@ requires \separated(fr, fr->handle, &errno, &Frama_C_entropy_source); @ requires \separated(fr, fr->handle, &errno, &Frama_C_entropy_source);
@ ensures \result == -1 || \result == 0; @ ensures \result == -1 || \result == 0;
@ assigns *fr->handle, fr->file_size, errno, Frama_C_entropy_source; @ assigns *fr->handle, fr->file_size, errno, Frama_C_entropy_source;
@ -939,6 +948,7 @@ static int zip_parse_data_desc(file_recovery_t *fr)
/*@ /*@
@ requires \valid(fr); @ requires \valid(fr);
@ requires \valid(fr->handle); @ requires \valid(fr->handle);
@ requires fr->file_size < 0x8000000000000000;
@ requires \separated(fr, fr->handle, &errno, &Frama_C_entropy_source); @ requires \separated(fr, fr->handle, &errno, &Frama_C_entropy_source);
@ ensures \result == -1 || \result == 0; @ ensures \result == -1 || \result == 0;
@ assigns *fr->handle, fr->file_size, errno, Frama_C_entropy_source; @ assigns *fr->handle, fr->file_size, errno, Frama_C_entropy_source;
@ -979,6 +989,7 @@ static int zip_parse_signature(file_recovery_t *fr)
/*@ /*@
@ requires \valid(fr); @ requires \valid(fr);
@ requires \valid(fr->handle); @ requires \valid(fr->handle);
@ requires fr->file_size < 0x8000000000000000;
@ requires \separated(fr, fr->handle, &errno); @ requires \separated(fr, fr->handle, &errno);
@ ensures \result == -1 || \result == 0; @ ensures \result == -1 || \result == 0;
@ assigns *fr->handle, fr->file_size, errno; @ assigns *fr->handle, fr->file_size, errno;