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

file_tiff*: additional frama-c annotations

Browse source
This commit is contained in:
Christophe Grenier 2019-12-07 20:31:13 +01:00
parent 1f77cbec99
commit ded0ae6ed7
2 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/file_tiff.h
View file

@ -99,6 +99,7 @@ unsigned int find_tag_from_tiff_header_le(const unsigned char *buffer, const uns
@ requires \valid(fr->handle);
@ requires \valid_read(&fr->extension);
@ requires valid_read_string(fr->extension);
@ requires fr->file_check==&file_check_tiff_le;
@ ensures \valid(fr->handle);
@ ensures valid_read_string(fr->extension);
@*/

1
src/file_tiff_be.c
View file

@ -659,6 +659,7 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
@ requires \valid(fr->handle);
@ requires \valid_read(&fr->extension);
@ requires valid_read_string(fr->extension);
@ requires fr->file_check==&file_check_tiff_be;
@*/
static void file_check_tiff_be(file_recovery_t *fr)
{