From cce26972972e1798f36b3347552f56afa4c6ea49 Mon Sep 17 00:00:00 2001
From: Christophe Grenier <grenier@cgsecurity.org>
Date: Sat, 28 Dec 2019 11:59:44 +0100
Subject: [PATCH] PhotoRec: src/file_pf.c - additional frama-c annotations for
 file_rename_pf()

---
 src/file_pf.c | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/file_pf.c b/src/file_pf.c
index 7b9a8c63..bff762b3 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); */
 }
 
 /*@