From 23e422615dd7b92e0c70159ed38644549141e3be Mon Sep 17 00:00:00 2001
From: Christophe Grenier <grenier@cgsecurity.org>
Date: Fri, 2 Jul 2021 18:48:54 +0200
Subject: [PATCH] src/file_mig.c: fix Frama-C warnings

---
 src/file_mig.c | 34 ++++++++++++++--------------------
 1 file changed, 14 insertions(+), 20 deletions(-)

diff --git a/src/file_mig.c b/src/file_mig.c
index 31f3a3f0..1930788e 100644
--- a/src/file_mig.c
+++ b/src/file_mig.c
@@ -35,7 +35,7 @@
 #include "log.h"
 #endif
 
-/*@ requires \valid(file_stat); */
+/*@ requires valid_register_header_check(file_stat); */
 static void register_header_check_mig(file_stat_t *file_stat);
 
 const file_hint_t file_hint_mig= {
@@ -61,16 +61,12 @@ struct MIG_HDR
 } __attribute__ ((gcc_struct, __packed__));
 
 /*@
-  @ requires valid_file_recovery(file_recovery);
-  @ requires \valid(file_recovery->handle);
-  @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
-  @ requires \initialized(&file_recovery->time);
-  @
   @ requires file_recovery->file_check == &file_check_mig;
+  @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
+  @ requires valid_file_check_param(file_recovery);
+  @ ensures  valid_file_check_result(file_recovery);
   @ assigns *file_recovery->handle, errno, file_recovery->file_size;
   @ assigns Frama_C_entropy_source;
-  @
-  @ ensures \valid(file_recovery->handle);
   @*/
 static void file_check_mig(file_recovery_t *file_recovery)
 {
@@ -83,7 +79,8 @@ static void file_check_mig(file_recovery_t *file_recovery)
     @*/
   while(1)
   {
-    struct MIG_HDR h;
+    char buffer[sizeof(struct MIG_HDR)];
+    const struct MIG_HDR *h=(const struct MIG_HDR *)&buffer;
     size_t res;
     if(my_fseek(file_recovery->handle, offset, SEEK_SET) < 0)
     {
@@ -92,7 +89,7 @@ static void file_check_mig(file_recovery_t *file_recovery)
 #endif
       return ;
     }
-    res=fread(&h, 1, sizeof(h), file_recovery->handle);
+    res=fread(&buffer, 1, sizeof(buffer), file_recovery->handle);
     if(res < 8)
     {
 #ifdef DEBUG_MIG
@@ -100,31 +97,28 @@ static void file_check_mig(file_recovery_t *file_recovery)
 #endif
       return ;
     }
-    if(res < sizeof(h) || le32(h.magic)!=0x5354524d)	/* STRM=stream */
+    /* STRM=stream */
+    if(res < sizeof(buffer) || le32(h->magic)!=0x5354524d || offset >= PHOTOREC_MAX_FILE_SIZE)
     {
 #ifdef DEBUG_MIG
-      log_info("0x%lx no magic %x\n", (long unsigned)offset, le32(h.magic));
+      log_info("0x%lx no magic %x\n", (long unsigned)offset, le32(h->magic));
 #endif
       file_recovery->file_size=offset+8;
       return ;
     }
 #ifdef DEBUG_MIG
-    log_info("0x%lx magic s_size=0x%u\n", (long unsigned)offset, le32(h.s_size));
+    log_info("0x%lx magic s_size=0x%u\n", (long unsigned)offset, le32(h->s_size));
 #endif
-    offset+=sizeof(h)+le32(h.s_size);
+    offset+=sizeof(buffer)+le32(h->s_size);
   }
 }
 
 /*@
   @ requires buffer_size > 0x38;
-  @ requires \valid_read(buffer+(0..buffer_size-1));
-  @ requires valid_file_recovery(file_recovery);
-  @ requires \valid(file_recovery_new);
-  @ requires file_recovery_new->blocksize > 0;
   @ requires separation: \separated(&file_hint_mig, buffer+(..), file_recovery, file_recovery_new);
+  @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ ensures  valid_header_check_result(\result, file_recovery_new);
   @ assigns  *file_recovery_new;
-  @ ensures \result == 0 || \result == 1;
-  @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
   @*/
 static int header_check_mig(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
 {