src/filegen.[ch]: update frama-c annotations

1 files changed, 71 insertions, 25 deletions

diff --git a/src/filegen.h b/src/filegen.h
index 6ced8ea8..0428f51f 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -40,9 +40,20 @@ extern "C" {
 
 typedef enum { DC_SCAN=0, DC_CONTINUE=1, DC_STOP=2, DC_ERROR=3} data_check_t;
 typedef struct file_hint_struct file_hint_t;
+typedef struct file_stat_struct file_stat_t;
 typedef struct file_recovery_struct file_recovery_t;
 typedef struct file_enable_struct file_enable_t;
-typedef struct file_stat_struct file_stat_t;
+
+struct file_hint_struct
+{
+  const char *extension;
+  const char *description;
+  const uint64_t max_filesize;
+  const int recover;
+  const unsigned int enable_by_default;
+  void (*register_header_check)(file_stat_t *file_stat);
+};
+
 typedef struct
 {
   struct td_list_head list;
@@ -80,7 +91,7 @@ struct file_recovery_struct
   uint64_t extra;	/* extra bytes between offset_ok and offset_error */
   uint64_t calculated_file_size;
   data_check_t (*data_check)(const unsigned char*buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
-  /* data_check modifies file_recovery->calculated_file_size but not must alter file_recovery->file_size */
+  /* data_check modifies file_recovery->calculated_file_size, it can also update data_check, file_check, offset_error */
   void (*file_check)(file_recovery_t *file_recovery);
   void (*file_rename)(file_recovery_t *file_recovery);
   uint64_t checkpoint_offset;
@@ -89,16 +100,6 @@ struct file_recovery_struct
   unsigned int flags;
 };
 
-struct file_hint_struct
-{
-  const char *extension;
-  const char *description;
-  const uint64_t max_filesize;
-  const int recover;
-  const unsigned int enable_by_default;
-  void (*register_header_check)(file_stat_t *file_stat);
-};
-
 typedef struct
 {
   struct td_list_head list;
@@ -121,11 +122,35 @@ typedef struct
 #define NL_CRLF         (1 << 1)
 #define NL_BARECR       (1 << 2)
 
+/*@
+   predicate valid_file_hint(file_hint_t *file_hint) = (\valid_read(file_hint) && valid_read_string(file_hint->description));
+  @*/
+
+/*@
+   predicate valid_file_stat(file_stat_t *file_stat) = (\valid_read(file_stat) && valid_file_hint(file_stat->file_hint));
+  @*/
+
+/*@
+   predicate valid_file_recovery(file_recovery_t *file_recovery) = (\valid_read(file_recovery) &&
+        valid_read_string((const char *)file_recovery->filename) &&
+	(file_recovery->file_stat == \null || valid_file_stat(file_recovery->file_stat)) &&
+	(file_recovery->handle == \null || \valid(file_recovery->handle)) &&
+        (file_recovery->extension == \null || valid_read_string(file_recovery->extension)) &&
+	(file_recovery->data_check == \null || \valid_function(file_recovery->data_check)) &&
+	(file_recovery->file_check == \null || \valid_function(file_recovery->file_check)) &&
+	(file_recovery->file_rename == \null || \valid_function(file_recovery->file_rename))
+	);
+  @*/
+/*@
+    predicate valid_list_search_space(alloc_data_t *list) = (\valid_read(list) && \valid(list->list.prev) && \valid_read(list->list.next));
+  @*/
+
 void free_header_check(void);
 
 /*@
   @ requires \valid(file_recovery);
   @ requires \valid(file_recovery->handle);
+  @ requires valid_file_recovery(file_recovery);
   @ requires \separated(file_recovery, file_recovery->handle, &errno, &Frama_C_entropy_source);
   @ ensures file_recovery->handle == \old(file_recovery->handle);
   @ assigns *file_recovery->handle, errno, Frama_C_entropy_source, file_recovery->file_size;
@@ -144,10 +169,12 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
 /*@
   @ requires \valid(file_recovery);
   @ requires \valid(file_recovery->handle);
+  @ requires valid_file_recovery(file_recovery);
   @ requires 0 < footer_length < 4096;
   @ requires \valid_read((char *)footer+(0..footer_length-1));
   @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
   @ ensures \valid(file_recovery->handle);
+  @ ensures valid_file_recovery(file_recovery);
   @ assigns *file_recovery->handle, errno, file_recovery->file_size;
   @ assigns Frama_C_entropy_source;
   @*/
@@ -159,29 +186,39 @@ void file_search_footer(file_recovery_t *file_recovery, const void*footer, const
   @ requires \valid_read((char *)buffer+(0..buffer_size-1));
   @ requires \valid(file_recovery);
   @ requires file_recovery->data_check == &data_check_size;
-  @ ensures \result == DC_STOP || \result == DC_CONTINUE;
-  @ ensures file_recovery->data_check == &data_check_size;
-  @ assigns \nothing;
+  @ requires valid_file_recovery(file_recovery);
+  @ requires \initialized(&file_recovery->file_size);
+  @ requires \initialized(&file_recovery->calculated_file_size);
+  @ ensures  valid_file_recovery(file_recovery);
+  @ ensures  \result == DC_STOP || \result == DC_CONTINUE;
+  @ ensures  file_recovery->data_check == &data_check_size;
+  @ assigns  \nothing;
   @*/
 data_check_t data_check_size(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
 
 /*@
   @ requires \valid(file_recovery);
   @ requires file_recovery->file_check == &file_check_size;
-  @ assigns file_recovery->file_size;
+  @ requires valid_file_recovery(file_recovery);
+  @ ensures  valid_file_recovery(file_recovery);
+  @ assigns  file_recovery->file_size;
   @*/
 void file_check_size(file_recovery_t *file_recovery);
 
 /*@
   @ requires \valid(file_recovery);
   @ requires file_recovery->file_check == &file_check_size_min;
-  @ assigns file_recovery->file_size;
+  @ requires valid_file_recovery(file_recovery);
+  @ ensures  valid_file_recovery(file_recovery);
+  @ assigns  file_recovery->file_size;
   @*/
 void file_check_size_min(file_recovery_t *file_recovery);
 
 /*@
   @ requires \valid(file_recovery);
   @ requires file_recovery->file_check == &file_check_size_max;
+  @ requires valid_file_recovery(file_recovery);
+  @ ensures  valid_file_recovery(file_recovery);
   @ assigns file_recovery->file_size;
   @*/
 void file_check_size_max(file_recovery_t *file_recovery);
@@ -231,12 +268,13 @@ void file_check_size_max(file_recovery_t *file_recovery);
   assigns file_recovery->flags;
   assigns file_recovery->extra;
 */
+//  ensures valid_file_recovery(file_recovery);
 void reset_file_recovery(file_recovery_t *file_recovery);
 
 /*@
   @ requires offset < 0x80000000;
   @ requires 0 < length <= 4096;
-  @ requires \valid_read((char *)value+(0..length-1));
+  @ requires \valid_read((const char *)value+(0..length-1));
   @ requires \valid_function(header_check);
   @ requires \valid(file_stat);
   @*/
@@ -253,10 +291,12 @@ file_stat_t * init_file_stats(file_enable_t *files_enable);
 /*@
   @ requires \valid(file_recovery);
   @ requires valid_read_string((char*)&file_recovery->filename);
+  @ requires valid_file_recovery(file_recovery);
   @ requires \valid_read((char *)buffer+(0..buffer_size-1));
   @ requires new_ext==\null || valid_read_string(new_ext);
-  @ ensures valid_read_string((char*)&file_recovery->filename);
+  @ ensures  valid_read_string((char*)&file_recovery->filename);
   @*/
+// ensures  valid_file_recovery(file_recovery);
 int file_rename(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int force_ext);
 
 /*@
@@ -264,14 +304,16 @@ int file_rename(file_recovery_t *file_recovery, const void *buffer, const int bu
   @ requires valid_read_string((char*)&file_recovery->filename);
   @ requires \valid_read((char *)buffer+(0..buffer_size-1));
   @ requires new_ext==\null || valid_read_string(new_ext);
+  @ requires valid_file_recovery(file_recovery);
   @ ensures valid_read_string((char*)&file_recovery->filename);
   @*/
+// ensures  valid_file_recovery(file_recovery);
 int file_rename_unicode(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int force_ext);
 
 void header_ignored_cond_reset(uint64_t start, uint64_t end);
 
 /*@
-  @ requires file_recovery_new==\null || \valid_read(file_recovery_new);
+  @ requires file_recovery_new==\null || valid_file_recovery(file_recovery_new);
   @*/
 void header_ignored(const file_recovery_t *file_recovery_new);
 
@@ -279,23 +321,26 @@ void header_ignored(const file_recovery_t *file_recovery_new);
   @ requires separation: \separated(file_recovery, file_recovery_new, &errno);
   @ requires \valid_read(file_recovery);
   @ requires \valid_read(file_recovery_new);
-  @ requires file_recovery->handle == \null || \valid(file_recovery->handle);
+  @ requires valid_file_recovery(file_recovery);
+  @ requires valid_file_recovery(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);
+// ensures  valid_file_recovery(file_recovery_new);
 int header_ignored_adv(const file_recovery_t *file_recovery, const file_recovery_t *file_recovery_new);
 
 /*@
   requires valid_stream: \valid(stream);
   requires whence_enum: whence == SEEK_SET || whence == SEEK_CUR || whence == SEEK_END;
   requires \separated(&errno, stream);
-  assigns *stream \from *stream, indirect:offset, indirect:whence;
-  assigns \result, errno \from indirect:*stream, indirect:offset,
-                                    indirect:whence;
+  assigns *stream, \result, errno;
 */
+// assigns *stream \from *stream, indirect:offset, indirect:whence;
+// assigns \result, errno \from indirect:*stream, indirect:offset, indirect:whence;
 int my_fseek(FILE *stream, off_t offset, int whence);
 
 /*@
@@ -323,9 +368,10 @@ time_t get_time_from_YYYY_MM_DD_HHMMSS(const char *date_asc);
 time_t get_time_from_YYYYMMDD_HHMMSS(const char *date_asc);
 
 /*@
-  @ requires \valid(list_search_space);
+  @ requires \valid_read(list_search_space);
   @ requires \valid(current_search_space);
   @ requires \valid(offset);
+  @ requires \separated(list_search_space, current_search_space, offset);
   @*/
 void get_prev_location_smart(const alloc_data_t *list_search_space, alloc_data_t **current_search_space, uint64_t *offset, const uint64_t prev_location);