summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-10-13 10:05:24 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2019-10-13 10:05:24 +0200
commit920c1660395aa5cbaff9f0926622f40d32ec7952 (patch)
tree21da8f24b83e147b49c9c39fc93dd1214ec8cbb5
parent11c73ceb734013980c752598ca85eab238665524 (diff)
file_bmp.c: add new frama-c annotations
-rw-r--r--src/file_bmp.c36
-rw-r--r--src/filegen.h139
2 files changed, 157 insertions, 18 deletions
diff --git a/src/file_bmp.c b/src/file_bmp.c
index dfc824b..340a1c6 100644
--- a/src/file_bmp.c
+++ b/src/file_bmp.c
@@ -60,8 +60,10 @@ struct bmp_header
@ requires buffer_size >= 18;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires \valid_read(file_recovery);
+ @ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
+ @ requires separation: \separated(file_recovery, file_recovery_new);
@ ensures \result == 0 || \result == 1;
@ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_bmp.extension);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size >= 65);
@@ -112,6 +114,7 @@ static void register_header_check_bmp(file_stat_t *file_stat)
#define BLOCKSIZE 65536u
int main()
{
+ const char *fn = "recup_dir.1/f0000000.bmp";
unsigned char buffer[BLOCKSIZE];
int res;
file_recovery_t file_recovery_new;
@@ -124,6 +127,7 @@ int main()
#endif
reset_file_recovery(&file_recovery);
+ /*@ assert file_recovery.file_stat == \null; */
file_recovery.blocksize=BLOCKSIZE;
file_recovery_new.blocksize=BLOCKSIZE;
file_recovery_new.data_check=NULL;
@@ -137,19 +141,20 @@ int main()
file_stats.file_hint=&file_hint_bmp;
file_stats.not_recovered=0;
file_stats.recovered=0;
- file_hint_bmp.register_header_check(&file_stats);
+ register_header_check_bmp(&file_stats);
if(header_check_bmp(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
return 0;
- memcpy(file_recovery_new.filename, "demo", 5);
+ /*@ assert valid_read_string(fn); */
+ strcpy(file_recovery_new.filename, fn);
+ file_recovery_new.file_stat=&file_stats;
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
/*@ assert file_recovery_new.extension == file_hint_bmp.extension; */
/*@ assert file_recovery_new.calculated_file_size >= 65; */
/*@ assert file_recovery_new.file_size == 0; */
/*@ assert file_recovery_new.min_filesize == 65; */
/*@ assert file_recovery_new.file_check == &file_check_size; */
/*@ assert file_recovery_new.data_check == &data_check_size; */
- file_recovery_new.file_stat=&file_stats;
/*@ assert file_recovery_new.file_stat->file_hint!=NULL; */
- if(file_recovery_new.data_check!=NULL)
{
unsigned char big_buffer[2*BLOCKSIZE];
data_check_t res_data_check=DC_CONTINUE;
@@ -158,7 +163,7 @@ int main()
/*@ assert file_recovery_new.data_check == &data_check_size; */
/*@ assert file_recovery_new.file_size == 0; */;
/*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
- res_data_check=file_recovery_new.data_check(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ res_data_check=data_check_size(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
file_recovery_new.file_size+=BLOCKSIZE;
if(res_data_check == DC_CONTINUE)
{
@@ -166,7 +171,7 @@ int main()
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
#endif
- file_recovery_new.data_check(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ data_check_size(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
}
}
{
@@ -179,21 +184,16 @@ int main()
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
header_check_bmp(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
}
- if(file_recovery_new.file_check!=NULL)
- {
- file_recovery_new.handle=fopen("demo", "rb");
- if(file_recovery_new.handle!=NULL)
- {
- (file_recovery_new.file_check)(&file_recovery_new);
- fclose(file_recovery_new.handle);
- }
- }
- if(file_recovery_new.file_rename!=NULL)
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ if(file_recovery_new.handle!=NULL)
{
- /*@ assert valid_read_string((char *)&file_recovery_new.filename); */
- (file_recovery_new.file_rename)(&file_recovery_new);
+ file_check_size(&file_recovery_new);
+ fclose(file_recovery_new.handle);
}
return 0;
}
diff --git a/src/filegen.h b/src/filegen.h
index d187fe9..2654443 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -119,19 +119,122 @@ typedef struct
#define NL_BARECR (1 << 2)
void free_header_check(void);
+
+/*@
+ @ requires \valid(file_recovery);
+ @*/
void file_allow_nl(file_recovery_t *file_recovery, const unsigned int nl_mode);
+
+/*@
+ @ requires \valid(handle);
+ @ requires footer_length > 0;
+ @ requires \valid_read((char *)footer+(0..footer_length-1));
+ @*/
uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const unsigned int footer_length);
+
+/*@
+ @ requires \valid(file_recovery);
+ @ requires footer_length > 0;
+ @ requires \valid_read((char *)footer+(0..footer_length-1));
+ @*/
void file_search_footer(file_recovery_t *file_recovery, const void*footer, const unsigned int footer_length, const unsigned int extra_length);
+
+/*@
+ @ requires \valid(file_recovery);
+ @ requires footer_length > 0;
+ @ requires \valid_read((char *)footer+(0..footer_length-1));
+ @*/
void file_search_lc_footer(file_recovery_t *file_recovery, const unsigned char*footer, const unsigned int footer_length);
+
+/*@
+ @ requires \valid(list_search_space);
+ @*/
void del_search_space(alloc_data_t *list_search_space, const uint64_t start, const uint64_t end);
+
+/*@
+ @ requires buffer_size > 0;
+ @ requires \valid_read((char *)buffer+(0..buffer_size-1));
+ @ requires \valid(file_recovery);
+ @ assigns \nothing;
+ @ ensures \result == DC_STOP || \result == DC_CONTINUE;
+ @*/
data_check_t data_check_size(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
+
+/*@
+ @ requires \valid(file_recovery);
+ @*/
void file_check_size(file_recovery_t *file_recovery);
+
+/*@
+ @ requires \valid(file_recovery);
+ @*/
void file_check_size_min(file_recovery_t *file_recovery);
+
+/*@
+ @ requires \valid(file_recovery);
+ @*/
void file_check_size_max(file_recovery_t *file_recovery);
+
+/*@
+ requires \valid(file_recovery);
+ ensures file_recovery->filename[0]=='\0';
+ ensures file_recovery->time==0;
+ ensures file_recovery->file_stat==\null;
+ ensures file_recovery->handle==\null;
+ ensures file_recovery->file_size==0;
+ ensures file_recovery->location.list.prev==&file_recovery->location.list;
+ ensures file_recovery->location.list.next==&file_recovery->location.list;
+ ensures file_recovery->location.end==0;
+ ensures file_recovery->location.data==0;
+ ensures file_recovery->extension==\null;
+ ensures file_recovery->min_filesize==0;
+ ensures file_recovery->calculated_file_size==0;
+ ensures file_recovery->data_check==\null;
+ ensures file_recovery->file_check==\null;
+ ensures file_recovery->file_rename==\null;
+ ensures file_recovery->offset_error==0;
+ ensures file_recovery->offset_ok==0;
+ ensures file_recovery->checkpoint_status==0;
+ ensures file_recovery->checkpoint_offset==0;
+ ensures file_recovery->flags==0;
+ ensures file_recovery->extra==0;
+ assigns file_recovery->filename[0];
+ assigns file_recovery->time;
+ assigns file_recovery->file_stat;
+ assigns file_recovery->handle;
+ assigns file_recovery->file_size;
+ assigns file_recovery->location.list.prev;
+ assigns file_recovery->location.list.next;
+ assigns file_recovery->location.end;
+ assigns file_recovery->location.data;
+ assigns file_recovery->extension;
+ assigns file_recovery->min_filesize;
+ assigns file_recovery->calculated_file_size;
+ assigns file_recovery->data_check;
+ assigns file_recovery->file_check;
+ assigns file_recovery->file_rename;
+ assigns file_recovery->offset_error;
+ assigns file_recovery->offset_ok;
+ assigns file_recovery->checkpoint_status;
+ assigns file_recovery->checkpoint_offset;
+ assigns file_recovery->flags;
+ assigns file_recovery->extra;
+*/
void reset_file_recovery(file_recovery_t *file_recovery);
+
+/*@
+ @ requires length > 0;
+ @ requires \valid_read((char *)value+(0..length-1));
+ @ requires \valid_function(header_check);
+ @ requires \valid(file_stat);
+ @*/
void register_header_check(const unsigned int offset, const void *value, const unsigned int length, int (*header_check)(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),
file_stat_t *file_stat);
+
+/*@
+ @ requires \valid(files_enable);
+ @*/
file_stat_t * init_file_stats(file_enable_t *files_enable);
/*@
@@ -151,12 +254,48 @@ int file_rename(file_recovery_t *file_recovery, const void *buffer, const int bu
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);
+ @*/
void header_ignored(const file_recovery_t *file_recovery_new);
+
+/*@
+ @ requires \valid_read(file_recovery);
+ @ requires \valid_read(file_recovery_new);
+ @ requires \initialized(&file_recovery->file_check);
+ @ requires \initialized(&file_recovery->handle);
+ @ ensures \result == 0 || \result == 1;
+ @*/
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;
+ assigns *stream \from *stream, indirect:offset, indirect:whence;
+ assigns \result, __fc_errno \from indirect:*stream, indirect:offset,
+ indirect:whence;
+*/
int my_fseek(FILE *stream, off_t offset, int whence);
+
+/*@
+ @ requires \valid_read(date_asc + (0 .. 11));
+ @*/
time_t get_time_from_YYMMDDHHMMSS(const char *date_asc);
+
+/*@
+ @ requires \valid_read(date_asc + (0 .. 18));
+ @*/
time_t get_time_from_YYYY_MM_DD_HH_MM_SS(const char *date_asc);
+
+/*@
+ @ requires \valid_read(date_asc + (0 .. 16));
+ @*/
time_t get_time_from_YYYY_MM_DD_HHMMSS(const char *date_asc);
+
+/*@
+ @ requires \valid_read(date_asc + (0 .. 14));
+ @*/
time_t get_time_from_YYYYMMDD_HHMMSS(const char *date_asc);
#ifdef __cplusplus