luisgulo/testdisk
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

src/file_bmp.c: fix Frama-C annotations

Browse source
This commit is contained in:
Christophe Grenier 2021-06-06 14:58:32 +02:00
parent b6eb4fe3ab
commit b932ef701f
3 changed files with 22 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
src/file_bmp.c
View file

@ -35,6 +35,9 @@
#include "__fc_builtin.h"
#endif
/*@
@ requires valid_register_header_check(file_stat);
@*/
static void register_header_check_bmp(file_stat_t *file_stat);
const file_hint_t file_hint_bmp= {
@ -59,12 +62,19 @@ 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_hint_bmp, buffer+(..), 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);
@ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null);
@ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
@ ensures (\result == 1) ==> (file_recovery_new->time == 0);
@ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_bmp.extension);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size >= 65);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 65);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_size);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
@ assigns file_recovery_new->filename[0];
@ assigns file_recovery_new->time;
@ assigns file_recovery_new->file_stat;
@ -86,19 +96,7 @@ struct bmp_header
@ assigns file_recovery_new->checkpoint_offset;
@ assigns file_recovery_new->flags;
@ assigns file_recovery_new->extra;
@ ensures \result == 0 || \result == 1;
@ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null);
@ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
@ ensures (\result == 1) ==> \initialized(&file_recovery_new->time);
@ ensures (\result == 1) ==> (file_recovery_new->time == 0);
@ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_bmp.extension);
@ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size >= 65);
@ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
@ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 65);
@ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_size);
@ 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));
@ assigns file_recovery_new->data_check_tmp;
@*/
// 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)
@ -136,9 +134,6 @@ static int header_check_bmp(const unsigned char *buffer, const unsigned int buff
return 0;
}
/*@
@ requires \valid(file_stat);
@*/
static void register_header_check_bmp(file_stat_t *file_stat)
{
register_header_check(0, bmp_header,sizeof(bmp_header), &header_check_bmp, file_stat);

3
src/filegen.c
View file

@ -113,6 +113,8 @@ static void file_check_add_tail(file_check_t *file_check_new, file_check_list_t
/*@
@ loop unroll 256;
@ loop invariant 0 <= i <= 256;
@ loop invariant \forall integer j; (0 <= j < i) ==> newe->file_checks[j].list.prev == &newe->file_checks[j].list;
@ loop invariant \forall integer j; (0 <= j < i) ==> newe->file_checks[j].list.next == &newe->file_checks[j].list;
@ loop assigns i, newe->file_checks[0 .. i-1].list.prev, newe->file_checks[0 .. i-1].list.next;
@ loop variant 255-i;
@*/
@ -398,6 +400,7 @@ void reset_file_recovery(file_recovery_t *file_recovery)
file_recovery->checkpoint_offset=0;
file_recovery->flags=0;
file_recovery->extra=0;
file_recovery->data_check_tmp=0;
}
file_stat_t * init_file_stats(file_enable_t *files_enable)

3
src/filegen.h
View file

@ -101,6 +101,7 @@ struct file_recovery_struct
int checkpoint_status; /* 0=suspend at offset_checkpoint if offset_checkpoint>0, 1=resume at offset_checkpoint */
unsigned int blocksize;
unsigned int flags;
unsigned int data_check_tmp;
};
typedef struct
@ -300,6 +301,7 @@ void file_check_size_max(file_recovery_t *file_recovery);
ensures file_recovery->checkpoint_offset==0;
ensures file_recovery->flags==0;
ensures file_recovery->extra==0;
ensures file_recovery->data_check_tmp==0;
assigns file_recovery->filename[0];
assigns file_recovery->time;
assigns file_recovery->file_stat;
@ -321,6 +323,7 @@ void file_check_size_max(file_recovery_t *file_recovery);
assigns file_recovery->checkpoint_offset;
assigns file_recovery->flags;
assigns file_recovery->extra;
assigns file_recovery->data_check_tmp;
*/
// ensures valid_file_recovery(file_recovery);
void reset_file_recovery(file_recovery_t *file_recovery);