From e677eb6b6a2f36a54c94edb13371214e7b4d04b3 Mon Sep 17 00:00:00 2001
From: Christophe Grenier <grenier@cgsecurity.org>
Date: Wed, 23 Jun 2021 07:58:17 +0200
Subject: [PATCH] src/file_indd.c: fix Frama-C warnings

---
 src/file_indd.c | 33 ++++++++++++---------------------
 1 file changed, 12 insertions(+), 21 deletions(-)

diff --git a/src/file_indd.c b/src/file_indd.c
index af20a61c..0e1d019f 100644
--- a/src/file_indd.c
+++ b/src/file_indd.c
@@ -34,10 +34,8 @@
 #include "filegen.h"
 #include "log.h"
 
-/*@ requires \valid(file_stat); */
+/*@ requires valid_register_header_check(file_stat); */
 static void register_header_check_indd(file_stat_t *file_stat);
-static int header_check_indd(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);
-static void file_check_indd(file_recovery_t *file_recovery);
 
 const file_hint_t file_hint_indd= {
   .extension="indd",
@@ -76,16 +74,12 @@ struct InDesignContigObjMarker {
 } __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_indd;
+  @ 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_indd(file_recovery_t *file_recovery)
 {
@@ -104,7 +98,8 @@ static void file_check_indd(file_recovery_t *file_recovery)
     @*/
   do
   {
-    struct InDesignContigObjMarker hdr;
+    char buffer[sizeof(struct InDesignContigObjMarker)];
+    const struct InDesignContigObjMarker *hdr=(const struct InDesignContigObjMarker *)&buffer;;
 #ifdef DEBUG_INDD
     log_info("file_check_indd offset=%llu (0x%llx)\n", (long long unsigned)offset, (long long unsigned)offset);
 #endif
@@ -113,7 +108,7 @@ static void file_check_indd(file_recovery_t *file_recovery)
       file_recovery->file_size=0;
       return ;
     }
-    if(fread(&hdr, sizeof(hdr), 1, file_recovery->handle) != 1)
+    if(fread(buffer, sizeof(buffer), 1, file_recovery->handle) != 1)
     {
       file_recovery->file_size=(offset+4096-1)/4096*4096;
       if(file_recovery->file_size>file_size_org)
@@ -121,9 +116,9 @@ static void file_check_indd(file_recovery_t *file_recovery)
       return ;
     }
 #ifdef __FRAMAC__
-    Frama_C_make_unknown(&hdr, sizeof(hdr));
+    Frama_C_make_unknown(buffer, sizeof(buffer));
 #endif
-    if(memcmp(hdr.fGUID, kINDDContigObjHeaderGUID, sizeof(kINDDContigObjHeaderGUID))!=0)
+    if(memcmp(hdr->fGUID, kINDDContigObjHeaderGUID, sizeof(kINDDContigObjHeaderGUID))!=0)
     {
       file_recovery->file_size=(offset+4096-1)/4096*4096;
       if(file_recovery->file_size>file_size_org)
@@ -131,7 +126,7 @@ static void file_check_indd(file_recovery_t *file_recovery)
       return ;
     }
     /* header + data + trailer */
-    offset+=(uint64_t)le32(hdr.fStreamLength)+2*sizeof(struct InDesignContigObjMarker);
+    offset+=(uint64_t)le32(hdr->fStreamLength)+2*sizeof(struct InDesignContigObjMarker);
   } while(offset < file_size_org);
   file_recovery->file_size=(offset+4096-1)/4096*4096;
   if(file_recovery->file_size>file_size_org)
@@ -141,13 +136,9 @@ static void file_check_indd(file_recovery_t *file_recovery)
 
 /*@
   @ requires buffer_size >= 4096 + sizeof(struct InDesignMasterPage);
-  @ 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_indd, buffer+(..), file_recovery, file_recovery_new);
-  @ ensures \result == 0 || \result == 1;
-  @ ensures  \result!=0 ==> valid_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);
   @*/
 static int header_check_indd(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)
 {