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

PhotoRec: src/file_pf.c - additional frama-c annotations for file_rename_pf()

Browse Source
This commit is contained in:
Christophe Grenier 2019-12-28 11:59:44 +01:00
parent 8fa5b43d03
commit cce2697297
1 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/file_pf.c
View File

@ -61,20 +61,27 @@ struct pf_header
@ requires \valid(file_recovery); @ requires \valid(file_recovery);
@ requires valid_read_string((char*)&file_recovery->filename); @ requires valid_read_string((char*)&file_recovery->filename);
@ requires file_recovery->file_rename==&file_rename_pf; @ requires file_recovery->file_rename==&file_rename_pf;
@ ensures valid_read_string((char*)&file_recovery->filename);
@*/ @*/
static void file_rename_pf(file_recovery_t *file_recovery) static void file_rename_pf(file_recovery_t *file_recovery)
{ {
FILE *file; FILE *file;
struct pf_header hdr; struct pf_header hdr;
if((file=fopen(file_recovery->filename, "rb"))==NULL) if((file=fopen(file_recovery->filename, "rb"))==NULL)
{
/*@ assert valid_read_string((char*)&file_recovery->filename); */
return; return;
}
if(fread(&hdr, sizeof(hdr), 1, file) <= 0) if(fread(&hdr, sizeof(hdr), 1, file) <= 0)
{ {
fclose(file); fclose(file);
/*@ assert valid_read_string((char*)&file_recovery->filename); */
return ; return ;
} }
fclose(file); fclose(file);
/*@ assert valid_read_string((char*)&file_recovery->filename); */
file_rename_unicode(file_recovery, &hdr.name, sizeof(hdr.name), 0, "pf", 0); file_rename_unicode(file_recovery, &hdr.name, sizeof(hdr.name), 0, "pf", 0);
/*@ assert valid_read_string((char*)&file_recovery->filename); */
} }
/*@ /*@