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

src/file_sig.c: improve Frama-C annotation for load_signature()

Browse source
This commit is contained in:
Christophe Grenier 2023-10-08 14:43:57 +02:00
parent 2327c1f304
commit 5473a29587
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/file_sig.c
View file

@ -471,13 +471,15 @@ static unsigned int load_hex2(const unsigned char c1, const unsigned char c2)
}
/*@
@ requires \valid(ptr);
@ requires \valid(*ptr);
@ requires valid_string(*ptr);
@ requires \valid(tmp + (0 .. PHOTOREC_MAX_SIG_SIZE-1));
@ requires \separated(ptr, tmp + (..));
@ ensures valid_string(*ptr);
@ ensures \initialized(tmp + (0 .. \result-1));
@ assigns *ptr, tmp[0 .. PHOTOREC_MAX_SIG_SIZE-1];
@*/
/* TODO assigns *ptr, tmp[0 .. PHOTOREC_MAX_SIG_SIZE-1]; */
static unsigned int load_signature(char **ptr, unsigned char *tmp)
{
unsigned int signature_size=0;
@ -649,14 +651,14 @@ static char *parse_signature_line(file_stat_t *file_stat, char *pos)
if(sig_size>0 && sig_offset + sig_size <= PHOTOREC_MAX_SIG_OFFSET )
{
/* FIXME: memory leak for signature */
void *signature;
char *signature;
/*@ assert sig_size > 0; */
/*@ assert sig_offset + sig_size <= PHOTOREC_MAX_SIG_OFFSET; */
signature=(void *)MALLOC(sig_size);
/*@ assert \valid((char *)signature + (0 .. sig_size - 1)); */
signature=(char*)MALLOC(sig_size);
/*@ assert \valid(signature + (0 .. sig_size - 1)); */
memcpy(signature, sig_sig, sig_size);
#ifndef DISABLED_FOR_FRAMAC
signature_insert(sig_ext, sig_offset, signature, sig_size);
#ifndef DISABLED_FOR_FRAMAC
register_header_check(sig_offset, signature, sig_size, &header_check_sig, file_stat);
#endif
}