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

src/file_ab.c: fix frama-c annotation

Browse source
This commit is contained in:
Christophe Grenier 2020-11-01 13:27:37 +01:00
parent 7bb300df96
commit 16ec8ee8b5
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_ab.c
View file

@ -52,7 +52,7 @@ struct ab_header
@ requires (buffer_size&1)==0;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires \valid(file_recovery);
@ requires file_recovery->data_check==&data_check_ab;
@ requires file_recovery->data_check==&data_check_addressbook;
@ requires \separated(buffer, file_recovery);
@ ensures \result == DC_CONTINUE || \result == DC_STOP;
@ assigns file_recovery->calculated_file_size;