From 0933bc5bb269ab503ccbb0ff5f393fcafc69b164 Mon Sep 17 00:00:00 2001
From: Christophe Grenier <grenier@cgsecurity.org>
Date: Sat, 10 Apr 2021 11:34:54 +0200
Subject: [PATCH] file_*.c: add various Frama-C annotations

---
 src/file_ace.c      |  8 ++------
 src/file_amd.c      |  4 ++--
 src/file_amr.c      |  3 ++-
 src/file_arj.c      |  8 ++++----
 src/file_bmp.c      |  4 +---
 src/file_dir.c      |  2 ++
 src/file_fits.c     |  4 ++--
 src/file_found.h    |  5 +++++
 src/file_gz.c       |  1 +
 src/file_list.c     |  2 +-
 src/file_mlv.c      |  1 +
 src/file_png.c      |  1 +
 src/file_template.c |  1 +
 src/file_tiff.c     |  4 ++--
 src/file_tivo.c     | 26 +++++++++++++-------------
 src/filegen.c       |  2 +-
 src/filegen.h       |  3 +--
 17 files changed, 42 insertions(+), 37 deletions(-)

diff --git a/src/file_ace.c b/src/file_ace.c
index a39e170c..3d636858 100644
--- a/src/file_ace.c
+++ b/src/file_ace.c
@@ -111,10 +111,8 @@ static int check_ace_crc(FILE *handle, const unsigned int len, const unsigned in
 }
 
 /*@
-  @ requires \valid(file_recovery);
+  @ requires valid_file_recovery(file_recovery);
   @ requires \valid(file_recovery->handle);
-  @ requires \valid_read(&file_recovery->extension);
-  @ requires valid_read_string(file_recovery->extension);
   @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
   @ requires \initialized(&file_recovery->time);
   @
@@ -143,9 +141,7 @@ static void file_check_ace(file_recovery_t *file_recovery)
     {
       return ;
     }
-#ifdef __FRAMAC__
-    Frama_C_make_unknown(&buffer, sizeof(buffer));
-#endif
+    /*@ assert \initialized(&buffer + (0 .. sizeof(buffer)-1)); */
 #ifdef DEBUG_ACE
     log_info("file_ace: Block header at 0x%08lx: CRC16=0x%04X size=%u type=%u"
         " flags=0x%04X addsize=%u\n",
diff --git a/src/file_amd.c b/src/file_amd.c
index d7ed82a1..eb05fdb8 100644
--- a/src/file_amd.c
+++ b/src/file_amd.c
@@ -51,9 +51,9 @@ const file_hint_t file_hint_amd= {
   @ requires \valid(file_recovery_new);
   @ requires file_recovery_new->blocksize > 0;
   @ requires separation: \separated(&file_hint_amd, buffer+(..), file_recovery, file_recovery_new);
-  @ assigns  *file_recovery_new;
   @ ensures \result == 0 || \result == 1;
   @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
+  @ assigns  *file_recovery_new;
   @*/
 static int header_check_amd(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)
 {
@@ -73,9 +73,9 @@ static int header_check_amd(const unsigned char *buffer, const unsigned int buff
   @ requires \valid(file_recovery_new);
   @ requires file_recovery_new->blocksize > 0;
   @ requires separation: \separated(&file_hint_amd, buffer+(..), file_recovery, file_recovery_new);
-  @ assigns  *file_recovery_new;
   @ ensures \result == 0 || \result == 1;
   @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
+  @ assigns  *file_recovery_new;
   @*/
 static int header_check_amt(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)
 {
diff --git a/src/file_amr.c b/src/file_amr.c
index 9b76d25f..2e91205d 100644
--- a/src/file_amr.c
+++ b/src/file_amr.c
@@ -94,8 +94,9 @@ static data_check_t data_check_amr(const unsigned char *buffer, const unsigned i
   @ requires \valid(file_recovery_new);
   @ requires file_recovery_new->blocksize > 0;
   @ requires separation: \separated(&file_hint_amr, buffer+(..), file_recovery, file_recovery_new);
-  @ assigns  *file_recovery_new;
+  @ ensures  \result == 0 || \result == 1;
   @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
+  @ assigns  *file_recovery_new;
   @*/
 static int header_check_amr(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)
 {
diff --git a/src/file_arj.c b/src/file_arj.c
index c86a7951..e2e392d8 100644
--- a/src/file_arj.c
+++ b/src/file_arj.c
@@ -119,13 +119,13 @@ struct arj_main_header {
 } __attribute__ ((gcc_struct, __packed__));
 
 /*@
+  @ requires \valid(file_recovery);
   @ requires valid_file_recovery(file_recovery);
   @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
   @ requires file_recovery->file_check == &file_check_arj;
+  @ ensures \valid(file_recovery->handle);
   @ assigns *file_recovery->handle, errno, file_recovery->file_size;
   @ assigns Frama_C_entropy_source;
-  @
-  @ ensures \valid(file_recovery->handle);
   @*/
 static void file_check_arj(file_recovery_t *file_recovery)
 {
@@ -134,14 +134,14 @@ static void file_check_arj(file_recovery_t *file_recovery)
 }
 
 /*@
-  @ requires buffer_size > sizeof(struct arj_main_header);
+  @ requires buffer_size >= sizeof(struct arj_main_header);
   @ 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_arj, buffer+(..), file_recovery, file_recovery_new);
-  @ assigns  *file_recovery_new;
   @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
+  @ assigns  *file_recovery_new;
   @*/
 static int header_check_arj(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)
 {
diff --git a/src/file_bmp.c b/src/file_bmp.c
index b2d56b06..841ed92a 100644
--- a/src/file_bmp.c
+++ b/src/file_bmp.c
@@ -99,10 +99,8 @@ struct bmp_header
   @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
   @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
   @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
-  @ ensures (\result == 1) ==>  \separated(file_recovery_new, file_recovery_new->extension);
-  @ ensures *buffer==\old(*buffer);
   @*/
-  /* TODO ensures *file_recovery==\old(*file_recovery); */
+// ensures (\result == 1) ==>  \separated(file_recovery_new, file_recovery_new->extension);
 static int header_check_bmp(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)
 {
   const struct bmp_header *bm=(const struct bmp_header *)buffer;
diff --git a/src/file_dir.c b/src/file_dir.c
index 1abbf0f3..54a97777 100644
--- a/src/file_dir.c
+++ b/src/file_dir.c
@@ -66,6 +66,7 @@ static void file_rename_fatdir(file_recovery_t *file_recovery)
   fclose(file);
   if(buffer_size<32)
     return;
+  /*@ assert buffer_size >= 32; */
   cluster=fat_get_cluster_from_entry((const struct msdos_dir_entry *)&buffer[0]);
   sprintf(buffer_cluster, "cluster_%u", cluster);
   file_rename(file_recovery, buffer_cluster, strlen(buffer_cluster), 0, NULL, 1);
@@ -109,6 +110,7 @@ static int header_check_dir(const unsigned char *buffer, const unsigned int buff
   file_recovery_new->file_check=&file_check_size;
   file_recovery_new->file_rename=&file_rename_fatdir;
   file_recovery_new->time=date_dos2unix(le16(de->time),le16(de->date));
+  /*@ assert valid_file_recovery(file_recovery_new); */
   return 1;
 }
 
diff --git a/src/file_fits.c b/src/file_fits.c
index 5882573c..ff2ba0c3 100644
--- a/src/file_fits.c
+++ b/src/file_fits.c
@@ -118,7 +118,7 @@ static uint64_t fits_info(const unsigned char *buffer, const unsigned int buffer
       if(tmp > PHOTOREC_MAX_FILE_SIZE)
 	naxis_size=0;
       else if(tmp>0)
-      {
+      { /* FIXME overflow */
 	naxis_size*=(tmp+8-1)/8;
       }
     }
@@ -135,7 +135,7 @@ static uint64_t fits_info(const unsigned char *buffer, const unsigned int buffer
       if(naxis_val > PHOTOREC_MAX_FILE_SIZE)
 	naxis_size=0;
       else
-      {
+      { /* FIXME overflow */
 	naxis_size*=naxis_val;
       }
     }
diff --git a/src/file_found.h b/src/file_found.h
index e03f3194..9607c404 100644
--- a/src/file_found.h
+++ b/src/file_found.h
@@ -25,6 +25,11 @@
 extern "C" {
 #endif
 
+/*@
+  @ requires \valid(current_search_space);
+  @ requires \valid(file_stat);
+  @ requires \separated(current_search_space, file_stat);
+  @*/
 alloc_data_t *file_found(alloc_data_t *current_search_space, const uint64_t offset, file_stat_t *file_stat);
 
 #ifdef __cplusplus
diff --git a/src/file_gz.c b/src/file_gz.c
index 3cb62827..33b017af 100644
--- a/src/file_gz.c
+++ b/src/file_gz.c
@@ -249,6 +249,7 @@ static int header_check_gz(const unsigned char *buffer, const unsigned int buffe
 #endif
     if(file_recovery->file_check==&file_check_bgzf)
     {
+      /*@ assert \valid_function(file_recovery->file_check); */
       header_ignored(file_recovery_new);
       return 0;
     }
diff --git a/src/file_list.c b/src/file_list.c
index 962d9abb..0ab9e9f8 100644
--- a/src/file_list.c
+++ b/src/file_list.c
@@ -371,7 +371,7 @@ extern const file_hint_t file_hint_zpr;
 
 file_enable_t array_file_enable[]=
 {
-#if (!defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_sig)) && !defined(__FRAMAC__)
+#if ((!defined(SINGLE_FORMAT)  && !defined(__FRAMAC__)) || defined(SINGLE_FORMAT_sig))
   { .enable=0, .file_hint=&file_hint_sig  },
 #endif
 #if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_1cd)
diff --git a/src/file_mlv.c b/src/file_mlv.c
index 00fc6cde..2f2d9db7 100644
--- a/src/file_mlv.c
+++ b/src/file_mlv.c
@@ -161,6 +161,7 @@ static void file_check_mlv(file_recovery_t *file_recovery)
 
 /*@
   @ requires valid_file_recovery(file_recovery);
+  @ requires file_recovery->file_rename == &file_rename_mlv;
   @*/
 static void file_rename_mlv(file_recovery_t *file_recovery)
 {
diff --git a/src/file_png.c b/src/file_png.c
index 00be0be9..1f66ec80 100644
--- a/src/file_png.c
+++ b/src/file_png.c
@@ -41,6 +41,7 @@
 
 extern const file_hint_t file_hint_doc;
 
+/*@ requires \valid(file_stat); */
 static void register_header_check_png(file_stat_t *file_stat);
 static data_check_t data_check_png(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
 static data_check_t data_check_mng(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
diff --git a/src/file_template.c b/src/file_template.c
index eb1f0528..37733700 100644
--- a/src/file_template.c
+++ b/src/file_template.c
@@ -31,6 +31,7 @@
 #include "types.h"
 #include "filegen.h"
 
+/*@ requires \valid(file_stat); */
 static void register_header_check_EXTENSION(file_stat_t *file_stat);
 
 const file_hint_t file_hint_EXTENSION= {
diff --git a/src/file_tiff.c b/src/file_tiff.c
index cf79e732..17edb1f9 100644
--- a/src/file_tiff.c
+++ b/src/file_tiff.c
@@ -20,7 +20,7 @@
 
  */
 
-#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tiff) || defined(SINGLE_FORMAT_jpg) || defined(SINGLE_FORMAT_rw2) || defined(SINGLE_FORMAT_orf)
+#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tiff) || defined(SINGLE_FORMAT_jpg) || defined(SINGLE_FORMAT_rw2) || defined(SINGLE_FORMAT_orf) || defined(SINGLE_FORMAT_wdp)
 #ifdef HAVE_CONFIG_H
 #include <config.h>
 #endif
@@ -185,7 +185,7 @@ static void register_header_check_tiff(file_stat_t *file_stat)
 {
   static const unsigned char tiff_header_be[4]= { 'M','M',0x00, 0x2a};
   static const unsigned char tiff_header_le[4]= { 'I','I',0x2a, 0x00};
-#if !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2) && !defined(SINGLE_FORMAT_orf)
+#if !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2) && !defined(SINGLE_FORMAT_orf) && !defined(SINGLE_FORMAT_wdp)
 #if !defined(MAIN_tiff_le) && !defined(MAIN_jpg)
   register_header_check(0, tiff_header_be, sizeof(tiff_header_be), &header_check_tiff_be, file_stat);
 #endif
diff --git a/src/file_tivo.c b/src/file_tivo.c
index 966f2575..a739e677 100644
--- a/src/file_tivo.c
+++ b/src/file_tivo.c
@@ -34,13 +34,13 @@
 /*@ requires \valid(file_stat); */
 static void register_header_check_tivo(file_stat_t *file_stat);
 
-const file_hint_t file_hint_tivo= {
-  .extension="TiVo",
-  .description="TiVo video record",
-  .max_filesize=PHOTOREC_MAX_FILE_SIZE,
-  .recover=1,
-  .enable_by_default=1,
-  .register_header_check=&register_header_check_tivo
+const file_hint_t file_hint_tivo = {
+  .extension = "TiVo",
+  .description = "TiVo video record",
+  .max_filesize = PHOTOREC_MAX_FILE_SIZE,
+  .recover = 1,
+  .enable_by_default = 1,
+  .register_header_check = &register_header_check_tivo
 };
 
 /*@
@@ -54,7 +54,7 @@ const file_hint_t file_hint_tivo= {
   @*/
 static void file_check_tivo(file_recovery_t *file_recovery)
 {
-  const unsigned char tivo_footer[8]= {
+  const unsigned char tivo_footer[8] = {
     0x00, 0x00, 0x01, 0xb7, 0x00, 0x00, 0x01, 0xb9
   };
   file_search_footer(file_recovery, tivo_footer, sizeof(tivo_footer), 0);
@@ -73,18 +73,18 @@ static void file_check_tivo(file_recovery_t *file_recovery)
   @*/
 static int header_check_tivo(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)
 {
-  if(memcmp(&buffer[0x1c], "<?xml ", 6)!=0)
+  if(memcmp(&buffer[0x1c], "<?xml ", 6) != 0)
     return 0;
   reset_file_recovery(file_recovery_new);
-  file_recovery_new->extension=file_hint_tivo.extension;
-  file_recovery_new->file_check=&file_check_tivo;
+  file_recovery_new->extension = file_hint_tivo.extension;
+  file_recovery_new->file_check = &file_check_tivo;
   return 1;
 }
 
 static void register_header_check_tivo(file_stat_t *file_stat)
 {
-  static const unsigned char tivo_header[7]=  {
-    'T' , 'i' , 'V' , 'o' , 0x00, 0x04, 0x00
+  static const unsigned char tivo_header[7] = {
+    'T', 'i', 'V', 'o', 0x00, 0x04, 0x00
   };
   register_header_check(0, tivo_header, sizeof(tivo_header), &header_check_tivo, file_stat);
 }
diff --git a/src/filegen.c b/src/filegen.c
index f1b457a7..d8bdbffb 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -758,7 +758,7 @@ void header_ignored_cond_reset(uint64_t start, uint64_t end)
 /* 0: file_recovery_new->location.start has been taken into account, offset_skipped_header may have been updated
  * 1: file_recovery_new->location.start has been ignored */
 /*@
-  @ requires separation: \separated(file_recovery, file_recovery_new, &errno, &offset_skipped_header);
+  @ requires separation: \separated(file_recovery, file_recovery->handle, file_recovery_new, &errno, &offset_skipped_header);
   @*/
 int header_ignored_adv(const file_recovery_t *file_recovery, const file_recovery_t *file_recovery_new)
 {
diff --git a/src/filegen.h b/src/filegen.h
index 415d9067..1c94ab04 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -319,7 +319,7 @@ void header_ignored_cond_reset(uint64_t start, uint64_t end);
 void header_ignored(const file_recovery_t *file_recovery_new);
 
 /*@
-  @ requires separation: \separated(file_recovery, file_recovery_new, &errno);
+  @ requires separation: \separated(file_recovery, file_recovery->handle, file_recovery_new, &errno);
   @ requires \valid_read(file_recovery);
   @ requires \valid_read(file_recovery_new);
   @ requires valid_file_recovery(file_recovery);
@@ -327,7 +327,6 @@ void header_ignored(const file_recovery_t *file_recovery_new);
   @ requires \valid_function(file_recovery->file_check);
   @ requires \initialized(&file_recovery->file_check);
   @ requires \initialized(&file_recovery->handle);
-  @ requires \separated(file_recovery, file_recovery->handle);
   @ ensures \result == 0 || \result == 1;
   @*/
 // ensures  valid_file_recovery(file_recovery);