summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/filegen.c19
-rw-r--r--src/filegen.h2
2 files changed, 18 insertions, 3 deletions
diff --git a/src/filegen.c b/src/filegen.c
index 174912cd..86b1ffec 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -50,9 +50,6 @@ static int file_check_cmp(const struct td_list_head *a, const struct td_list_hea
#ifndef __FRAMAC__
#include "list_add_sorted.h"
-/*@ requires compar == file_check_cmp; */
-static inline void td_list_add_sorted(struct td_list_head *newe, struct td_list_head *head,
- int (*compar)(const struct td_list_head *a, const struct td_list_head *b));
#else
/*@
@@ -72,6 +69,7 @@ static inline void td_list_add_sorted_fcc(struct td_list_head *newe, struct td_l
@ loop invariant \valid(pos->prev);
@ loop invariant \valid(pos->next);
@ loop invariant pos == head || \separated(pos, head);
+ @ loop invariant finite(head);
@ loop assigns pos;
@*/
td_list_for_each(pos, head)
@@ -201,7 +199,9 @@ void register_header_check(const unsigned int offset, const void *value, const u
file_check_new->value=value;
file_check_new->length=length;
file_check_new->offset=offset;
+ /*@ assert header_check != \null; */
file_check_new->header_check=header_check;
+ /*@ assert file_check_new->header_check != \null; */
file_check_new->file_stat=file_stat;
/*@ assert \valid_read(file_check_new); */
@@ -356,6 +356,7 @@ void file_allow_nl(file_recovery_t *file_recovery, const unsigned int nl_mode)
/*@ assert valid_file_check_result(file_recovery); */
return;
}
+ /*@ assert \separated(file_recovery, buffer+(..)); */
/*@ assert valid_file_recovery(file_recovery); */
taille=fread(buffer,1, 4096,file_recovery->handle);
/*@ assert valid_file_recovery(file_recovery); */
@@ -577,6 +578,7 @@ file_stat_t * init_file_stats(file_enable_t *files_enable)
@ requires strlen(new_ext) < (1<<30);
@ requires separation: \separated(file_recovery, new_ext);
@ ensures valid_file_recovery(file_recovery);
+ @ ensures file_recovery->file_size == \old(file_recovery->file_size);
@*/
static int file_rename_aux(file_recovery_t *file_recovery, const char *new_ext)
{
@@ -628,6 +630,8 @@ static int file_rename_aux(file_recovery_t *file_recovery, const char *new_ext)
@ loop invariant odst <= dst <= odst + strlen(odst);
@ loop invariant valid_read_string(new_ext);
@ loop invariant strlen(new_ext) < (1<<30);
+ @ loop invariant valid_file_recovery(file_recovery);
+ @ loop invariant valid_string(&new_filename[0]);
@ loop assigns dst;
@ loop variant strlen(dst);
@*/
@@ -635,12 +639,14 @@ static int file_rename_aux(file_recovery_t *file_recovery, const char *new_ext)
dst++;
/* Add extension */
*dst++ = '.';
+ /*@ assert valid_read_string(new_ext); */
/*@ assert strlen(new_ext) < (1<<30); */
#ifdef DISABLED_FOR_FRAMAC
memcpy(dst, new_ext, strlen(new_ext)+1);
#else
strcpy(dst, new_ext);
#endif
+ /*@ assert valid_string(dst); */
/*@ assert valid_string(&new_filename[0]); */
if(strlen(new_filename) >= sizeof(file_recovery->filename))
{
@@ -672,6 +678,8 @@ static int file_rename_aux(file_recovery_t *file_recovery, const char *new_ext)
@ requires buffer_size < 1<<30;
@ requires \valid_read((char *)buffer+(0..buffer_size-1));
@ requires new_ext==\null || (valid_read_string(new_ext) && strlen(new_ext) < 1<<30);
+ @ requires \separated(filename, (char *)buffer+(0..buffer_size-1));
+ @ requires \separated(filename, new_ext);
@ ensures new_ext==\null || (valid_read_string(new_ext) && strlen(new_ext) < 1<<30);
@ ensures valid_string(filename);
@ ensures 0 < strlen(filename) < 1<<30;
@@ -827,7 +835,11 @@ int file_rename(file_recovery_t *file_recovery, const void *buffer, const int bu
/*@ assert new_ext==\null || valid_read_string(new_ext); */
if(buffer!=NULL && 0 <= offset && offset < buffer_size &&
_file_rename(file_recovery->filename, buffer, buffer_size, offset, new_ext, append_original_ext)==0)
+ {
+ /*@ assert valid_file_recovery(file_recovery); */
return 0;
+ }
+ /*@ assert valid_file_recovery(file_recovery); */
/*@ assert valid_string((char *)(&file_recovery->filename)); */
/*@ assert new_ext==\null || valid_read_string(new_ext); */
if(new_ext==NULL)
@@ -850,6 +862,7 @@ int file_rename(file_recovery_t *file_recovery, const void *buffer, const int bu
@ ensures new_ext==\null || (valid_read_string(new_ext) && strlen(new_ext) < 1<<30);
@ ensures valid_read_string((char*)&file_recovery->filename);
@ ensures valid_file_recovery(file_recovery);
+ @ ensures file_recovery->file_size == \old(file_recovery->file_size);
@*/
static 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 append_original_ext)
{
diff --git a/src/filegen.h b/src/filegen.h
index c51ef7f4..c713eafb 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -159,6 +159,7 @@ typedef struct
(file_recovery->file_check == \null || \valid_function(file_recovery->file_check)) &&
(file_recovery->file_rename == \null || \valid_function(file_recovery->file_rename)) &&
\separated(file_recovery, file_recovery->extension) &&
+ \separated(file_recovery, file_recovery->file_stat) &&
\separated(file_recovery, file_recovery->handle) &&
\initialized(&file_recovery->calculated_file_size) &&
\initialized(&file_recovery->file_check) &&
@@ -378,6 +379,7 @@ void register_header_check(const unsigned int offset, const void *value, const u
/*@
@ requires valid_file_enable_node(files_enable);
+ @ decreases 0;
@ ensures valid_file_stat(\result);
@*/
file_stat_t * init_file_stats(file_enable_t *files_enable);