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

src/file_psb.c: improve Frama-C annotations

Browse source
This commit is contained in:
Christophe Grenier 2023-10-08 14:35:55 +02:00
parent 4730b7aa87
commit 51f8d1310b
1 changed files with 13 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/file_psb.c
View file

@ -92,6 +92,9 @@ static uint64_t get_be64(const void *buffer, const unsigned int offset)
@*/ @*/
static data_check_t psb_skip_image_data(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery) static data_check_t psb_skip_image_data(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{ {
/*@ assert file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; */
/*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */
/*@ assert buffer_size <= 2 * PHOTOREC_MAX_BLOCKSIZE; */
file_recovery->calculated_file_size+=2; file_recovery->calculated_file_size+=2;
file_recovery->data_check=NULL; file_recovery->data_check=NULL;
return DC_CONTINUE; return DC_CONTINUE;
@ -103,10 +106,13 @@ static data_check_t psb_skip_image_data(const unsigned char *buffer, const unsig
@ ensures valid_data_check_result(\result, file_recovery); @ ensures valid_data_check_result(\result, file_recovery);
@ ensures file_recovery->data_check==&psb_skip_layer_info || file_recovery->data_check==\null; @ ensures file_recovery->data_check==&psb_skip_layer_info || file_recovery->data_check==\null;
@ ensures \result == DC_CONTINUE || \result == DC_STOP; @ ensures \result == DC_CONTINUE || \result == DC_STOP;
@ assigns file_recovery->data_check, file_recovery->file_check, file_recovery->calculated_file_size; @ assigns file_recovery->data_check, file_recovery->calculated_file_size;
@*/ @*/
static data_check_t psb_skip_layer_info(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery) static data_check_t psb_skip_layer_info(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{ {
/*@ assert file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; */
/*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */
/*@ assert buffer_size <= 2 * PHOTOREC_MAX_BLOCKSIZE; */
if(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size && if(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size &&
file_recovery->calculated_file_size + 8 < file_recovery->file_size + buffer_size/2) file_recovery->calculated_file_size + 8 < file_recovery->file_size + buffer_size/2)
{ {
@ -137,6 +143,9 @@ static data_check_t psb_skip_layer_info(const unsigned char *buffer, const unsig
@*/ @*/
static data_check_t psb_skip_image_resources(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery) static data_check_t psb_skip_image_resources(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{ {
/*@ assert file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; */
/*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */
/*@ assert buffer_size <= 2 * PHOTOREC_MAX_BLOCKSIZE; */
if(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size && if(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size &&
file_recovery->calculated_file_size + 4 < file_recovery->file_size + buffer_size/2) file_recovery->calculated_file_size + 4 < file_recovery->file_size + buffer_size/2)
{ {
@ -171,6 +180,9 @@ static data_check_t psb_skip_color_mode(const unsigned char *buffer, const unsig
const unsigned int depth=be16(hdr->depth); const unsigned int depth=be16(hdr->depth);
const unsigned int height=be32(hdr->height); const unsigned int height=be32(hdr->height);
const unsigned int width=be32(hdr->width); const unsigned int width=be32(hdr->width);
/*@ assert file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; */
/*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */
/*@ assert buffer_size <= 2 * PHOTOREC_MAX_BLOCKSIZE; */
if(channels==0 || channels>56 || if(channels==0 || channels>56 ||
height==0 || height>300000 || height==0 || height>300000 ||
width==0 || width>300000 || width==0 || width>300000 ||