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

src/filegen.c: add more Frama-C annotations

Browse source
This commit is contained in:
Christophe Grenier 2021-03-20 14:46:35 +01:00
parent 6d4908eb2f
commit b0ca4399a9
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/filegen.c
View file

@ -492,6 +492,7 @@ static int file_rename_aux(file_recovery_t *file_recovery, const char *new_ext)
@ requires \valid_read((char *)buffer+(0..buffer_size-1));
@ requires new_ext==\null || valid_read_string(new_ext);
@ ensures valid_read_string((char*)&file_recovery->filename);
@ ensures new_ext==\null || valid_read_string(new_ext);
@*/
static int _file_rename(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int append_original_ext)
{
@ -608,9 +609,12 @@ static int _file_rename(file_recovery_t *file_recovery, const void *buffer, cons
/* The original filename begins at offset in buffer and is null terminated */
int file_rename(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int append_original_ext)
{
/*@ assert new_ext==\null || valid_read_string(new_ext); */
if(buffer!=NULL && 0 <= offset && offset < buffer_size &&
_file_rename(file_recovery, buffer, buffer_size, offset, new_ext, append_original_ext)==0)
return 0;
/*@ assert valid_read_string((char const *)(&file_recovery->filename)); */
/*@ assert new_ext==\null || valid_read_string(new_ext); */
if(new_ext==NULL)
return 0;
/* Try without the original filename */