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

src/file_hdf.c: improve file_check_hdf() annotations

Browse source
This commit is contained in:
Christophe Grenier 2023-10-08 14:33:59 +02:00
parent 7c660ff10b
commit 2ddc089e4d
1 changed files with 44 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

66
src/file_hdf.c
View file

@ -65,48 +65,56 @@ struct dd_struct
} __attribute__ ((gcc_struct, __packed__)); } __attribute__ ((gcc_struct, __packed__));
/*@ /*@
@ requires \separated(file_recovery, file_recovery->handle, &errno, &Frama_C_entropy_source, &__fc_heap_status); @ requires \valid(handle);
@ requires valid_file_check_param(file_recovery); @ requires \valid(dd_buf + (0 .. 65536 * sizeof(struct dd_struct)-1));
@ ensures valid_file_check_result(file_recovery); @ requires \separated(handle, dd_buf + (..), &errno, &Frama_C_entropy_source);
@ assigns *(dd_buf + (0 .. 65536 * sizeof(struct dd_struct)-1));
@ assigns Frama_C_entropy_source;
@ assigns *handle, errno;
@*/ @*/
static void file_check_hdf(file_recovery_t *file_recovery) static uint64_t file_check_hdf_aux(FILE *handle, char *dd_buf)
{ {
uint64_t file_size=0; uint64_t file_size=0;
uint64_t offset_old; uint64_t offset_old;
uint64_t offset=4; uint64_t offset=4;
struct dd_struct *dd=(struct dd_struct *)MALLOC(sizeof(struct dd_struct)*65536); const struct dd_struct *dd=(const struct dd_struct *)dd_buf;
/*@
@ loop assigns file_size, offset_old, offset;
@ loop assigns *(dd_buf + (0 .. 65536 * sizeof(struct dd_struct)-1));
@ loop assigns Frama_C_entropy_source;
@ loop assigns *handle, errno;
@*/
do do
{ {
struct ddh_struct ddh; char ddh_buf[sizeof(struct ddh_struct)];
const struct ddh_struct *ddh=(const struct ddh_struct *)&ddh_buf;
unsigned int i; unsigned int i;
unsigned int size; unsigned int size;
if(my_fseek(file_recovery->handle, offset, SEEK_SET) < 0 || if(my_fseek(handle, offset, SEEK_SET) < 0 ||
fread(&ddh, sizeof(ddh), 1, file_recovery->handle) !=1) fread(&ddh_buf, sizeof(ddh_buf), 1, handle) !=1)
{ {
free(dd); return 0;
file_recovery->file_size=0;
return ;
} }
#ifdef __FRAMAC__ #ifdef __FRAMAC__
Frama_C_make_unknown(&ddh, sizeof(ddh)); Frama_C_make_unknown(&ddh_buf, sizeof(ddh_buf));
#endif #endif
size=be16(ddh.size); size=be16(ddh->size);
/*@ assert 0 <= size < 65536; */
if(size==0 || if(size==0 ||
fread(dd, sizeof(struct dd_struct)*size, 1, file_recovery->handle) !=1) fread(dd_buf, sizeof(struct dd_struct)*size, 1, handle) !=1)
{ {
free(dd); return 0;
file_recovery->file_size=0;
return ;
} }
#ifdef __FRAMAC__ #ifdef __FRAMAC__
Frama_C_make_unknown(dd, sizeof(struct dd_struct)*size); Frama_C_make_unknown(dd_buf, sizeof(struct dd_struct)*size);
#endif #endif
if(file_size < offset + sizeof(struct dd_struct) * size) if(file_size < offset + sizeof(struct dd_struct) * size)
file_size = offset + sizeof(struct dd_struct) * size; file_size = offset + sizeof(struct dd_struct) * size;
#ifdef DEBUG_HDF #ifdef DEBUG_HDF
log_info("size=%u next=%lu\n", size, be32(ddh.next)); log_info("size=%u next=%lu\n", size, be32(ddh->next));
#endif #endif
/*@ /*@
@ loop invariant 0 <= i <= size;
@ loop assigns i, file_size; @ loop assigns i, file_size;
@*/ @*/
for(i=0; i < size; i++) for(i=0; i < size; i++)
@ -123,14 +131,28 @@ static void file_check_hdf(file_recovery_t *file_recovery)
file_size = (uint64_t)p_offset + (uint64_t)p_length; file_size = (uint64_t)p_offset + (uint64_t)p_length;
} }
offset_old=offset; offset_old=offset;
offset=be32(ddh.next); offset=be32(ddh->next);
} while(offset > offset_old); } while(offset > offset_old);
free(dd);
file_size++; file_size++;
return file_size;
}
/*@
@ requires \separated(file_recovery, file_recovery->handle, &errno, &Frama_C_entropy_source, &__fc_heap_status);
@ requires valid_file_check_param(file_recovery);
@ ensures valid_file_check_result(file_recovery);
@*/
static void file_check_hdf(file_recovery_t *file_recovery)
{
uint64_t file_size;
char *dd;
dd=(char *)MALLOC(sizeof(struct dd_struct)*65536);
file_size = file_check_hdf_aux(file_recovery->handle, dd);
free(dd);
#ifdef DEBUG_HDF #ifdef DEBUG_HDF
log_info("file_size %llu\n", (long long unsigned)file_size); log_info("file_size %llu\n", (long long unsigned)file_size);
#endif #endif
if(file_recovery->file_size < file_size) if(file_recovery->file_size < file_size || file_size==0)
file_recovery->file_size=0; file_recovery->file_size=0;
else else
file_recovery->file_size = file_size; file_recovery->file_size = file_size;