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

src/file_abr.c: stricter frama-c annotation

Browse source
This commit is contained in:
Christophe Grenier 2021-02-07 18:42:37 +01:00
parent b396d3af19
commit fa50d166ec
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/file_abr.c
View file

@ -83,7 +83,7 @@ static data_check_t data_check_abr(const unsigned char *buffer, const unsigned i
}
/*@
@ requires buffer_size > 0;
@ requires buffer_size >= 4 + sizeof(struct abr_header) ;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires valid_file_recovery(file_recovery);
@ requires \valid(file_recovery_new);