summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-12-28 11:59:44 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2019-12-28 11:59:44 +0100
commitcce26972972e1798f36b3347552f56afa4c6ea49 (patch)
tree62f6c546d4ec19ba3fae7f20484930e12a5b87c4
parent8fa5b43d03ae21cfd8bfcd4fab0409af5e768dec (diff)
PhotoRec: src/file_pf.c - additional frama-c annotations for file_rename_pf()
-rw-r--r--src/file_pf.c7
1 files changed, 7 insertions, 0 deletions
diff --git a/src/file_pf.c b/src/file_pf.c
index 7b9a8c6..bff762b 100644
--- a/src/file_pf.c
+++ b/src/file_pf.c
@@ -61,20 +61,27 @@ struct pf_header
@ requires \valid(file_recovery);
@ requires valid_read_string((char*)&file_recovery->filename);
@ 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)
{
FILE *file;
struct pf_header hdr;
if((file=fopen(file_recovery->filename, "rb"))==NULL)
+ {
+ /*@ assert valid_read_string((char*)&file_recovery->filename); */
return;
+ }
if(fread(&hdr, sizeof(hdr), 1, file) <= 0)
{
fclose(file);
+ /*@ assert valid_read_string((char*)&file_recovery->filename); */
return ;
}
fclose(file);
+ /*@ assert valid_read_string((char*)&file_recovery->filename); */
file_rename_unicode(file_recovery, &hdr.name, sizeof(hdr.name), 0, "pf", 0);
+ /*@ assert valid_read_string((char*)&file_recovery->filename); */
}
/*@