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

src/file_fits.c: two integer overflow remains...

Browse source
This commit is contained in:
Christophe Grenier 2021-02-20 18:35:23 +01:00
parent 756a415fe8
commit e887a34a85
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/file_fits.c
View file

@ -164,12 +164,13 @@ static uint64_t fits_info(const unsigned char *buffer, const unsigned int buffer
@ requires (buffer_size&1)==0; @ requires (buffer_size&1)==0;
@ requires \valid_read(buffer+(0..buffer_size-1)); @ requires \valid_read(buffer+(0..buffer_size-1));
@ requires \valid(file_recovery); @ requires \valid(file_recovery);
@ requires valid_file_recovery(file_recovery);
@ requires file_recovery->data_check==&data_check_fits; @ requires file_recovery->data_check==&data_check_fits;
@ requires file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; @ requires file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE;
@ requires \separated(buffer, file_recovery); @ requires \separated(buffer, file_recovery);
@ ensures \result == DC_CONTINUE || \result == DC_STOP; @ ensures \result == DC_CONTINUE || \result == DC_STOP;
@ assigns file_recovery->calculated_file_size, file_recovery->time;
@*/ @*/
/* assigns file_recovery->calculated_file_size, file_recovery->time; */
static data_check_t data_check_fits(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery) static data_check_t data_check_fits(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{ {
/*@ /*@