From 611da961b33b7d1d0b68a8d7f87437417055dab5 Mon Sep 17 00:00:00 2001
From: Christophe Grenier <grenier@cgsecurity.org>
Date: Wed, 1 Jan 2020 16:34:38 +0100
Subject: [PATCH] add a few frama-c annotations

---
 src/file_mov.c |  1 +
 src/file_zip.c | 14 ++++++++++++++
 src/filegen.h  |  3 ++-
 3 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/src/file_mov.c b/src/file_mov.c
index 2246cd76..b3303957 100644
--- a/src/file_mov.c
+++ b/src/file_mov.c
@@ -103,6 +103,7 @@ static void file_rename_mov(file_recovery_t *file_recovery)
 
 /*@
   @ requires buffer_size >= 16;
+  @ requires (buffer_size&1)==0;
   @ requires \valid_read(buffer+(0..buffer_size-1));
   @ requires \valid(file_recovery);
   @ requires file_recovery->data_check==&data_check_mov;
diff --git a/src/file_zip.c b/src/file_zip.c
index 50578d94..c674b2fc 100644
--- a/src/file_zip.c
+++ b/src/file_zip.c
@@ -852,22 +852,29 @@ static void file_check_zip(file_recovery_t *fr)
   @ requires valid_read_string((char*)file_recovery->filename);
   @ requires file_recovery->file_rename==&file_rename_zip;
   @*/
+/* TODO ensures  valid_read_string((char*)file_recovery->filename); */
 static void file_rename_zip(file_recovery_t *file_recovery)
 {
   const char *ext=NULL;
   unsigned int file_nbr=0;
   file_recovery_t fr;
   reset_file_recovery(&fr);
+  /*@ assert valid_read_string((char*)file_recovery->filename); */
   if((fr.handle=fopen(file_recovery->filename, "rb"))==NULL)
+  {
+    /*@ assert valid_read_string((char*)file_recovery->filename); */
     return;
+  }
   fr.file_size = 0;
   fr.offset_error=0;
   first_filename[0]='\0';
   if(my_fseek(fr.handle, 0, SEEK_SET) < 0)
   {
     fclose(fr.handle);
+    /*@ assert valid_read_string((char*)file_recovery->filename); */
     return ;
   }
+  /*@ loop invariant valid_read_string((char*)file_recovery->filename); */
   while (1)
   {
     uint32_t header;
@@ -875,6 +882,7 @@ static void file_rename_zip(file_recovery_t *file_recovery)
     if(file_nbr>=0xffffffff || fr.file_size >= 0x8000000000000000 - 4)
     {
       fclose(fr.handle);
+      /*@ assert valid_read_string((char*)file_recovery->filename); */
       return;
     }
     /*@ assert fr.file_size < 0x8000000000000000 - 4; */
@@ -885,6 +893,7 @@ static void file_rename_zip(file_recovery_t *file_recovery)
       log_trace("Failed to read block header\n");
 #endif
       fclose(fr.handle);
+      /*@ assert valid_read_string((char*)file_recovery->filename); */
       return;
     }
 #if defined(__FRAMAC__)
@@ -921,7 +930,9 @@ static void file_rename_zip(file_recovery_t *file_recovery)
 	if(ext!=NULL)
 	{
 	  fclose(fr.handle);
+	  /*@ assert valid_read_string((char*)file_recovery->filename); */
 	  file_rename(file_recovery, NULL, 0, 0, ext, 1);
+	  /*@ assert valid_read_string((char*)file_recovery->filename); */
 	  return;
 	}
         break;
@@ -943,6 +954,7 @@ static void file_rename_zip(file_recovery_t *file_recovery)
     if (status<0)
     {
       fclose(fr.handle);
+      /*@ assert valid_read_string((char*)file_recovery->filename); */
       return;
     }
     /* Only end of central dir is end of archive, 64b version of it is before */
@@ -956,7 +968,9 @@ static void file_rename_zip(file_recovery_t *file_recovery)
 	  first_filename[len]!='/' &&
 	  first_filename[len]!='\\';
 	  len++);
+      /*@ assert valid_read_string((char*)file_recovery->filename); */
       file_rename(file_recovery, first_filename, len, 0, "zip", 0);
+      /*@ assert valid_read_string((char*)file_recovery->filename); */
       return;
     }
   }
diff --git a/src/filegen.h b/src/filegen.h
index 7a1807b3..a7ebde4c 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -144,7 +144,8 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
 void file_search_footer(file_recovery_t *file_recovery, const void*footer, const unsigned int footer_length, const unsigned int extra_length);
 
 /*@
-  @ requires buffer_size > 0;
+  @ requires buffer_size >= 2;
+  @ requires (buffer_size&1)==0;
   @ requires \valid_read((char *)buffer+(0..buffer_size-1));
   @ requires \valid(file_recovery);
   @ requires file_recovery->data_check == &data_check_size;